First we prove a well known tautology:
1. Proposition
(ØP Ú P) (theo1)
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)
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)
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)
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)
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)
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 |