deduction theorem holds for intuitionistic propositional logic

In this entry, we show that the deduction theoremMathworldPlanetmath below holds for intuitionistic propositional logicPlanetmathPlanetmath. We use the axiom system provided in this entry (

Theorem 1.

If Δ,AiB, where Δ is a set of wff’s of the intuitionistic propositional logic, then ΔiAB.

The proof is very similar to that of the classical propositional logic, given here (, in that it uses inductionMathworldPlanetmath on the length of the deductionMathworldPlanetmathPlanetmath of B. In fact, the proof is simpler as only two axiom schemasMathworldPlanetmath are used: A(BA) and (AB)((A(BC))(AC)).


There are two main cases to consider:

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


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

  • Now, suppose that


    is a deduction of B from Δ{A}, with B obtained from earlier formulasMathworldPlanetmathPlanetmath by modus ponens.

    We use induction on the length n of deduction of B. Note that n3. If n=3, then C and CB are either axioms or in Δ{A}.

    • If C is A, then CB is either an axiom or in Δ. So ΔiAB.

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


      is a deduction of AB from Δ, where 0 is a deduction of the theoremMathworldPlanetmath AA, followed by an axiom instance, then C, then the result of modus ponens, then an axiom instance, and finally two applications of modus ponens. Note the second to the last formula is just (AA)(AB).

    • If C and CB are axioms or in Δ, then ΔiAB based on the deduction C,CB,B,B(AB),AB.

    Next, assume there is a deduction of B of length n>3. So one of the earlier formulas is AkB, and a subsequenceMathworldPlanetmath of is a deduction of AkB, which has length less than n, and therefore by induction, ΔiA(AkB). Likewise, a subsequence of is a deduction of Ak, so by induction, ΔiAAk. With the axiom instance (AAk)((A(AkB))(AB)), and two applications of modus ponens, we get ΔiAB as required.

In both cases, ΔiAB, and the proof is completePlanetmathPlanetmathPlanetmathPlanetmath. ∎

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


  • 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
Title deduction theorem holds for intuitionistic propositional logic
Canonical name DeductionTheoremHoldsForIntuitionisticPropositionalLogic
Date of creation 2013-03-22 19:31:32
Last modified on 2013-03-22 19:31:32
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 21
Author CWoo (3771)
Entry type Theorem
Classification msc 03F55
Classification msc 03B20
Related topic AxiomSystemForIntuitionisticLogic