axiom system for propositional logic

The languagePlanetmathPlanetmath of (classical) propositional logicPlanetmathPlanetmath PLc consists of a set of propositional letters or variablesMathworldPlanetmath, the symbol (for falsity), together with two symbols for logical connectives ¬ and . The well-formed formulas (wff’s) of PLc are inductively defined as follows:

  • each propositional letter is a wff

  • is a wff

  • if A and B are wff’s, then AB is a wff

We also use parentheses ( and ) to remove ambiguities. The other familiar logical connectives may be defined in terms of : ¬A is A, AB is the abbreviation for ¬AB, AB is the abbreviation for ¬(A¬B), and AB is the abbreviation for (AB)(BA).

The axiom system for PLc consists of sets of wffs called axiom schemasMathworldPlanetmath together with a rule of inferenceMathworldPlanetmath. The axiom schemas are:

  1. 1.


  2. 2.


  3. 3.


and the rule of inference is modus ponensMathworldPlanetmath (MP): from AB and A, we may infer B.

A deductionMathworldPlanetmathPlanetmath is a finite sequencePlanetmathPlanetmath of wff’s A1,,An such that each Ai is either an instance of one of the axiom schemas above, or as a result of applying rule MP to earlier wff’s in the sequence. In other words, there are j,k<i such that Ak is the wff AjAi. The last wff An in the deduction is called a theoremMathworldPlanetmath of PLc. When A is a theorem of PLc, we write

cA    or simply    A.

For example, AA, whose deduction is

  1. 1.

    (A((BA)A))((A(BA))(AA)) by Axiom II,

  2. 2.

    A((BA)A) by Axiom I,

  3. 3.

    (A(BA))(AA) by modus ponens on 2 to 1,

  4. 4.

    A(BA) by Axiom I,

  5. 5.

    AA by modus ponens on 4 to 3.

More generally, given a set Σ of wff’s, we write


if there is a finite sequence of wff’s such that each wff is either an axiom, a member of Σ, or as a result of applying MP to earlier wff’s in the sequence. An important (meta-)theorem called the deduction theoremMathworldPlanetmath, states: if Σ,AB, then ΣAB. The deduction theorem holds for PLc (proof here (

Remark. The axiom system above was first introduced by Polish logician Jan Łukasiewicz. Two axiom systems are said to be deductively equivalent if every theorem in one system is also a theorem in the other system. There are many axiom systems for PLc that are deductively equivalent to Łukasiewicz’s system. One such system consists of the first two axiom schemas above, but the third axiom schema is ¬¬AA, with MP its sole inference rule.

Title axiom system for propositional logic
Canonical name AxiomSystemForPropositionalLogic
Date of creation 2013-03-22 19:31:50
Last modified on 2013-03-22 19:31:50
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 13
Author CWoo (3771)
Entry type Definition
Classification msc 03B05
Synonym axiom system for classical propositional logic
Related topic DeductionTheoremHoldsForClassicalPropositionalLogic
Related topic SubstitutionTheoremForPropositionalLogic