Editing Deduction theorem (section)

==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
*[((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'')]→[''Q''→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R''))] 5. axiom 1
*''Q''→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R'')) 6. modus ponens 3,5
*[''Q''→(((''Q''→''R'')→''Q'')→((''Q''→''R'')→''R''))]→([''Q''→((''Q''→''R'')→''Q'')]→[''Q''→((''Q''→''R'')→''R''))]) 7. axiom 2
*[''Q''→((''Q''→''R'')→''Q'')]→[''Q''→((''Q''→''R'')→''R''))] 8. modus ponens 6,7
*''Q''→((''Q''→''R'')→''R'')) 9. modus ponens 4,8 QED

{{anchor|Using the Curry–Howard correspondence}}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