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.

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 (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

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 (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
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