natural deduction for propositional logic

The natural deduction system for classical propositional logicPlanetmathPlanetmath described here is based on the languagePlanetmathPlanetmath that consists of a set of propositional variables, a symbol for falsity, and two logical connectives and . The other connectives are defined as follows:

  • ¬A:=A,

  • AB:=¬(¬A¬B),

  • AB:=(AB)(BA).

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 two rules, one introduction I (ex falso quodlibet), and one RAA (reductio ad absurdumMathworldPlanetmathPlanetmath):

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

Remark. In the rules I and RAA, 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 RAA, to prove A, we start by assuming ¬A, and then reach a contradictionMathworldPlanetmathPlanetmath (), and hence we conclude with A. Of course, ¬A is no longer needed at this point.

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

  • A(BA)

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

  • (¬A¬B)(BA)

  • ABBA

  • ¬(A¬A)

  • A¬¬A

For example, ¬(A¬A) as

  [A¬A]1   (EL)          A         [A¬A]1   (ER)         ¬A          (E)                                                                                                            (I)1                                                  (A¬A)

is a derivation of (A¬A), which is ¬(A¬A), where all of the assumptions have been discharged. The subscript indicates that the discharging of the assumptions at the top correspond to the application of the inference rule I at the bottom.

Note also that the first three theorems are the axiom schemasMathworldPlanetmath for the Łukasiewicz’s axiom system for propositional logic, and it is easy to see that NK and the axiom system are in fact deductively equivalent: the theorems in both systems are precisely the same. In additionPlanetmathPlanetmath to the theorems above, we also have the following meta-theorems:

  1. 1.


  2. 2.

    if Σ{A}, then Σ¬A,

  3. 3.

    AAB and BAB,

  4. 4.

    if Σ{A}C and Σ{B}C, then Σ{AB}C.

Remark. If ¬ and were introduced as primitive logical symbols instead of them as being “defined”, then we need to have inference rules for ¬ and as well:

  1. 1.

    for ¬, there are two rules, one introduction ¬I and one elimination ¬E:

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

    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)

Note that the inference rules correspond to the meta-theorems above: rule ¬E corresponds to meta-theorem 1, ¬I corresponds to 2, IL and IR correspond to 3, and E to 4. The resulting system is deductively equivalent to original NK system.

Title natural deduction for propositional logic
Canonical name NaturalDeductionForPropositionalLogic
Date of creation 2013-03-22 19:31:59
Last modified on 2013-03-22 19:31:59
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 25
Author CWoo (3771)
Entry type Definition
Classification msc 03F03
Classification msc 03B05
Synonym natural deduction for classical propositional logic
Defines NK