some theorem schemas of propositional logic

Based on the axiom system in this entry (, we will exhibit some theorem schemas, as well as prove some meta-theorems of propositional logicPlanetmathPlanetmath. All of these are based on the important deduction theoremMathworldPlanetmath, which is proved here (

First, some theorem schemas:

  1. 1.


  2. 2.


  3. 3.

    (law of the excluded middle) A¬A

  4. 4.

    (ex falso quodlibet) A

  5. 5.


  6. 6.

    (law of double negation) A¬¬A

  7. 7.

    ABA and ABB

  8. 8.

    (absorption law for ) AAA

  9. 9.

    (commutative law for ) ABBA

  10. 10.

    (associative law for ) (AB)CA(BC)

  11. 11.

    (law of syllogism) (AB)((BC)(AC))

  12. 12.

    (law of importation) (A(BC))(ABC)

  13. 13.


  14. 14.



Many of these can be easily proved using the deduction theorem:

  1. 1.

    we need to show A¬¬A, which means we need to show A,¬A. Since ¬A is A, by modus ponensMathworldPlanetmath, A,¬A.

  2. 2.

    we observe first that ¬A¬¬¬A is an instance of the above theorem schema, since (¬A¬¬¬A)(¬¬AA) is an instance of one of the axiom schemasMathworldPlanetmath, we have ¬¬AA as a result.

  3. 3.

    since A¬A is ¬A¬A, to show A¬A, we need to show ¬A¬A, but this is obvious.

  4. 4.

    we need to show A. Since ,(A),A is a deductionMathworldPlanetmathPlanetmath of A from , and the result follows.

  5. 5.

    this is because AA, so (AA)(AA).

  6. 6.

    this is the result of the first two theorem schemas above.

For the next four schemas, we need the the following meta-theorems (see here ( for proofs):

  1. M1.

    ΔA and ΔB iff ΔAB

  2. M2.

    ΔA implies ΔB iff ΔAB

  1. 7.

    If AB, then A by M1, so ABA by M2. Similarly, ABB.

  2. 8.

    AAA comes from 7, and since A implies AA by M1, AAA by M2. Therefore, AAA by M1.

  3. 9.

    If AB, then A and B by M1, so BA by M1 again, and therefore ABBA by M2. Similarly, BAAB. Combining the two and apply M1, we have the result.

  4. 10.

    If (AB)C, then AB and C, so A, B, and C by M1. By M1 again, we have A and BC, and another application of M1, A(BC). Therefore, by M2, (AB)CA(BC), Similarly, A(BC)(AB)C. Combining the two and applying M1, we have the result.

  5. 11.

    AB,BC,AC by modus ponens 3 times.

  6. 12.

    A(BC),AB,ABA,A,BC,ABB,B,C is a deduction of C from A(BC) and AB.

  7. 13.

    AB,B(CD),AC,ACA,A,B,CD,ACC,C,D is a deduction of D from AB,B(CD), and AC.

  8. 14.

    (AB)(A(AB)) is just an axiom, while (A(AB))(AB) comes from two applications of the deduction theorem to A(AB),AB, which is the result of the deduction A(AB),A,AB,B of B from A(AB) and A.

Title some theorem schemas of propositional logic
Canonical name SomeTheoremSchemasOfPropositionalLogic
Date of creation 2013-03-22 19:33:04
Last modified on 2013-03-22 19:33:04
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 40
Author CWoo (3771)
Entry type Result
Classification msc 03B05
Defines law of double negation
Defines law of the excluded middle
Defines ex falso quodlibet