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 |