some meta-theorems of propositional logic

Based on the axiom system in this entry (, we will prove some meta-theorems of propositional logicPlanetmathPlanetmath. In the discussion below, Δ and Γ are sets of well-formed formulas (wff’s), and A,B,C, are wff’s.

  1. 1.

    (Deduction TheoremMathworldPlanetmath) Δ,AB iff ΔAB.

  2. 2.

    (Proof by ContradictionMathworldPlanetmathPlanetmath) Δ,A iff Δ¬A.

  3. 3.

    (Proof by Contrapositive) Δ,A¬B iff Δ,B¬A.

  4. 4.

    (Law of Syllogism) If ΔAB and ΓBC, then Δ,ΓAC.

  5. 5.

    ΔA and ΔB iff ΔAB.

  6. 6.

    ΔAB iff Δ,AB and Δ,BA.

  7. 7.

    If ΔAB, then ΔBA.

  8. 8.

    If ΔAB and ΔBC, then ΔAC.

  9. 9.

    ΔABC iff ΔA(BC).

  10. 10.

    ΔA implies ΔB iff ΔAB. This is a useful restatement of the deduction theorem.

  11. 11.

    (Substitution Theorem) If BiCi, then A[B¯/p¯]A[C¯/p¯].

  12. 12.

    Δ iff there is a wff A such that ΔA and Δ¬A.

  13. 13.

    If Δ,AB and Δ,¬AB, then ΔB.

Remark. The theorem schema A¬¬A is used in the proofs below.


The first three are proved here (, and the last three are proved here ( We will prove the rest here, some of which relies on the deduction theorem.

  1. 4.

    From ΔAB, by the deduction theorem, we have Δ,AB. Let 1 be a deductionMathworldPlanetmathPlanetmath of B from Δ{A}, and 2 be a deduction of BC from Γ, then


    is a deduction of C from Δ{A}Γ, so Δ,A,ΓC, and by the deduction theorem again, we get Δ,ΓAC.

  2. 5.

    (). Since AB is ¬(A¬B), by the deduction theorem, it is enough to show Δ,A¬B. Suppose 1 is a deduction of A from Δ and 2 is a deduction of B from Δ, then


    is a deduction of from Δ{A¬B}.

    (). We first show that ΔB. Now, ¬B(A¬B) is an axiom and (A¬B)¬¬(A¬B) is a theorem, ¬B¬¬(A¬B), so that by modus ponensMathworldPlanetmath, ¬(A¬B)B, using axiom schemaMathworldPlanetmath (¬C¬D)(DC). Since by assumption Δ¬(A¬B), by modus ponens again, we get ΔB.

    We next show that ΔA. From the deduction A,A,, we have A,¬A, so certainly Δ,¬A,A,B. By three applications of the deduction theorem, we get Δ¬A(A¬B). By theorem (A¬B)¬¬(A¬B), Δ¬A¬¬(A¬B). By axiom schema (¬C¬D)(DC) and modus ponens, we get Δ¬(A¬B)A. Since Δ¬A¬B by assumption, ΔA as a result.

  3. 6.

    ΔAB iff ΔAB and ΔBA iff Δ,AB and Δ,BA.

  4. 7.

    Apply 6 to ΔAB and ΔBA.

  5. 8.

    Apply 5 and 6.

  6. 9.

    Since Δ,ABAB by the theorem schema A(BAB), together with ΔABC, we have Δ,ABC by law of syllogism, or equivalently ΔA(BC), by the deduction theorem. Conversely, Δ,ABC and theorem schema ABB result in Δ,AABC by law of syllogism. So ΔA(ABC) by the deduction theorem. But ABA is a theorem schema, ΔAB(ABC), and therefore ΔABC by the theorem schema (X(XY))(XY).

  7. 10.

    Assume the former. Then a deduction of B from Δ may or may not contain A. In either case, Δ,AB, so ΔAB by the deduction theorem. Next, assume the later. Let 1 be a deduction of AB from Δ. Then if 2 is a deduction of A from Δ, then 1,2,B is a deduction of B from Δ, and therefore ΔB.

To see the last meta-theorem implies the deduction theorem, assume Δ,AB. Suppose ΔA. Let 1 be a deduction of A from Δ, and 2 a deduction of B from Δ{A}. Then 1,2 is a deduction of B from Δ. So ΔB. As a result ΔAB by the statement of the meta-theorem. ∎

Remark. Meta-theorems 7 and 8, together with the theorem schema AA, show that defines an equivalence relationMathworldPlanetmath on the set of all wff’s of propositional logic. Formally, for any two wff’s A,B, if we define AB iff AB, then is an equivalence relation.

Title some meta-theorems of propositional logic
Canonical name SomeMetatheoremsOfPropositionalLogic
Date of creation 2013-03-22 19:34:29
Last modified on 2013-03-22 19:34:29
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 10
Author CWoo (3771)
Entry type Result
Classification msc 03B05
Defines law of syllogism