# First theorems of Propositional Calculus

name: proptheo1, module version: 1.00.00, rule version: 1.00.00, original: proptheo1, author of this module: Michael Meyling

## Description

This module includes first proofs of propositional calculus theorems.

## References

This document uses the results of the following documents:

## Content

First we prove a well known tautology:

1. Proposition
(
ØP Ú P)     (theo1)

Proof:
 1 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 2 (((P Ú P) ® Q) ® ((A Ú (P Ú P)) ® (A Ú Q))) replace proposition variable P by (P Ú P) in 1 3 (((P Ú P) ® P) ® ((A Ú (P Ú P)) ® (A Ú P))) replace proposition variable Q by P in 2 4 (((P Ú P) ® P) ® ((ØP Ú (P Ú P)) ® (ØP Ú P))) replace proposition variable A by ØP in 3 5 ((P Ú P) ® P) add axiom axiom1 6 ((ØP Ú (P Ú P)) ® (ØP Ú P)) modus ponens with 5, 4 7 ((P ® (P Ú P)) ® (ØP Ú P)) reverse abbreviation impl in 6 at occurence 1 8 (P ® (P Ú Q)) add axiom axiom2 9 (P ® (P Ú P)) replace proposition variable Q by P in 8 10 (ØP Ú P) modus ponens with 9, 7 qed

We just use our first sentence to get the second theorem:

2. Proposition
(P
® P)     (theo2)

Proof:
 1 (ØP Ú P) add proposition theo1 2 (P ® P) reverse abbreviation impl in 1 at occurence 1 qed

And another use of the first theorem, to get the law of the excluded middle (tertium non datur):

3. Proposition
(P
Ú ØP)     (theo3)

Proof:
 1 (ØP Ú P) add proposition theo1 2 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 3 ((ØP Ú Q) ® (Q Ú ØP)) replace proposition variable P by ØP in 2 4 ((ØP Ú P) ® (P Ú ØP)) replace proposition variable Q by P in 3 5 (P Ú ØP) modus ponens with 1, 4 qed

Also trivial is:

4. Proposition
(P
® ØØP)     (theo4)

Proof:
 1 (P Ú ØP) add proposition theo3 2 (ØP Ú ØØP) replace proposition variable P by ØP in 1 3 (P ® ØØP) reverse abbreviation impl in 2 at occurence 1 qed

Three negations:

5. Proposition
(P
Ú ØØØP)     (theo5)

Proof:
 1 (P ® ØØP) add proposition theo4 2 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 3 ((P ® ØØP) ® ((A Ú P) ® (A Ú ØØP))) replace proposition variable Q by ØØP in 2 4 ((A Ú P) ® (A Ú ØØP)) modus ponens with 1, 3 5 ((A Ú ØP) ® (A Ú ØØØP)) replace proposition variable P by ØP in 4 6 ((P Ú ØP) ® (P Ú ØØØP)) replace proposition variable A by P in 5 7 (P Ú ØP) add proposition theo3 8 (P Ú ØØØP) modus ponens with 7, 6 qed

Now we could prove the reverse of Proposition 4:

6. Proposition
(
ØØP ® P)     (theo6)

Proof:
 1 (P Ú ØØØP) add proposition theo5 2 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 3 ((P Ú ØØØP) ® (ØØØP Ú P)) replace proposition variable Q by ØØØP in 2 4 (ØØØP Ú P) modus ponens with 1, 3 5 (ØØP ® P) reverse abbreviation impl in 4 at occurence 1 qed