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, $\mathrm{\Delta }$ and $\mathrm{\Gamma }$ are sets of well-formed formulas (wff’s), and $A,B,C,\mathrm{\dots }$ are wff’s.

1. (Deduction Theorem) $\mathrm{\Delta },A⊢B$ iff $\mathrm{\Delta }⊢A\to B$.

2. (Proof by Contradiction) $\mathrm{\Delta },A⊢⟂$ iff $\mathrm{\Delta }⊢\mathrm{\neg }A$.

3. (Proof by Contrapositive) $\mathrm{\Delta },A⊢\mathrm{\neg }B$ iff $\mathrm{\Delta },B⊢\mathrm{\neg }A$.

4. (Law of Syllogism) If $\mathrm{\Delta }⊢A\to B$ and $\mathrm{\Gamma }⊢B\to C$, then $\mathrm{\Delta },\mathrm{\Gamma }⊢A\to C$.

5. $\mathrm{\Delta }⊢A$ and $\mathrm{\Delta }⊢B$ iff $\mathrm{\Delta }⊢A\wedge B$.

6. $\mathrm{\Delta }⊢A\leftrightarrow B$ iff $\mathrm{\Delta },A⊢B$ and $\mathrm{\Delta },B⊢A$.

7. If $\mathrm{\Delta }⊢A\leftrightarrow B$, then $\mathrm{\Delta }⊢B\leftrightarrow A$.

8. If $\mathrm{\Delta }⊢A\leftrightarrow B$ and $\mathrm{\Delta }⊢B\leftrightarrow C$, then $\mathrm{\Delta }⊢A\leftrightarrow C$.

9. $\mathrm{\Delta }⊢A\wedge B\to C$ iff $\mathrm{\Delta }⊢A\to (B\to C)$.

10. $\mathrm{\Delta }⊢A$ implies $\mathrm{\Delta }⊢B$ iff $\mathrm{\Delta }⊢A\to B$. This is a useful restatement of the deduction theorem.

11. (Substitution Theorem) If $⊢B_i\leftrightarrow C_i$, then $⊢A[\overline{B}/\overline{p}]\leftrightarrow A[\overline{C}/\overline{p}]$.

12. $\mathrm{\Delta }⊢⟂$ iff there is a wff $A$ such that $\mathrm{\Delta }⊢A$ and $\mathrm{\Delta }⊢\mathrm{\neg }A$.

13. If $\mathrm{\Delta },A⊢B$ and $\mathrm{\Delta },\mathrm{\neg }A⊢B$, then $\mathrm{\Delta }⊢B$.

Remark. The theorem schema $A\to \mathrm{\neg }\mathrm{\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. From $\mathrm{\Delta }⊢A\to B$, by the deduction theorem, we have $\mathrm{\Delta },A⊢B$. Let ${ℰ}_1$ be a deduction of $B$ from $\mathrm{\Delta }\cup \{A\}$, and ${ℰ}_2$ be a deduction of $B\to C$ from $\mathrm{\Gamma }$, then

   $${ℰ}_1,{ℰ}_2,C$$

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

2. $(\Rightarrow )$. Since $A\wedge B$ is $\mathrm{\neg }(A\to \mathrm{\neg }B)$, by the deduction theorem, it is enough to show $\mathrm{\Delta },A\to \mathrm{\neg }B⊢⟂$. Suppose ${ℰ}_1$ is a deduction of $A$ from $\mathrm{\Delta }$ and ${ℰ}_2$ is a deduction of $B$ from $\mathrm{\Delta }$, then

   $${ℰ}_1,{ℰ}_2,A\to \mathrm{\neg }B,\mathrm{\neg }B,⟂$$

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

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

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

3. $\mathrm{\Delta }⊢A\leftrightarrow B$ iff $\mathrm{\Delta }⊢A\to B$ and $\mathrm{\Delta }⊢B\to A$ iff $\mathrm{\Delta },A⊢B$ and $\mathrm{\Delta },B⊢A$.

4. Apply 6 to $\mathrm{\Delta }⊢A\to B$ and $\mathrm{\Delta }⊢B\to A$.

5. Apply 5 and 6.

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

7. Assume the former. Then a deduction of $B$ from $\mathrm{\Delta }$ may or may not contain $A$. In either case, $\mathrm{\Delta },A⊢B$, so $\mathrm{\Delta }⊢A\to B$ by the deduction theorem. Next, assume the later. Let ${ℰ}_1$ be a deduction of $A\to B$ from $\mathrm{\Delta }$. Then if ${ℰ}_2$ is a deduction of $A$ from $\mathrm{\Delta }$, then ${ℰ}_1,{ℰ}_2,B$ is a deduction of $B$ from $\mathrm{\Delta }$, and therefore $\mathrm{\Delta }⊢B$.

To see the last meta-theorem implies the deduction theorem, assume $\mathrm{\Delta },A⊢B$. Suppose $\mathrm{\Delta }⊢A$. Let ${ℰ}_1$ be a deduction of $A$ from $\mathrm{\Delta }$, and ${ℰ}_2$ a deduction of $B$ from $\mathrm{\Delta }\cup \{A\}$. Then ${ℰ}_1,{ℰ}_2$ is a deduction of $B$ from $\mathrm{\Delta }$. So $\mathrm{\Delta }⊢B$. As a result $\mathrm{\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 $⊢A\leftrightarrow B$, then $\sim$ is an equivalence relation.