substitution theorem for propositional logic

In this entry, we will prove the substitution theorem for propositional logic based on the axiom system found here (http://planetmath.org/AxiomSystemForPropositionalLogic). Besides the deduction theorem, below are some additional results we will need to prove the theorem:

1. 1.

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

2. 2.

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

3. 3.

$\vdash A\leftrightarrow A$.

4. 4.

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

5. 5.

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

6. 6.

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

The proofs of these results can be found here (http://planetmath.org/SomeTheoremSchemasOfPropositionalLogic).

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.

We do induction on the number $n$ of $\to$ in wff $A$.

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

1. 7.

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

2. 8.

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

3. 9.

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

Proof.
1. 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)$.

2. 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))$.

3. 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 (http://planetmath.org/SomeTheoremSchemasOfPropositionalLogic). 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.$

Title substitution theorem for propositional logic SubstitutionTheoremForPropositionalLogic 2013-03-22 19:33:08 2013-03-22 19:33:08 CWoo (3771) CWoo (3771) 17 CWoo (3771) Result msc 03B05 AxiomSystemForPropositionalLogic substitution theorem