Editing Deduction theorem (section)

==Conversion from proof using the deduction meta-theorem to axiomatic proof==
In axiomatic versions of propositional logic, one usually has among the [[axiom schema]]s (where ''P'', ''Q'', and ''R'' are replaced by any propositions):
*Axiom 1 is: ''P''→(''Q''→''P'')
*Axiom 2 is: (''P''→(''Q''→''R''))→((''P''→''Q'')→(''P''→''R''))
*Modus ponens is: from ''P'' and ''P''→''Q'' infer ''Q''

These axiom schemas are chosen to enable one to derive the deduction theorem from them easily. So it might seem that we are begging the question. However, they can be justified by checking that they are [[tautology (logic)|tautologies]] using truth tables and that modus ponens preserves truth.

From these axiom schemas one can quickly deduce the theorem schema ''P''→''P'' (reflexivity of implication), which is used below:
# (''P''→((''Q''→''P'')→''P''))→((''P''→(''Q''→''P''))→(''P''→''P'')) from axiom schema 2 with ''P'', (''Q''→''P''), ''P''
# ''P''→((''Q''→''P'')→''P'') from axiom schema 1 with ''P'', (''Q''→''P'')
# (''P''→(''Q''→''P''))→(''P''→''P'') from modus ponens applied to step 2 and step 1
# ''P''→(''Q''→''P'') from axiom schema 1 with ''P'', ''Q''
# ''P''→''P'' from modus ponens applied to step 4 and step 3

Suppose that we have that Γ and ''H'' together prove ''C'', and we wish to show that Γ proves ''H''→''C''. For each step ''S'' in the deduction that is a premise in Γ (a reiteration step) or an axiom, we can apply modus ponens to the axiom 1, ''S''→(''H''→''S''), to get ''H''→''S''. If the step is ''H'' itself (a hypothesis step), we apply the theorem schema to get ''H''→''H''. If the step is the result of applying modus ponens to ''A'' and ''A''→''S'', we first make sure that these have been converted to ''H''→''A'' and ''H''→(''A''→''S'') and then we take the axiom 2, (''H''→(''A''→''S''))→((''H''→''A'')→(''H''→''S'')), and apply modus ponens to get (''H''→''A'')→(''H''→''S'') and then again to get ''H''→''S''. At the end of the proof we will have ''H''→''C'' as required, except that now it only depends on Γ, not on ''H''. So the deduction step will disappear, consolidated into the previous step which was the conclusion derived from ''H''.

To minimize the complexity of the resulting proof, some preprocessing should be done before the conversion. Any steps (other than the conclusion) that do not actually depend on ''H'' should be moved up before the hypothesis step and unindented one level. And any other unnecessary steps (which are not used to get the conclusion or can be bypassed), such as reiterations that are not the conclusion, should be eliminated.

During the conversion, it may be useful to put all the applications of modus ponens to axiom 1 at the beginning of the deduction (right after the ''H''→''H'' step).

When converting a modus ponens, if ''A'' is outside the scope of ''H'', then it will be necessary to apply axiom 1, ''A''→(''H''→''A''), and modus ponens to get ''H''→''A''. Similarly, if ''A''→''S'' is outside the scope of ''H'', apply axiom 1, (''A''→''S'')→(''H''→(''A''→''S'')), and modus ponens to get ''H''→(''A''→''S''). It should not be necessary to do both of these, unless the modus ponens step is the conclusion, because if both are outside the scope, then the modus ponens should have been moved up before ''H'' and thus be outside the scope also.

Under the [[Curry–Howard correspondence]], the above conversion process for the deduction [[meta-theorem]] is analogous to the [[Combinatory logic#Completeness of the S-K basis|conversion process]] from [[lambda calculus]] terms to terms of [[combinatory logic]], where axiom 1 corresponds to the K combinator, and axiom 2 corresponds to the S combinator.  Note that the I combinator corresponds to the theorem schema ''P''→''P''.