intuitionistic propositional logic is a subsystem of classical propositional logic

Suppose logical systems 1 and 2 share the same set L of well-formed formulas (wff’s). Let F1 be the set of all theoremsMathworldPlanetmath of 1, and F2 the set of all theorems of 2. We say that 1 is a subsystem of 2 if F1F2, and a proper subsystem if F1F2.

In the subsequent discussion, PLc stands for classical propositional logicPlanetmathPlanetmath, and PLi for intuitionistic propositional logic. We write PLi PLc to mean that PLi is a subsystem of PLc, or < if it is proper.

Proposition 1.

PL<i PLc.

Unless otherwise specified, A means the wff A is a theorem of PLc.

Before proving this, we need the following facts about PLc:

  1. 1.

    A and B iff AB.

  2. 2.

    A implies B iff AB.

  3. 3.


  4. 4.


  5. 5.

    if ΔA and Γ,AB, then Δ,ΓB.


The first two facts are proved, and the third is

Fact 4 is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to (AB)((¬AB)B) by the deduction theoremMathworldPlanetmath twice. Use the theorem schemas (AB)(¬B¬A) and A¬¬A (law of double negation), and the substitution theorem twice, it is enough to show


By the deduction theorem three times, it is enough to show ¬B¬A,¬BA,¬B, which is provided by the deductionMathworldPlanetmathPlanetmath ¬B¬A,¬BA,¬B,¬A,A,.

For the last fact, given deduction 1 of A from Δ, and deduction 2 of AB from Γ, 1,2,B is a deduction of B from ΔΓ. ∎


Since in both systems, the only inference rule is modus ponensMathworldPlanetmath, and theoremhood of wff’s is preserved by the inference rule (that is, if A and AB, then B), all we need to show is that every axiom of PLi is a theorem of PLc.

  1. 1.

    A(BA). This is just an axiom schemaMathworldPlanetmath for PLc.

  2. 2.


    A,B,A¬B,¬B, leads to A,B,A¬B. Applying the deduction theorem three times, we get A(B((A¬B))), or A(BAB).

  3. 3.

    ABA and ABB. See

  4. 4.


    A,¬A,,B,B results in A,¬AB, since B is a theorem. By applying the deduction theorem twice, we get A(¬AB), or AAB.

  5. 5.


    Clearly, B,¬AB. By the deduction theorem, B¬AB, or BAB. By the deduction theorem again, BAB.

  6. 6.


    By fact 3, AC,BC,¬AB¬AC. With fact 4: AC,¬ACC, so AC,BC,¬ABC by fact 5. Now apply the deduction theorem 3 times.

  7. 7.


    From AB,A(BC),A,BC,B,C, we get AB,A(BC),AC. Applying the deduction theorem three times, we have the result.

  8. 8.

    (AB)((A¬B)¬A). This is just 7, where C is .

  9. 9.


    From ¬A,A and B, we get ¬A,AB by fact 5, and the result follows with two applications of the deduction theorem.

Since A¬A is a theorem of PLc and not of PLi (see, we conclude that PLi is a proper subsystem of PLc. ∎


  1. 1.

    Strictly speaking, the languagePlanetmathPlanetmath Li of PLi under system is different from the language Lc of PLc under system. In Li, the logical connectives consist of , ¬, , , whereas in Lc, only is used. The other connectives are introduced as abbreviational devices: ¬A is A, AB is ¬AB, and AB is ¬(A¬B). So it doesn’t make much sense to say that PL<i PLc.

  2. 2.

    One way to get around this issue is to re-define what it means for one logical system to be a subsystem of another. For example, one can define a mapping τ:LiLc such that

    A mapping satisfying these conditions is called a translation. Then, a system PLi is a subsystem of PLc if there is a translation τ:LiLc such that

    • for any wff A in Li, we have iA implies cτ(A).

    To further require that PLi be a proper subsystem of PLc, we also need

    • there is an wff B in Li such that ⊬iB and cτ(B).

  3. 3.

    Using this definition, define τ:LiLc by

    τ(A):={Aif A is a propositional variableτ(B)τ(C)if A is BC¬τ(B)if A is ¬Bτ(B)τ(C)if A is BCτ(B)τ(C)if A is BC.

    where the symbols ¬, , and in Lc are used as abbreviational tools (see the first remark). Then we see that the proposition makes sense.

  4. 4.

    Another way of getting around this issue is to come up with another axiom system for PLc that uses , ¬, , and as primitive logical connectives. Such an axiom system exists. In fact, add ¬¬AA to the list of axiom schemas for PLi, and we get an axiom system for PLc.

  5. 5.

    Using the idea in 2 above further, it can be shown that PLc is a subsystem of PLi (under the right translation)! The existence of such a translation ν is known as the Glivenko’s theorem. This translation ν has the further property that for any wff A in Lc,

    cA  iff  iν(A).
Title intuitionistic propositional logic is a subsystem of classical propositional logic
Canonical name IntuitionisticPropositionalLogicIsASubsystemOfClassicalPropositionalLogic
Date of creation 2013-03-22 19:33:12
Last modified on 2013-03-22 19:33:12
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 31
Author CWoo (3771)
Entry type Result
Classification msc 03B20
Classification msc 03F55