substitution theorem for propositional logic

In this entry, we will prove the substitution theorem for propositional logic based on the axiom system found here ( Besides the deduction theoremMathworldPlanetmath, below are some additional results we will need to prove the theorem:

  1. 1.

    If ΔAB and ΓBC, then Δ,ΓAC.

  2. 2.

    ΔA and ΔB iff ΔAB.

  3. 3.


  4. 4.

    A¬¬A (law of double negation).

  5. 5.

    A (ex falso quodlibet)

  6. 6.

    ΔA implies ΔB iff ΔAB.

The proofs of these results can be found here (

Theorem 1.

(Substitution Theorem) Suppose p1,,pm are all the propositional variables, not necessarily distinct, that occur in order in A, and if B1,,Bm,C1,,Cm are wff’s such that BiCi, then


where A[X1/p1,,Xm/pm] is the wff obtained from A by replacing pi by the wff Xi via simultaneous substitution.


We do inductionMathworldPlanetmath on the number n of in wff A.

If n=0, A is either a propositional variable, say p, or , which respectively means that A[B/p]A[C/p] is either BC or . The former is the assumptionPlanetmathPlanetmath and the latter is a theorem.

Suppose now A has n+1 occurrences of . We may write A as XY uniquely by unique readability. Also, both X and Y have at most n occurrences of .

Let A1 be A[B1/p1,,Bm/pm] and A2 be A[C1/p1,,Cm/pm]. Then A1 is X1Y1 and X2Y2, where X1 is X[B1/p1,,Bk/pk], Y1 is Y[Bk+1/pk+1,,Bm/pm], X2 is X[C1/p1,,Ck/pk], and Y2 is Y[Ck+1/pk+1,,Cm/pm].


by induction X1X2 (1)
by 2 above X1X2 and X2X1 (2)
by induction Y1Y2 (3)
by 2 above Y1Y2 and Y2Y1 (4)
since A1 is X1Y1 A1X1Y1 (5)
by applying 1 to X2X1 and (5) A1X2Y1 (6)
by applying 1 to (6) and Y1Y2 A1X2Y2 (7)
by the deduction theorem A1A2 (8)
by a similar reasoning as above A2A1 (9)
by applying 2 to (8) and (9) A1A2 (10)

As a corollary, we have

Corollary 1.

If BC, then A[B/s(p)]A[C/s(p)], where p is a propositional variable that occurs in A, s(p) is a set of positions of occurrences of p in A, and the wff A[X/s(p)] is obtained by replacing all p that occur in the positions in s(p) in A by wff X.


For any propositional variable q not being replaced, use the corresponding theorem qq, and then apply the substitution theorem. ∎

Remark. What about B[A/p]C[A/p], given BC? Here, B[A/p] and C[A/p] are wff’s obtained by uniform substitution of p (all occurrences of p) in B and C respectively. Since B[A/p]C[A/p] is just (BC)[A/p], an instance of the schema BC by assumption, the result follows directly if we assume BC is a theorem schema.

Using the substitution theorem, we can easily derive more theorem schemas, such as

  1. 7.

    (AB)(¬B¬A) (Law of Contraposition)

  2. 8.


  3. 9.

    ((AB)A)A (Peirce’s Law)

  1. 7.

    Since (¬B¬A)(AB) is already a theorem schema, we only need to show (AB)(¬B¬A). By law of double negation (4 above) and the substitution theorem, it is enough to show that (¬¬A¬¬B)(¬B¬A). But this is just an instance of an axiom schemaMathworldPlanetmath. Combining the two schemas, we get (AB)(¬B¬A).

  2. 8.

    First, observe that A,ABB by modus ponensMathworldPlanetmath. Since B¬¬B, we have A,AB¬¬B by the substitution theorem. So A,AB,¬B by the deduction theorem, and A,¬B(AB) by the deduction theorem again. Apply the deduction two more times, we get A(¬B¬(AB)).

  3. 9.

    To show ((AB)A)A, it is enough to show ¬A¬((AB)A) by 7 and modus ponens, or ¬A¬((AB)A) by the deduction theorem. Now, since XY¬(X¬Y) (as they are the same thing, and because CC is a theorem schema), by the law of double negation and the substitution theorem, X¬Y¬(XY), and we have (AB)¬A¬((AB)A). So to show ¬A¬((AB)A), it is enough to show ¬A(AB)¬A, which is enough to show that ¬AAB and ¬A¬A, according to a meta-theorem found here ( To show ¬AAB, it is enough to show {¬A,A}B, and A,¬A,,B,B is such a deduction. The second statement ¬A¬A is clear.

As an application, we prove the following useful meta-theorems of propositional logicPlanetmathPlanetmath:

Proposition 1.

There is a wff A such that ΔA and Δ¬A iff Δ


Assume the former. Let 1 be a deduction of A from Δ and 2 a deduction of ¬A from Δ, then


is a deduction of from Δ. Conversely, assume the later. Pick any wff A (if necessary, pick ). Then A by ex falso quodlibet. By modus ponens, we have ΔA. Similarly, Δ¬A. ∎

Proposition 2.

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


By assumption, we have ΔAB and Δ¬AB. Using modus ponens and the theorem schema (AB)(¬B¬A), we have Δ¬B¬A, or


Similarly, Δ¬B¬¬A. By the law of double negation and the substitution theorem, we have Δ¬BA, or


By the previous proposition, Δ,¬B, or Δ¬¬B. Applying the substitution theorem and the law of double negation, we have


Title substitution theorem for propositional logic
Canonical name SubstitutionTheoremForPropositionalLogic
Date of creation 2013-03-22 19:33:08
Last modified on 2013-03-22 19:33:08
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 17
Author CWoo (3771)
Entry type Result
Classification msc 03B05
Related topic AxiomSystemForPropositionalLogic
Defines substitution theorem