natural deduction for intuitionistic propositional logic

The natural deduction system for intuitionistic propositional logicPlanetmathPlanetmath described here is based on the languagePlanetmathPlanetmath that consists of a set of propositional variables, a symbol for falsity, and logical connectives , , . In this system, there are no axioms, only rules of inferenceMathworldPlanetmath.

  1. 1.

    for , there are three rules, one introduction rule I, and two elimination rules EL and ER:

    A B   A B (I)        A B   A (EL)        A B   B (ER)
  2. 2.

    for , there are two rules, one introduction I and one elimination E (modus ponensMathworldPlanetmath):

    [ A ] . . . . B   A B (I)        A A B   B (E)
  3. 3.

    for , there are three rules, two introduction rules IE, IL, and one elimination rule E:

    A   A B (IL)        B   A B (IR)        A B [ A ] . . . . C [ B ] . . . . C   C (E)
  4. 4.

    for , there is one rule, an introduction rule I (ex falso quodlibet):

      A (I)

In short, intuitionistic propositional logic is classical propositional logic without the rule RAA (reductio ad absurdumMathworldPlanetmathPlanetmath). Furthermore, ¬ is a defined one-place logical symbol: ¬A:=A.

Remark. In the rules I and E, the square brackets around the top formulaMathworldPlanetmathPlanetmath denote that the formula is removed, or discharged. In other words,

“once the conclusionMathworldPlanetmath is reached, the assumptionPlanetmathPlanetmath can be dropped.”

In I, when the formula B is deduced from the assumption or hypothesisMathworldPlanetmath A, we conclude with the formula AB. Once this conclusion is reached, A is superfluous and therefore removed, as it is embodied in the formula AB. This is often encountered in mathematical proofs: if we want to prove AB, we first assume A, then we proceed with the proof and reach B, and therefore AB. Simiarly, in E, if C can be concluded from A and from B individually, then C can be concluded from anyone of them, or AB, without the assumptions A and B individually.

Intuitionistic propositional logic as defined by the natural deduction system above is termed NJ. Derivations and theoremsMathworldPlanetmath for NJ are defined in the usual manner like all natural deduction systems, which can be found here ( Some of the theorems of NJ are listed below:

  • A(BA)

  • (A(BC))((AB)(AC))

  • (AB)(¬B¬A)

  • ABBA

  • ¬(A¬A)

  • A¬¬A

  • ¬¬¬A¬A

For example, A¬¬A as

  [A]2         [¬A]1   (E)                                        (I)1                  ¬A              (I)2              A(¬A)

and A(¬A) is just A¬¬A. Also, ¬¬¬A¬A, as

  [A]1          A→¬¬A   (E)                    ¬¬A        [¬¬¬A]2                    (E)                                                                                                                                                                                                             (I)1                                                                                                      ¬A                                                                                                (I)2                                                                                                ¬¬¬A¬A

The subscripts indicate that the discharging of the assumptions at the top correspond to the applications of the inference rules I at the bottom. The box around A¬¬A indicates that the derivation of A¬¬A has been embedded (as a subtree) into the derivation of ¬¬¬A¬A.

Remark. If ¬ were introduced as a primitive logical symbol instead of it being as “defined”, then we need to have inference rules for ¬ as well, one of which is introduction ¬I, and the other elimination ¬E:

[ A ] . . . .   ¬ A (¬I)        A ¬ A   (¬E)

Note that in the original NJ system, ¬I is just an instance of I, and ¬E is just an instance of E.

Title natural deduction for intuitionistic propositional logic
Canonical name NaturalDeductionForIntuitionisticPropositionalLogic
Date of creation 2013-03-22 19:32:11
Last modified on 2013-03-22 19:32:11
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 25
Author CWoo (3771)
Entry type Definition
Classification msc 03B20
Classification msc 03F03
Classification msc 03F55
Related topic DisjunctionProperty