some meta-theorems of propositional logic

Based on the axiom system in this entry (http://planetmath.org/AxiomSystemForPropositionalLogic), we will prove some meta-theorems of propositional logic. In the discussion below, $\Delta$ and $\Gamma$ are sets of well-formed formulas (wff’s), and $A,B,C,\ldots$ are wff’s.

1.

(Deduction Theorem) $\Delta,A\vdash B$ iff $\Delta\vdash A\to B$ .
2.

(Proof by Contradiction) $\Delta,A\vdash\perp$ iff $\Delta\vdash\neg A$ .
3.

(Proof by Contrapositive) $\Delta,A\vdash\neg B$ iff $\Delta,B\vdash\neg A$ .
4.

(Law of Syllogism) If $\Delta\vdash A\to B$ and $\Gamma\vdash B\to C$ , then $\Delta,\Gamma\vdash A\to C$ .
5.

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

$\Delta\vdash A\leftrightarrow B$ iff $\Delta,A\vdash B$ and $\Delta,B\vdash A$ .
7.

If $\Delta\vdash A\leftrightarrow B$ , then $\Delta\vdash B\leftrightarrow A$ .
8.

If $\Delta\vdash A\leftrightarrow B$ and $\Delta\vdash B\leftrightarrow C$ , then $\Delta\vdash A\leftrightarrow C$ .
9.

$\Delta\vdash A\land B\to C$ iff $\Delta\vdash A\to(B\to C)$ .
10.

$\Delta\vdash A$ implies $\Delta\vdash B$ iff $\Delta\vdash A\to B$ . This is a useful restatement of the deduction theorem.
11.

(Substitution Theorem) If $\vdash B_{i}\leftrightarrow C_{i}$ , then $\vdash A[\overline{B}/\overline{p}]\leftrightarrow A[\overline{C}/\overline{p}]$ .
12.

$\Delta\vdash\perp$ iff there is a wff $A$ such that $\Delta\vdash A$ and $\Delta\vdash\neg A$ .
13.

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

Remark. The theorem schema $A\to\neg\neg A$ is used in the proofs below.

Proof.

The first three are proved here (http://planetmath.org/DeductionTheoremHoldsForClassicalPropositionalLogic), and the last three are proved here (http://planetmath.org/SubstitutionTheoremForPropositionalLogic). We will prove the rest here, some of which relies on the deduction theorem.

4.

From $\Delta\vdash A\to B$ , by the deduction theorem, we have $\Delta,A\vdash B$ . Let $\mathcal{E}_{1}$ be a deduction of $B$ from $\Delta\cup\{A\}$ , and $\mathcal{E}_{2}$ be a deduction of $B\to C$ from $\Gamma$ , then

$\mathcal{E}_{1},\mathcal{E}_{2},C$

is a deduction of $C$ from $\Delta\cup\{A\}\cup\Gamma$ , so $\Delta,A,\Gamma\vdash C$ , and by the deduction theorem again, we get $\Delta,\Gamma\vdash A\to C$ .
5.

$(\Rightarrow)$ . Since $A\land B$ is $\neg(A\to\neg B)$ , by the deduction theorem, it is enough to show $\Delta,A\to\neg B\vdash\perp$ . Suppose $\mathcal{E}_{1}$ is a deduction of $A$ from $\Delta$ and $\mathcal{E}_{2}$ is a deduction of $B$ from $\Delta$ , then

$\mathcal{E}_{1},\mathcal{E}_{2},A\to\neg B,\neg B,\perp$

is a deduction of $\perp$ from $\Delta\cup\{A\to\neg B\}$ .

$(\Leftarrow)$ . We first show that $\Delta\vdash B$ . Now, $\neg B\to(A\to\neg B)$ is an axiom and $\vdash(A\to\neg B)\to\neg\neg(A\to\neg B)$ is a theorem, $\vdash\neg B\to\neg\neg(A\to\neg B)$ , so that by modus ponens, $\vdash\neg(A\to\neg B)\to B$ , using axiom schema $(\neg C\to\neg D)\to(D\to C)$ . Since by assumption $\Delta\vdash\neg(A\to\neg B)$ , by modus ponens again, we get $\Delta\vdash B$ .

We next show that $\Delta\vdash A$ . From the deduction $A,A\to\perp,\perp$ , we have $A,\neg A\vdash\perp$ , so certainly $\Delta,\neg A,A,B\vdash\perp$ . By three applications of the deduction theorem, we get $\Delta\vdash\neg A\to(A\to\neg B)$ . By theorem $(A\to\neg B)\to\neg\neg(A\to\neg B)$ , $\Delta\vdash\neg A\to\neg\neg(A\to\neg B)$ . By axiom schema $(\neg C\to\neg D)\to(D\to C)$ and modus ponens, we get $\Delta\vdash\neg(A\to\neg B)\to A$ . Since $\Delta\vdash\neg A\to\neg B$ by assumption, $\Delta\to A$ as a result.
6.

$\Delta\vdash A\leftrightarrow B$ iff $\Delta\vdash A\to B$ and $\Delta\vdash B\to A$ iff $\Delta,A\vdash B$ and $\Delta,B\vdash A$ .
7.

Apply 6 to $\Delta\vdash A\to B$ and $\Delta\vdash B\to A$ .
8.

Apply 5 and 6.
9.

Since $\Delta,A\vdash B\to A\land B$ by the theorem schema $\vdash A\to(B\to A\land B)$ , together with $\Delta\vdash A\land B\to C$ , we have $\Delta,A\vdash B\to C$ by law of syllogism, or equivalently $\Delta\vdash A\to(B\to C)$ , by the deduction theorem. Conversely, $\Delta,A\vdash B\to C$ and theorem schema $A\land B\to B$ result in $\Delta,A\vdash A\land B\to C$ by law of syllogism. So $\Delta\vdash A\to(A\land B\to C)$ by the deduction theorem. But $A\land B\to A$ is a theorem schema, $\Delta\vdash A\land B\to(A\land B\to C)$ , and therefore $\Delta\vdash A\land B\to C$ by the theorem schema $(X\to(X\to Y))\leftrightarrow(X\to Y)$ .
10.

Assume the former. Then a deduction of $B$ from $\Delta$ may or may not contain $A$ . In either case, $\Delta,A\vdash B$ , so $\Delta\vdash A\to B$ by the deduction theorem. Next, assume the later. Let $\mathcal{E}_{1}$ be a deduction of $A\to B$ from $\Delta$ . Then if $\mathcal{E}_{2}$ is a deduction of $A$ from $\Delta$ , then $\mathcal{E}_{1},\mathcal{E}_{2},B$ is a deduction of $B$ from $\Delta$ , and therefore $\Delta\vdash B$ .

To see the last meta-theorem implies the deduction theorem, assume $\Delta,A\vdash B$ . Suppose $\Delta\vdash A$ . Let $\mathcal{E}_{1}$ be a deduction of $A$ from $\Delta$ , and $\mathcal{E}_{2}$ a deduction of $B$ from $\Delta\cup\{A\}$ . Then $\mathcal{E}_{1},\mathcal{E}_{2}$ is a deduction of $B$ from $\Delta$ . So $\Delta\vdash B$ . As a result $\Delta A\to B$ by the statement of the meta-theorem. ∎

Remark. Meta-theorems 7 and 8, together with the theorem schema $A\leftrightarrow A$ , show that $\leftrightarrow$ defines an equivalence relation on the set of all wff’s of propositional logic. Formally, for any two wff’s $A, B$ , if we define $A\sim B$ iff $\vdash A\leftrightarrow B$ , then $\sim$ 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