Examples of deduction
#"Prove" axiom 1: ''P''→(''Q''→''P'') #:*''P'' 1. hypothesis #:**''Q'' 2. hypothesis #:**''P'' 3. reiteration of 1 #:*''Q''→''P'' 4. deduction from 2 to 3 #:''P''→(''Q''→''P'') 5. deduction from 1 to 4 QED #"Prove" axiom 2: #:*''P''→(''Q''→''R'') 1. hypothesis #:**''P''→''Q'' 2. hypothesis #:***''P'' 3. hypothesis #:***''Q'' 4. modus ponens 3,2 #:***''Q''→''R'' 5. modus ponens 3,1 #:***''R'' 6. modus ponens 4,5 #:**''P''→''R'' 7. deduction from 3 to 6 #:*(''P''→''Q'')→(''P''→''R'') 8. deduction from 2 to 7 #:(''P''→(''Q''→''R''))→((''P''→''Q'')→(''P''→''R'')) 9. deduction from 1 to 8 QED #Using axiom 1 to show ((''P''→(''Q''→''P''))→''R'')→''R'': #:*(''P''→(''Q''→''P''))→''R'' 1. hypothesis #:*''P''→(''Q''→''P'') 2. axiom 1 #:*''R'' 3. modus ponens 2,1 #:((''P''→(''Q''→''P''))→''R'')→''R'' 4. deduction from 1 to 3 QEDVirtual rules of inference
From the examples, you can see that we have added three virtual (or extra and temporary) rules of inference to our normal axiomatic logic. These are "hypothesis", "reiteration", and "deduction". The normal rules of inference (i.e. "modus ponens" and the various axioms) remain available. 1. Hypothesis is a step where one adds an additional premise to those already available. So, if your previous step ''S'' was deduced as: : then one adds another premise ''H'' and gets: : This is symbolized by moving from the ''n''-th level of indentation to the ''n''+1-th level and saying ::::*''S'' previous step ::::**''H'' hypothesis 2. Reiteration is a step where one re-uses a previous step. In practice, this is only necessary when one wants to take a hypothesis that is not the most recent hypothesis and use it as the final step before a deduction step. 3. Deduction is a step where one removes the most recent hypothesis (still available) and prefixes it to the previous step. This is shown by unindenting one level as follows: :::::*''H'' hypothesis :::::*......... (other steps) :::::*''C'' (conclusion drawn from ''H'') ::::*''H''→''C'' deductionConversion from proof using the deduction meta-theorem to axiomatic proof
In axiomatic versions of propositional logic, one usually has among the axiom schemas (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 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 theHelpful theorems
If one intends to convert a complicated proof using the deduction theorem to a straight-line proof not using the deduction theorem, then it would probably be useful to prove these theorems once and for all at the beginning and then use them to help with the conversion: : helps convert the hypothesis steps. : helps convert modus ponens when the major premise is not dependent on the hypothesis, replaces axiom 2 while avoiding a use of axiom 1. : helps convert modus ponens when the minor premise is not dependent on the hypothesis, replaces axiom 2 while avoiding a use of axiom 1. These two theorems jointly can be used in lieu of axiom 2, although the converted proof would be more complicated: : :Proof of the deduction theorem
We prove the deduction theorem in a Hilbert-style deductive system of propositional calculus. Let be a set of formulas and and formulas, such that . We want to prove that . Since , there is a proof of from . We prove the theorem by induction on the proof length ''n''; thus the induction hypothesis is that for any , and such that there is a proof of from of length up to ''n'', holds. If ''n'' = 1 then is member of the set of formulas . Thus either , in which case is simply , which is derivable by substitution from ''p'' → ''p'', which is derivable from the axioms, and hence also , or is in , in which case ; it follows from axiom ''p'' → (''q'' → ''p'') with substitution that and hence by modus ponens that . Now let us assume the induction hypothesis for proofs of length up to ''n'', and let be a formula provable from with a proof of length ''n''+1. Then there are two possibilities: # is member of the set of formulas ; in this case we proceed as for ''n''=1. # is arrived at by using modus ponens. Then there is a formula ''C'' such that proves and , and modus ponens is then used to prove . The proofs of and are with at most ''n'' steps, and by the induction hypothesis we have and . By the axiom (''p'' → (''q'' → ''r'')) → ((''p'' → ''q'') → (''p'' → ''r'')) with substitution it follows that , and by using modus ponens twice we have . Thus in all cases the theorem holds also for ''n''+1, and by induction the deduction theorem is proven.The deduction theorem in predicate logic
The deduction theorem is also valid in first-order logic in the following form: *If ''T'' is a theory and ''F'', ''G'' are formulas with ''F''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 These three steps can be stated succinctly using theSee also
* Cut-elimination theorem * Conditional proof *Notes
References
* September/October 2008 * * * . * {{Citation , last1=Shoenfield , first1=Joseph R. , author1-link=Joseph R. Shoenfield , title=Mathematical Logic , orig-year=1967 , publisher= A K Peters , edition=2nd , isbn=978-1-56881-135-2 , year=2001External links