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 |