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 metatheorems 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) $\u27c2\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\u22a2\mathrm{\neg}\mathrm{\neg}A$, which means we need to show $A,\mathrm{\neg}A\u22a2\u27c2$. Since $\mathrm{\neg}A$ is $A\to \u27c2$, by modus ponens^{}, $A,\mathrm{\neg}A\u22a2\u27c2$.

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 $\u22a2\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 $\u22a2A\vee \mathrm{\neg}A$, we need to show $\mathrm{\neg}A\u22a2\mathrm{\neg}A$, but this is obvious.

4.
we need to show $\u27c2\u22a2A$. Since $\u27c2,\u27c2\to (A\to \u27c2),A\to \u27c2$ is a deduction^{} of $A\to \u27c2$ from $\u27c2$, and the result follows.

5.
this is because $\u22a2A\to A$, so $\u22a2(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 metatheorems (see here (http://planetmath.org/SomeMetatheoremsOfPropositionalLogic) for proofs):

M1.
$\mathrm{\Delta}\u22a2A$ and $\mathrm{\Delta}\u22a2B$ iff $\mathrm{\Delta}\u22a2A\wedge B$

M2.
$\mathrm{\Delta}\u22a2A$ implies $\mathrm{\Delta}\u22a2B$ iff $\mathrm{\Delta}\u22a2A\to B$

7.
If $\u22a2A\wedge B$, then $\u22a2A$ by M1, so $\u22a2A\wedge B\to A$ by M2. Similarly, $\u22a2A\wedge B\to B$.

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

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

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

11.
$A\to B,B\to C,A\u22a2C$ by modus ponens 3 times.

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

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

14.
$(A\to B)\to (A\to (A\to B))$ is just an axiom, while $\u22a2(A\to (A\to B))\to (A\to B)$ comes from two applications of the deduction theorem to $A\to (A\to B),A\u22a2B$, 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  20130322 19:33:04 
Last modified on  20130322 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 