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

$A\to\neg\neg A$

2. 2.

$\neg\neg A\to A$

3. 3.

(law of the excluded middle) $A\lor\neg A$

4. 4.

(ex falso quodlibet) $\perp\to A$

5. 5.

$A\leftrightarrow A$

6. 6.

(law of double negation) $A\leftrightarrow\neg\neg A$

7. 7.

$A\land B\to A$ and $A\land B\to B$

8. 8.

(absorption law for $\land$) $A\leftrightarrow A\land A$

9. 9.

(commutative law for $\land$) $A\land B\leftrightarrow B\land A$

10. 10.

(associative law for $\land$) $(A\land B)\land C\leftrightarrow A\land(B\land C)$

11. 11.

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

12. 12.

(law of importation) $(A\to(B\to C))\to(A\land B\to C)$

13. 13.

$(A\to B)\to((B\to(C\to D))\to(A\land C\to D))$

14. 14.

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

###### Proof.

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

1. 1.

we need to show $A\vdash\neg\neg A$, which means we need to show $A,\neg A\vdash\perp$. Since $\neg A$ is $A\to\perp$, by modus ponens, $A,\neg A\vdash\perp$.

2. 2.

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

3. 3.

since $A\lor\neg A$ is $\neg A\to\neg A$, to show $\vdash A\lor\neg A$, we need to show $\neg A\vdash\neg A$, but this is obvious.

4. 4.

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

5. 5.

this is because $\vdash A\to A$, so $\vdash(A\to A)\land(A\to A)$.

6. 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. M1.

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

2. M2.

$\Delta\vdash A$ implies $\Delta\vdash B$ iff $\Delta\vdash A\to B$

1. 7.

If $\vdash A\land B$, then $\vdash A$ by M1, so $\vdash A\land B\to A$ by M2. Similarly, $\vdash A\land B\to B$.

2. 8.

$\vdash A\land A\to A$ comes from 7, and since $\vdash A$ implies $\vdash A\land A$ by M1, $\vdash A\to A\land A$ by M2. Therefore, $\vdash A\leftrightarrow A\land A$ by M1.

3. 9.

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

4. 10.

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

5. 11.

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

6. 12.

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

7. 13.

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

8. 14.

$(A\to B)\to(A\to(A\to B))$ is just an axiom, while $\vdash(A\to(A\to B))\to(A\to B)$ comes from two applications of the deduction theorem to $A\to(A\to B),A\vdash 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 SomeTheoremSchemasOfPropositionalLogic 2013-03-22 19:33:04 2013-03-22 19:33:04 CWoo (3771) CWoo (3771) 40 CWoo (3771) Result msc 03B05 law of double negation law of the excluded middle ex falso quodlibet