Deduction theorem

You don't need to be Editor-In-Chief to add or edit content to WikiDoc. You can begin to add to or edit text on this WikiDoc page by clicking on the edit button at the top of this page. Next enter or edit the information that you would like to appear here. Once you are done editing, scroll down and click the Save page button at the bottom of the page.

In mathematical logic, the deduction theorem states that if a formula F is deducible from E then the implication E → F is demonstrable (i.e. it is "deducible" from the empty set). In symbols, if , then

The deduction theorem may be generalized to any finite sequence of assumption formulas such that from

, infer , and so on until

.

The deduction theorem is a meta-theorem: it is used to deduce proofs in a given theory though it is not a theorem of the theory itself.

The deduction meta-theorem is one of the most important meta-theorems. In some systems of logic, it is taken as a rule of inference, an introduction rule for "→". In other systems, proving it from the axioms is the first major task in proving that the logic is complete. It is very hard to prove anything in propositional logic without using the deduction meta-theorem. And usually quite easy, if you can use it.

Examples of deduction

"Prove" axiom 1:

• • 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 QED

Virtual 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 which 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 deduction

Conversion 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

From these one can quickly deduce the theorem schema P→P (see propositional calculus). 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.

Suppose that we have that Γ and H prove C, and we wish to show that Γ proves H→C. For each step S in the deduction which 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) which 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 which 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 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.

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

The resolution theorem

The Resolution theorem is the converse of the deduction theorem. It follows immediately from modus ponens which is the elimination rule for implication.

See also

• Conditional proof
• Propositional calculus
• Peirce's law

References

• Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks Podnieks is a comprehensive tutorial. See Section 1.5.de:Deduktionstheorem

it:Teorema di deduzione