Does There Exist an M-Proof Shorter than Twenty-Lines of the Rule of Antecedent Commutation?

Question

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?

Answer 1

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:

                   level
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:

                                                    level
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))

Answer 2

$$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.