deduction theorem holds for classical propositional logic


In this entry, we prove that the deduction theorem holds for classical propositional logic. For the logic, we use the axiom system found in this entry (http://planetmath.org/AxiomSystemForPropositionalLogic). To prove the theorem, we use the theorem schema AA (whose deductionMathworldPlanetmathPlanetmath can be found here (http://planetmath.org/AxiomSystemForPropositionalLogic)).

Proof.

Suppose A1,,An is a deduction of B from Δ{A}. We want to find a deduction of AB from Δ. There are two main cases to consider:

  • If B is an axiom or in Δ{A}, then

    B,B(AB),AB

    is a deduction of AB from Δ, where AB is obtained by modus ponensMathworldPlanetmath applied to B and the axiom B(AB). So ΔAB.

  • If B is obtained from Ai and Aj by modus ponens. Then Aj, say, is AiB. We use inductionMathworldPlanetmath on the length n of the deduction of B. Note that n3. If n=3, then the first two formulasMathworldPlanetmathPlanetmath are C and CB.

    • If C is A, then CB is either an axiom or in Δ. So AB, which is just CB, is a deduction of AB from Δ.

    • If CB is A, then C is either an axiom or in Δ, and

      0,(AA)((AC)(AB)),C(AC),C,AC,AB

      is a deduction of AB from Δ, where 0 is a deduction of AA, followed by two axiom instances, followed by C, followed by results of two applications of modus ponens.

    • If both C and CB are either axioms are in Δ, then

      C,CB,B,B(AB),AB

      is a deduction of AB from Δ.

    Next, assume the deduction of B has length n>3. A subsequence of is a deduction of AiB from Δ{A}. This deduction has length less than n, so by induction,

    ΔA(AiB),

    and therefore by (A(AiB))((AAi)(AB)), an axiom instance, and modus ponens,

    Δ(AAi)(AB).

    Likewise, a subsequence of is a deduction of Ai, so by induction, ΔAAi. Therefore, an application of modus ponens gives us ΔAB.

In both cases, ΔAB and we are done. ∎

We record two corollaries:

Corollary 1.

(Proof by ContradictionMathworldPlanetmath). If Δ,A, then Δ¬A.

Proof.

From Δ,A, we have ΔA by the deduction theoremMathworldPlanetmath. Since ¬A, the result follows. ∎

Corollary 2.

(Proof by Contrapositive). If Δ,A¬B, then Δ,B¬A.

Proof.

If Δ,A¬B, then Δ,A,B by the deduction thereom, and therefore Δ,B¬A by the deduction theorem again. ∎

Remark The deduction theorem for the classical propositional logicPlanetmathPlanetmath can be used to prove the deduction theorem for the classical first and second orderPlanetmathPlanetmath predicate logic.

References

  • 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
Title deduction theorem holds for classical propositional logic
Canonical name DeductionTheoremHoldsForClassicalPropositionalLogic
Date of creation 2013-03-22 19:13:42
Last modified on 2013-03-22 19:13:42
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 23
Author CWoo (3771)
Entry type Theorem
Classification msc 03F03
Classification msc 03B99
Classification msc 03B22
Related topic AxiomSystemForPropositionalLogic
Defines proof by contradiction
Defines proof by contrapositive