## You are here

Homesubstitution theorem for propositional logic

## Primary tabs

# 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 theorem, below are some additional results we will need to prove the theorem:

1. If $\Delta\vdash A\to B$ and $\Gamma\vdash B\to C$, then $\Delta,\Gamma\vdash A\to C$.

2. $\Delta\vdash A$ and $\Delta\vdash B$ iff $\Delta\vdash A\land B$.

3. $\vdash A\leftrightarrow A$.

4. $\vdash A\leftrightarrow\neg\neg A$ (law of double negation).

5. $\perp\to A$ (ex falso quodlibet)

6. $\Delta\vdash A$ implies $\Delta\vdash B$ iff $\Delta\vdash A\to B$.

The proofs of these results can be found here.

###### Theorem 1.

(Substitution Theorem) Suppose $p_{1},\ldots,p_{m}$ are all the propositional variables, not necessarily distinct, that occur in order in $A$, and if $B_{1},\ldots,B_{m},C_{1},\ldots,C_{m}$ are wff’s such that $\vdash B_{i}\leftrightarrow C_{i}$, then

$\vdash A[B_{1}/p_{1},\ldots,B_{m}/p_{m}]\leftrightarrow A[C_{1}/p_{1},\ldots,C% _{m}/p_{m}]$ |

where $A[X_{1}/p_{1},\ldots,X_{m}/p_{m}]$ is the wff obtained from $A$ by replacing $p_{i}$ by the wff $X_{i}$ via simultaneous substitution.

###### Proof.

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

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

Let $A_{1}$ be $A[B_{1}/p_{1},\ldots,B_{m}/p_{m}]$ and $A_{2}$ be $A[C_{1}/p_{1},\ldots,C_{m}/p_{m}]$. Then $A_{1}$ is $X_{1}\to Y_{1}$ and $X_{2}\to Y_{2}$, where $X_{1}$ is $X[B_{1}/p_{1},\ldots,B_{k}/p_{k}]$, $Y_{1}$ is $Y[B_{{k+1}}/p_{{k+1}},\ldots,B_{m}/p_{m}]$, $X_{2}$ is $X[C_{1}/p_{1},\ldots,C_{k}/p_{k}]$, and $Y_{2}$ is $Y[C_{{k+1}}/p_{{k+1}},\ldots,C_{m}/p_{m}]$.

Then

by induction | $\displaystyle\vdash X_{1}\leftrightarrow X_{2}$ | (1) | |||

by 2 above | $\displaystyle\vdash X_{1}\to X_{2}\mbox{ and }\vdash X_{2}\to X_{1}$ | (2) | |||

by induction | $\displaystyle\vdash Y_{1}\leftrightarrow Y_{2}$ | (3) | |||

by 2 above | $\displaystyle\vdash Y_{1}\to Y_{2}\mbox{ and }\vdash Y_{2}\to Y_{1}$ | (4) | |||

$\displaystyle\mbox{since }A_{1}\mbox{ is }X_{1}\to Y_{1}$ | $\displaystyle A_{1}\vdash X_{1}\to Y_{1}$ | (5) | |||

$\displaystyle\mbox{by applying 1 to }\vdash X_{2}\to X_{1}\mbox{ and }(5)$ | $\displaystyle A_{1}\vdash X_{2}\to Y_{1}$ | (6) | |||

$\displaystyle\mbox{by applying 1 to }(6)\mbox{ and }\vdash Y_{1}\to Y_{2}$ | $\displaystyle A_{1}\vdash X_{2}\to Y_{2}$ | (7) | |||

by the deduction theorem | $\displaystyle\vdash A_{1}\to A_{2}$ | (8) | |||

by a similar reasoning as above | $\displaystyle\vdash A_{2}\to A_{1}$ | (9) | |||

$\displaystyle\mbox{by applying 2 to }(8)\mbox{ and }(9)$ | $\displaystyle\vdash A_{1}\leftrightarrow A_{2}$ | (10) |

∎

As a corollary, we have

###### Corollary 1.

If $\vdash B\leftrightarrow C$, then $\vdash A[B/s(p)]\leftrightarrow 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$.

###### Proof.

For any propositional variable $q$ not being replaced, use the corresponding theorem $\vdash q\leftrightarrow q$, and then apply the substitution theorem. ∎

Remark. What about $\vdash B[A/p]\leftrightarrow C[A/p]$, given $\vdash B\leftrightarrow C$? 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]\leftrightarrow C[A/p]$ is just $(B\leftrightarrow C)[A/p]$, an instance of the schema $B\leftrightarrow C$ by assumption, the result follows directly if we assume $B\leftrightarrow C$ is a theorem schema.

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

7. $(A\to B)\leftrightarrow(\neg B\to\neg A)$ (Law of Contraposition)

8. $A\to(\neg B\to\neg(A\to B))$

9. $((A\to B)\to A)\to A$ (Peirce’s Law)

###### Proof.

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

8. First, observe that $A,A\to B\vdash B$ by modus ponens. Since $\vdash B\leftrightarrow\neg\neg B$, we have $A,A\to B\vdash\neg\neg B$ by the substitution theorem. So $A,A\to B,\neg B\vdash\perp$ by the deduction theorem, and $A,\neg B\vdash(A\to B)\to\perp$ by the deduction theorem again. Apply the deduction two more times, we get $\vdash A\to(\neg B\to\neg(A\to B))$.

9. To show $\vdash((A\to B)\to A)\to A$, it is enough to show $\vdash\neg A\to\neg((A\to B)\to A)$ by $7$ and modus ponens, or $\neg A\vdash\neg((A\to B)\to A)$ by the deduction theorem. Now, since $\vdash X\land Y\leftrightarrow\neg(X\to\neg Y)$ (as they are the same thing, and because $C\leftrightarrow C$ is a theorem schema), by the law of double negation and the substitution theorem, $\vdash X\land\neg Y\leftrightarrow\neg(X\to Y)$, and we have $\vdash(A\to B)\land\neg A\leftrightarrow\neg((A\to B)\to A)$. So to show $\neg A\vdash\neg((A\to B)\to A)$, it is enough to show $\neg A\vdash(A\to B)\land\neg A$, which is enough to show that $\neg A\vdash A\to B$ and $\neg A\vdash\neg A$, according to a meta-theorem found here. To show $\neg A\vdash A\to B$, it is enough to show $\{\neg A,A\}\vdash B$, and $A,\neg A,\perp,\perp\to B,B$ is such a deduction. The second statement $\neg A\vdash\neg A$ is clear.

∎

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

###### Proposition 1.

There is a wff $A$ such that $\Delta\vdash A$ and $\Delta\vdash\neg A$ iff $\Delta\vdash\perp$

###### Proof.

Assume the former. Let $\mathcal{E}_{1}$ be a deduction of $A$ from $\Delta$ and $\mathcal{E}_{2}$ a deduction of $\neg A$ from $\Delta$, then

$\mathcal{E}_{1},\mathcal{E}_{2},\perp$ |

is a deduction of $\perp$ from $\Delta$. Conversely, assume the later. Pick any wff $A$ (if necessary, pick $\perp$). Then $\perp\to A$ by ex falso quodlibet. By modus ponens, we have $\Delta\vdash A$. Similarly, $\Delta\vdash\neg A$. ∎

###### Proposition 2.

If $\Delta,A\vdash B$ and $\Delta,\neg A\vdash B$, then $\Delta\vdash B$

###### Proof.

By assumption, we have $\Delta\vdash A\to B$ and $\Delta\vdash\neg A\to B$. Using modus ponens and the theorem schema $(A\to B)\to(\neg B\to\neg A)$, we have $\Delta\vdash\neg B\to\neg A$, or

$\Delta,\neg B\vdash\neg A.$ |

Similarly, $\Delta\vdash\neg B\to\neg\neg A$. By the law of double negation and the substitution theorem, we have $\Delta\vdash\neg B\to A$, or

$\Delta,\neg B\vdash A.$ |

By the previous proposition, $\Delta,\neg B\vdash\perp$, or $\Delta\vdash\neg\neg B$. Applying the substitution theorem and the law of double negation, we have

$\Delta\vdash B.$ |

∎

## Mathematics Subject Classification

03B05*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections