At first we show a little proposition to demonstrate the basic proof methods of propositional calculus:
1. Proposition
P → (Q ∨ P) (lem1)
1 | (P → Q) → ((A ∨ P) → (A ∨ Q)) | add axiom axiom4 |
2 | (B → Q) → ((A ∨ B) → (A ∨ Q)) | replace proposition variable P by B in 1 |
3 | (B → (Q ∨ P)) → ((A ∨ B) → (A ∨ (Q ∨ P))) | replace proposition variable Q by Q ∨ P in 2 |
4 | ((P ∨ Q) → (Q ∨ P)) → ((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) | replace proposition variable B by P ∨ Q in 3 |
5 | ((P ∨ Q) → (Q ∨ P)) → ((¬P ∨ (P ∨ Q)) → (¬P ∨ (Q ∨ P))) | replace proposition variable A by ¬P in 4 |
6 | ((P ∨ Q) → (Q ∨ P)) → ((P → (P ∨ Q)) → (¬P ∨ (Q ∨ P))) | reverse abbreviation impl in 5 at occurence 1 |
7 | ((P ∨ Q) → (Q ∨ P)) → ((P → (P ∨ Q)) → (P → (Q ∨ P))) | reverse abbreviation impl in 6 at occurence 1 |
8 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
9 | (P → (P ∨ Q)) → (P → (Q ∨ P)) | modus ponens with 8, 7 |
10 | P → (P ∨ Q) | add axiom axiom2 |
11 | P → (Q ∨ P) | modus ponens with 10, 9 |
qed |
This is the first primitive proposition, its equal to our first axiom:
2. Proposition
(P ∨ P) → P (prin1)
1 | (P ∨ P) → P | add axiom axiom1 |
qed |
Now comes the second primitive proposition. It looks simular to our second axiom, but we have to use our first proposition to prove it:
3. Proposition
Q → (P ∨ Q) (prin2)
1 | P → (Q ∨ P) | add proposition lem1 |
2 | P → (A ∨ P) | replace proposition variable Q by A in 1 |
3 | Q → (A ∨ Q) | replace proposition variable P by Q in 2 |
4 | Q → (P ∨ Q) | replace proposition variable A by P in 3 |
qed |
The third primitive proposition:
4. Proposition
(P ∨ Q) → (Q ∨ P) (prin3)
1 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
qed |
The fourth primitive proposition was proved with the other primitve propositions by P. Bernays. Here comes the sledgehammer:
5. Proposition
(P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) (prin4)
1 | (P → Q) → ((A ∨ P) → (A ∨ Q)) | add axiom axiom4 |
2 | (P7 → Q) → ((A ∨ P7) → (A ∨ Q)) | replace proposition variable P by P7 in 1 |
3 | (P7 → P8) → ((A ∨ P7) → (A ∨ P8)) | replace proposition variable Q by P8 in 2 |
4 | (P7 → P8) → ((P9 ∨ P7) → (P9 ∨ P8)) | replace proposition variable A by P9 in 3 |
5 | P → (Q ∨ P) | add proposition lem1 |
6 | (P → (Q ∨ P)) → ((A ∨ P) → (A ∨ (Q ∨ P))) | replace proposition variable Q by Q ∨ P in 1 |
7 | (A ∨ P) → (A ∨ (Q ∨ P)) | modus ponens with 5, 6 |
8 | ((A ∨ P) → P8) → ((P9 ∨ (A ∨ P)) → (P9 ∨ P8)) | replace proposition variable P7 by A ∨ P in 4 |
9 | ((A ∨ P) → (A ∨ (Q ∨ P))) → ((P9 ∨ (A ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P)))) | replace proposition variable P8 by A ∨ (Q ∨ P) in 8 |
10 | (P9 ∨ (A ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P))) | modus ponens with 7, 9 |
11 | (Q ∨ (A ∨ P)) → (Q ∨ (A ∨ (Q ∨ P))) | replace proposition variable P9 by Q in 10 |
12 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
13 | (D ∨ Q) → (Q ∨ D) | replace proposition variable P by D in 12 |
14 | (D ∨ (A ∨ (Q ∨ P))) → ((A ∨ (Q ∨ P)) ∨ D) | replace proposition variable Q by A ∨ (Q ∨ P) in 13 |
15 | (Q ∨ (A ∨ (Q ∨ P))) → ((A ∨ (Q ∨ P)) ∨ Q) | replace proposition variable D by Q in 14 |
16 | ((Q ∨ (A ∨ (Q ∨ P))) → P8) → ((P9 ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ P8)) | replace proposition variable P7 by Q ∨ (A ∨ (Q ∨ P)) in 4 |
17 | ((Q ∨ (A ∨ (Q ∨ P))) → ((A ∨ (Q ∨ P)) ∨ Q)) → ((P9 ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q))) | replace proposition variable P8 by (A ∨ (Q ∨ P)) ∨ Q in 16 |
18 | (P9 ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) | modus ponens with 15, 17 |
19 | (¬(Q ∨ (A ∨ P)) ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (¬(Q ∨ (A ∨ P)) ∨ ((A ∨ (Q ∨ P)) ∨ Q)) | replace proposition variable P9 by ¬(Q ∨ (A ∨ P)) in 18 |
20 | ((Q ∨ (A ∨ P)) → (Q ∨ (A ∨ (Q ∨ P)))) → (¬(Q ∨ (A ∨ P)) ∨ ((A ∨ (Q ∨ P)) ∨ Q)) | reverse abbreviation impl in 19 at occurence 1 |
21 | ((Q ∨ (A ∨ P)) → (Q ∨ (A ∨ (Q ∨ P)))) → ((Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q)) | reverse abbreviation impl in 20 at occurence 1 |
22 | (Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q) | modus ponens with 11, 21 |
23 | P → (P ∨ Q) | add axiom axiom2 |
24 | A → (A ∨ Q) | replace proposition variable P by A in 23 |
25 | A → (A ∨ P) | replace proposition variable Q by P in 24 |
26 | Q → (Q ∨ P) | replace proposition variable A by Q in 25 |
27 | P → (A ∨ P) | replace proposition variable Q by A in 5 |
28 | (Q ∨ P) → (A ∨ (Q ∨ P)) | replace proposition variable P by Q ∨ P in 27 |
29 | ((Q ∨ P) → P8) → ((P9 ∨ (Q ∨ P)) → (P9 ∨ P8)) | replace proposition variable P7 by Q ∨ P in 4 |
30 | ((Q ∨ P) → (A ∨ (Q ∨ P))) → ((P9 ∨ (Q ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P)))) | replace proposition variable P8 by A ∨ (Q ∨ P) in 29 |
31 | (P9 ∨ (Q ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P))) | modus ponens with 28, 30 |
32 | (¬Q ∨ (Q ∨ P)) → (¬Q ∨ (A ∨ (Q ∨ P))) | replace proposition variable P9 by ¬Q in 31 |
33 | (Q → (Q ∨ P)) → (¬Q ∨ (A ∨ (Q ∨ P))) | reverse abbreviation impl in 32 at occurence 1 |
34 | (Q → (Q ∨ P)) → (Q → (A ∨ (Q ∨ P))) | reverse abbreviation impl in 33 at occurence 1 |
35 | Q → (A ∨ (Q ∨ P)) | modus ponens with 26, 34 |
36 | (Q → P8) → ((P9 ∨ Q) → (P9 ∨ P8)) | replace proposition variable P7 by Q in 4 |
37 | (Q → (A ∨ (Q ∨ P))) → ((P9 ∨ Q) → (P9 ∨ (A ∨ (Q ∨ P)))) | replace proposition variable P8 by A ∨ (Q ∨ P) in 36 |
38 | (P9 ∨ Q) → (P9 ∨ (A ∨ (Q ∨ P))) | modus ponens with 35, 37 |
39 | ((A ∨ (Q ∨ P)) ∨ Q) → ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) | replace proposition variable P9 by A ∨ (Q ∨ P) in 38 |
40 | (P ∨ P) → P | add axiom axiom1 |
41 | ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) → (A ∨ (Q ∨ P)) | replace proposition variable P by A ∨ (Q ∨ P) in 40 |
42 | (((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) → P8) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ P8)) | replace proposition variable P7 by (A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)) in 4 |
43 | (((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) → (A ∨ (Q ∨ P))) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ (A ∨ (Q ∨ P)))) | replace proposition variable P8 by A ∨ (Q ∨ P) in 42 |
44 | (P9 ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ (A ∨ (Q ∨ P))) | modus ponens with 41, 43 |
45 | (¬((A ∨ (Q ∨ P)) ∨ Q) ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (¬((A ∨ (Q ∨ P)) ∨ Q) ∨ (A ∨ (Q ∨ P))) | replace proposition variable P9 by ¬((A ∨ (Q ∨ P)) ∨ Q) in 44 |
46 | (((A ∨ (Q ∨ P)) ∨ Q) → ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (¬((A ∨ (Q ∨ P)) ∨ Q) ∨ (A ∨ (Q ∨ P))) | reverse abbreviation impl in 45 at occurence 1 |
47 | (((A ∨ (Q ∨ P)) ∨ Q) → ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (((A ∨ (Q ∨ P)) ∨ Q) → (A ∨ (Q ∨ P))) | reverse abbreviation impl in 46 at occurence 1 |
48 | ((A ∨ (Q ∨ P)) ∨ Q) → (A ∨ (Q ∨ P)) | modus ponens with 39, 47 |
49 | (((A ∨ (Q ∨ P)) ∨ Q) → P8) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (P9 ∨ P8)) | replace proposition variable P7 by (A ∨ (Q ∨ P)) ∨ Q in 4 |
50 | (((A ∨ (Q ∨ P)) ∨ Q) → (A ∨ (Q ∨ P))) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (P9 ∨ (A ∨ (Q ∨ P)))) | replace proposition variable P8 by A ∨ (Q ∨ P) in 49 |
51 | (P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (P9 ∨ (A ∨ (Q ∨ P))) | modus ponens with 48, 50 |
52 | (¬(Q ∨ (A ∨ P)) ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (¬(Q ∨ (A ∨ P)) ∨ (A ∨ (Q ∨ P))) | replace proposition variable P9 by ¬(Q ∨ (A ∨ P)) in 51 |
53 | ((Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q)) → (¬(Q ∨ (A ∨ P)) ∨ (A ∨ (Q ∨ P))) | reverse abbreviation impl in 52 at occurence 1 |
54 | ((Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q)) → ((Q ∨ (A ∨ P)) → (A ∨ (Q ∨ P))) | reverse abbreviation impl in 53 at occurence 1 |
55 | (Q ∨ (A ∨ P)) → (A ∨ (Q ∨ P)) | modus ponens with 22, 54 |
56 | (P7 ∨ (A ∨ P)) → (A ∨ (P7 ∨ P)) | replace proposition variable Q by P7 in 55 |
57 | (P7 ∨ (Q ∨ P)) → (Q ∨ (P7 ∨ P)) | replace proposition variable A by Q in 56 |
58 | (P7 ∨ (Q ∨ A)) → (Q ∨ (P7 ∨ A)) | replace proposition variable P by A in 57 |
59 | (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) | replace proposition variable P7 by P in 58 |
qed |
The fifth primitive proposition is our fourth axiom:
6. Proposition
(P → Q) → ((A ∨ P) → (A ∨ Q)) (prin5)
1 | (P → Q) → ((A ∨ P) → (A ∨ Q)) | add axiom axiom4 |
qed |