# 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. 1.
2. 2.
3. 3.

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

4. 4.

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

5. 5.

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

6. 6.

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

7. 7.

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

8. 8.

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

9. 9.

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

10. 10.

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

11. 11.

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

12. 12.

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

13. 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.

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

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

3. 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$.

4. 7.

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

5. 8.

Apply 5 and 6.

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

7. 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 SomeMetatheoremsOfPropositionalLogic 2013-03-22 19:34:29 2013-03-22 19:34:29 CWoo (3771) CWoo (3771) 10 CWoo (3771) Result msc 03B05 law of syllogism