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

∎

Title	some theorem schemas of propositional logic
Canonical name	SomeTheoremSchemasOfPropositionalLogic
Date of creation	2013-03-22 19:33:04
Last modified on	2013-03-22 19:33:04
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	40
Author	CWoo (3771)
Entry type	Result
Classification	msc 03B05
Defines	law of double negation
Defines	law of the excluded middle
Defines	ex falso quodlibet