## You are here

Homesome theorem schemas of propositional logic

## Primary tabs

# some theorem schemas of propositional logic

Based on the axiom system in this entry, 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.

First, some theorem schemas:

1. $A\to\neg\neg A$

2. $\neg\neg A\to A$

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

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

5. $A\leftrightarrow A$

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

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

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

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

10. (associative law for $\land$) $(A\land B)\land C\leftrightarrow A\land(B\land 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\land B\to C)$

13. $(A\to B)\to((B\to(C\to D))\to(A\land 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\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. 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. 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. 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. this is because $\vdash A\to A$, so $\vdash(A\to A)\land(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 for proofs):

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

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

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

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.

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.

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.

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

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

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

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

∎

## Mathematics Subject Classification

03B05*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections