Deduction Theorem - Example of Conversion

Example of Conversion

To illustrate how one can convert a natural deduction to the axiomatic form of proof, we apply it to the tautology Q→((Q→R)→R). In practice, it is usually enough to know that we could do this. We normally use the natural-deductive form in place of the much longer axiomatic proof.

First, we write a proof using a natural-deduction like method:

• • Q 1. hypothesis
    • Q→R 2. hypothesis
    • R 3. modus ponens 1,2
  • (Q→R)→R 4. deduction from 2 to 3
• Q→((Q→R)→R) 5. deduction from 1 to 4 QED

Second, we convert the inner deduction to an axiomatic proof:

• (Q→R)→(Q→R) 1. theorem schema (A→A)
• ((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. axiom 2
• ((Q→R)→Q)→((Q→R)→R) 3. modus ponens 1,2
• Q→((Q→R)→Q) 4. axiom 1
  • Q 5. hypothesis
  • (Q→R)→Q 6. modus ponens 5,4
  • (Q→R)→R 7. modus ponens 6,3
• Q→((Q→R)→R) 8. deduction from 5 to 7 QED

Third, we convert the outer deduction to an axiomatic proof:

• (Q→R)→(Q→R) 1. theorem schema (A→A)
• ((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. axiom 2
• ((Q→R)→Q)→((Q→R)→R) 3. modus ponens 1,2
• Q→((Q→R)→Q) 4. axiom 1
• → 5. axiom 1
• Q→(((Q→R)→Q)→((Q→R)→R)) 6. modus ponens 3,5
• →(→) 7. axiom 2
• → 8. modus ponens 6,7
• Q→((Q→R)→R)) 9. modus ponens 4,8 QED

These three steps can be stated succinctly using the Curry–Howard correspondence:

• first, in lambda calculus, the function f = λa. λb. b a has type q → (q → r) → r
• second, by lambda elimination on b, f = λa. s i (k a)
• third, by lambda elimination on a, f = s (k (s i)) k