for questions or link request: module admin

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