some theorem schemas of propositional logic

Based on the axiom system in this entry (http://planetmath.org/AxiomSystemForPropositionalLogic), we will exhibit some theorem schemas, as well as prove some meta-theorems of propositional logic. All of these are based on the important deduction theorem, which is proved here (http://planetmath.org/DeductionTheoremHoldsForClassicalPropositionalLogic).

First, some theorem schemas:

1. $A\to \mathrm{\neg }\mathrm{\neg }A$

2. $\mathrm{\neg }\mathrm{\neg }A\to A$

3. (law of the excluded middle) $A\vee \mathrm{\neg }A$

4. (ex falso quodlibet) $⟂\to A$

5. $A\leftrightarrow A$

6. (law of double negation) $A\leftrightarrow \mathrm{\neg }\mathrm{\neg }A$

7. $A\wedge B\to A$ and $A\wedge B\to B$

8. (absorption law for $\wedge$) $A\leftrightarrow A\wedge A$

9. (commutative law for $\wedge$) $A\wedge B\leftrightarrow B\wedge A$

10. (associative law for $\wedge$) $(A\wedge B)\wedge C\leftrightarrow A\wedge (B\wedge C)$

11. (law of syllogism) $(A\to B)\to ((B\to C)\to (A\to C))$

12. (law of importation) $(A\to (B\to C))\to (A\wedge B\to C)$

13. $(A\to B)\to ((B\to (C\to D))\to (A\wedge C\to D))$

14. $(A\to B)\leftrightarrow (A\to (A\to B))$

Proof.

Many of these can be easily proved using the deduction theorem:

1. we need to show $A⊢\mathrm{\neg }\mathrm{\neg }A$, which means we need to show $A,\mathrm{\neg }A⊢⟂$. Since $\mathrm{\neg }A$ is $A\to ⟂$, by modus ponens, $A,\mathrm{\neg }A⊢⟂$.

2. we observe first that $\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A$ is an instance of the above theorem schema, since $(\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A)\to (\mathrm{\neg }\mathrm{\neg }A\to A)$ is an instance of one of the axiom schemas, we have $⊢\mathrm{\neg }\mathrm{\neg }A\to A$ as a result.

3. since $A\vee \mathrm{\neg }A$ is $\mathrm{\neg }A\to \mathrm{\neg }A$, to show $⊢A\vee \mathrm{\neg }A$, we need to show $\mathrm{\neg }A⊢\mathrm{\neg }A$, but this is obvious.

4. we need to show $⟂⊢A$. Since $⟂,⟂\to (A\to ⟂),A\to ⟂$ is a deduction of $A\to ⟂$ from $⟂$, and the result follows.

5. this is because $⊢A\to A$, so $⊢(A\to A)\wedge (A\to A)$.

6. this is the result of the first two theorem schemas above.

For the next four schemas, we need the the following meta-theorems (see here (http://planetmath.org/SomeMetatheoremsOfPropositionalLogic) for proofs):

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

2. $\mathrm{\Delta }⊢A$ implies $\mathrm{\Delta }⊢B$ iff $\mathrm{\Delta }⊢A\to B$

1. If $⊢A\wedge B$, then $⊢A$ by M1, so $⊢A\wedge B\to A$ by M2. Similarly, $⊢A\wedge B\to B$.

2. $⊢A\wedge A\to A$ comes from 7, and since $⊢A$ implies $⊢A\wedge A$ by M1, $⊢A\to A\wedge A$ by M2. Therefore, $⊢A\leftrightarrow A\wedge A$ by M1.

3. If $⊢A\wedge B$, then $⊢A$ and $⊢B$ by M1, so $⊢B\wedge A$ by M1 again, and therefore $⊢A\wedge B\to B\wedge A$ by M2. Similarly, $⊢B\wedge A\to A\wedge B$. Combining the two and apply M1, we have the result.

4. If $⊢(A\wedge B)\wedge C$, then $⊢A\wedge B$ and $⊢C$, so $⊢A$, $⊢B$, and $⊢C$ by M1. By M1 again, we have $⊢A$ and $⊢B\wedge C$, and another application of M1, $⊢A\wedge (B\wedge C)$. Therefore, by M2, $⊢(A\wedge B)\wedge C\to A\wedge (B\wedge C)$, Similarly, $⊢A\wedge (B\wedge C)\to (A\wedge B)\wedge C$. Combining the two and applying M1, we have the result.

5. $A\to B,B\to C,A⊢C$ by modus ponens 3 times.

6. $A\to (B\to C),A\wedge B,A\wedge B\to A,A,B\to C,A\wedge B\to B,B,C$ is a deduction of $C$ from $A\to (B\to C)$ and $A\wedge B$.

7. $A\to B,B\to (C\to D),A\wedge C,A\wedge C\to A,A,B,C\to D,A\wedge C\to C,C,D$ is a deduction of $D$ from $A\to B,B\to (C\to D)$, and $A\wedge C$.

8. $(A\to B)\to (A\to (A\to B))$ is just an axiom, while $⊢(A\to (A\to B))\to (A\to B)$ comes from two applications of the deduction theorem to $A\to (A\to B),A⊢B$, which is the result of the deduction $A\to (A\to B),A,A\to B,B$ of $B$ from $A\to (A\to B)$ and $A$.

∎