Peter Smith writes in his Type of Proof System

"I take it that neither of those proofs is wonderfully obvious or natural. For another example, consider (P -> (Q -> R)) $\vdash$$_M$ (Q -> (P -> R)). Again, that's an intuitively ob-vious validity, and can be checked by a quick tree proof (do it!). But the shortest known m-proof has twenty-one lines..."

The M-system has axiom schema:

Ax1. (A -> (B -> A))

Ax2. ((A -> (B -> C)) -> ((A -> B) -> (A -> C)))

Ax3. (($\lnot$ B -> $\lnot$A) -> (A -> B))

The only rule of inference is formal modus ponens; from A and (A -> C) infer C.

Can (P -> (Q -> R)) $\vdash$$_M$ (Q -> (P -> R)) get proven in less than twenty-one lines?

  • $\begingroup$ Assume condensed detachment as the only rule of inference for the following. The system {CCaCbcCCabCac, CaCba} has 2 step, level 2 proof of Caa. {CCaCbcCCabCac, CaCba, CpCqr} has a 4 step, level 4 proof of CqCpr. {CCaCbcCCabCac, CaCba, Cpq, Cqr} has a 3 step, level 3 proof of Cpr. $\endgroup$ – Doug Spoonwood Aug 25 '16 at 14:05
  • $\begingroup$ The system {CaCba, CCaCbcCCabCac, CCNaNbCba, CNCpNqp} has a 10 step, level 10 proof of the wff p also! At least, the above hold via some reasoning and use of OTTER. In the maximal case, a condensed detachment proof of 1 step corresponds to a 3 step substitution and detachment proof of the same wff. So, the 10 step hyper-resolution proof of OTTER implying a 10 step condensed proof entails that a 31 step proof of the wff p can get written for the substitution and detachment system. $\endgroup$ – Doug Spoonwood Aug 25 '16 at 14:25

$$P \implies Q \implies R \vdash_M Q \implies P \implies R \tag{1}$$

A proof of this can be constructed using typed lambda calculus.

Assuming a lambda expression $A$ exists of type $P \to Q \to R$. Then the following lambda expression:

$$\lambda ~ b~c~.~A~c~b$$

has type $Q \to P \to R$, given that $b$ has type $Q$ and $c$ has type $P$. Reducing this expression to combinatory logic, gives:

$$\lambda ~ b~c~.~A~c~b \quad \equiv \quad S (K (S A)) K$$

The above combinatory expression has $4$ instances of function application, $4$ instances of combinators, and there is the assumption of $A$ itself, so there is a proof of (1) using only $9$ steps.

Given the following types:

  • $A ~:~ P \to Q \to R$
  • $b ~:~ Q$
  • $c ~:~ P$

and distinguishing the combinators as $S_2 (K_2 (S_1 A)) K_1$ , the types of $K_1$, $K_2$, $S_1$, and $S_2$ work out as:

  • $S_1 ~:~ (P \to Q \to R) \to (P \to Q) \to P \to R $
  • $K_1 ~:~ Q \to P \to Q$
  • $S_2 ~:~ (Q \to (P \to Q) \to P \to R) \to (Q \to P \to Q) \to Q \to P \to R $
  • $K_2 ~:~ ((P \to Q) \to P \to R) \to Q \to (P \to Q) \to P \to R$

And the proof looks like:

$$\begin{array} {lll} (1) & P \implies Q \implies R & \text{Given} \\ (2) & (P \implies Q \implies R) \implies (P \implies Q) \implies P \implies R & \text{Ax 2}, a = P, b = Q, c = R \\ (3) & Q \implies P \implies Q & \text{Ax 1}, a = Q, b = Q \\ (4) & (Q \implies (P \implies Q) \implies P \implies R) \implies (Q \implies P \implies Q) \implies Q \implies P \implies R & \text{Ax 2}, a = Q, b = P \implies Q, c = P \implies R \\ (5) & ((P \implies Q) \implies P \implies R) \implies Q \implies (P \implies Q) \implies P \implies R & \text{Ax 1}, a = (P \implies Q) \implies P \implies R, b = Q \\ (6) & (P \implies Q) \implies P \implies R & \text{Modus Ponens}, (1), (2) \\ (7) & Q \implies (P \implies Q) \implies P \implies R & \text{Modus Ponens}, (6), (5) \\ (8) & (Q \implies P \implies Q) \implies Q \implies P \implies R & \text{Modus Ponens}, (7), (4) \\ (9) & Q \implies P \implies R & \text{Modus Ponens}, (3), (8) \\ \end{array}$$

The tedious nature of constructing this proof demonstrates what Smith was writing in his essay. Hilbert's axiom system is not something you want to use in practice, it's purpose is moreso to demonstrate that logic is possible. Later work by Gentzen was motivated more by making the logic useful.

  • $\begingroup$ "The above combinatory expression has 4 instances of function application, 4 instances of combinators, and there is the assumption of A itself, so there is a proof of (1) using only 9 steps." I'm really not very well acquainted with combinatory logic. But, I've read that there exists a correspondence with condensed detachment. Please correct any errors I make. Suppose we had the following combinator L: CCpqCCqrCpr. (LL)(LL) is a theorem. We have 4 instances of the combinator L. 3 instances of function application. So, a 7 step substitution and detachment proof exists... $\endgroup$ – Doug Spoonwood Aug 25 '16 at 5:43
  • $\begingroup$ And that may well hold. But, a 6 step substitution and detachment proof exists of the result CCpCqrCCsqCpCsr. $\endgroup$ – Doug Spoonwood Aug 25 '16 at 5:46
  • $\begingroup$ @DougSpoonwood I'm not sure what you are trying to establish. With lambda calculus / combinatory logic (they are 2 different ways of writing the same thing) , the expressions are proofs, and the types associated with the expressions are theorems. For example, if the type of $A$ is $x \to y$, and the type of $B$ is $x$, then the type of $AB$ is $y$, and $AB$ is a proof of the theorem $y$ given the premises (the types of $A$ and $B$). An example of a lambda expression with the type of $L$ would be $\lambda ~ x ~ y ~ . ~ (\lambda ~ z ~ . y ~ x ~ z)$ $\endgroup$ – DanielV Aug 25 '16 at 6:18
  • $\begingroup$ What do you mean by lambda expression? If lambda expression means the same as what Wikipedia calls a lamdba term en.wikipedia.org/wiki/Lambda_calculus, then you didn't provide an example of a lambda expression. If lambda expression means lambda term, what you provided in your last sentence doesn't satisfy the definition of a lambda expression. $\endgroup$ – Doug Spoonwood Aug 25 '16 at 13:35
  • $\begingroup$ @DougSpoonwood $\lambda~x~y~.~z$ is a common abbreviation for $\lambda ~x~.~\lambda ~y~.~z$, it's called currying, the principle is that a $n$-arity function is effectively the same thing as a $1$-arity function that returns an $n-1$-arity function. I recommend learning lambda calculus, it is the basis of all constructive logic. There was a pivotal point in history where the lambda expressions evolved from being used as theorems into being used as proofs. So when you study it, things like church encoding etc are all pre -pivot, and things like type theory are all post pivot. $\endgroup$ – DanielV Aug 25 '16 at 14:25

Suppose we rewrite the definition of well-formed formula of M in Polish notation. Then, it follows that the correlates of the above axiom schema can get written as the following:

Ax1 CaCba            0
Ax2 CCaCbcCCabCac    0
Ax3 CCNbNaCba        0

Formal modus ponens in Smith's system L corresponds to C-detachment; from Cac and a, we may infer c.

The question then corresponds to asking:

"Given CpCqr as a premiss in the above system in Polish notation, can we derive CqCpr in less than twenty-one lines?"

Consider the following:

premiss                      1 CpCqr                  0
Ax2 a/p, b/q, c/r            2 CCpCqrCCpqCpr          1
2 * C1-3                     3 CCpqCpr                2
Ax1 a/CCpqCpr, b/q           4 CCCpqCprCqCCpqCpr      1
4 * C3-5                     5 CqCCpqCpr              3
Ax2 a/q, b/Cpq, c/Cpr        6 CCqCCpqCprCCqCpqCqCpr  1
6 * C5-7                     7 CCqCpqCqCpr            4
Ax1 a/q, b/p                 8 CqCpq                  1
7 * C8-9                     9 CqCpr                  5

Consequently, given CpCqr as a premiss, CqCpr can get derived in nine steps. Nine is less than twenty-one. Therefore, (P -> (Q -> R)) ⊢$_M$ (Q -> (P -> R) can get proven in less than twenty-one steps.

Existence of such a proof:

(a -> (b -> a))
((a -> (b -> c)) -> ((a -> b) -> (a -> c)))
(p -> (q -> r))
((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
((p -> q) -> (p -> r))
(((p -> q) -> (p -> r)) -> (q -> ((p -> q) -> (p -> r))))
(q -> ((p -> q) -> (p -> r)))
((q -> ((p -> q) -> (p -> r))) -> ((q -> (p -> q)) -> (q -> (p -> r))))
((q -> (p -> q)) -> (q -> (p -> r)))
(q -> (p -> q))
(q -> (p -> r))
  • 2
    $\begingroup$ Good answer. However, in regards to your opening sentence of "suppose we rewrite the definition of well-formed formula of M in polish notation," I have a bit of confusion. At the end of your post you state "...Therefore (P -> (Q -> R)) ⊢m (Q -> (P -> R)" can get proven in less than twenty-one steps" which means that you are saying this particular statement of M can be proven in M in less than 21 steps, correct? But wasn't what was shown only that one can correspond with the system M an equivalent system which uses a different yet equivalent definition of well-formed-formulas? $\endgroup$ – Boolean_functions Aug 25 '16 at 1:26
  • 2
    $\begingroup$ You then show that the equivalent statement in this system can be proven in less than 21 steps. What I'm having trouble with is that you seemed to imply that the statement can be proven in M in less than 21 steps. Are you saying "Consider a different but equivalent system...here the equivalent statement can be proven in less than 21 steps" or are you instead saying "let's rewrite the definition of WFFs in M...then yes we can prove the statement in M in less than 21 steps", If it's the latter I'd have to disagree on the grounds that the system being used wouldn't actually be M. $\endgroup$ – Boolean_functions Aug 25 '16 at 1:27
  • $\begingroup$ @Boolean_functions Yes, I'm saying that particular statement can get proven in less then 21 steps. No, I didn't show that one can correspond the Polish notation system, P, with an equivalent system. I presumed that I, or someone else, could do so. To show that you might point out that every well-formed satisfies the definition of a well-formed formula. Each formula satisfies one of the clauses of such a definition. If the formula F is variable in M, then the formula F' is a variable in M. If F is of the type (a->b) in M, then F' is of the type Cab in P. If ... $\endgroup$ – Doug Spoonwood Aug 25 '16 at 1:38
  • 2
    $\begingroup$ Yes, I understand you didn't show formally that one can correspond the polish notation system with an equivalent system. I should have made clear that I understood you were presuming you or someone else could. The thoughts behind my comments originally stemmed from a thought that ran as follows: let's suppose there was yet another substantially different way to rewrite the definition of well-formed formulas of M. $\endgroup$ – Boolean_functions Aug 25 '16 at 1:51
  • 2
    $\begingroup$ Instead of re-writing them in polish notation, we re-wrote them in such-and-such-notation, but let's say that (for whatever reason) it is a complex procedure to translate the statements which used the old definition of WFFs into the statements which use the such-and-such-notation. If the method of translation was inefficient, then this translation would most likely be considered as part of the proof. Point being, wouldn't the process of determining the corresponding WFFs need to be efficient (with "efficient" being defined)? $\endgroup$ – Boolean_functions Aug 25 '16 at 1:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.