Uses the following modules:
At first we show a little proposition to demonstrate the basic proof methods of propositional calculus:
Proposition 1
(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:
Proposition 2
((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:
Proposition 3
(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:
Proposition 4
((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:
Proposition 5
((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 Þ (Q Ú P)) | add proposition lem1 |
28 | (P Þ (A Ú P)) | replace proposition variable Q by A in 27 |
29 | ((Q Ú P) Þ (A Ú (Q Ú P))) | replace proposition variable P by (Q Ú P) in 28 |
30 | (((Q Ú P) Þ P8) Þ ((P9 Ú (Q Ú P)) Þ (P9 Ú P8))) | replace proposition variable P7 by (Q Ú P) in 4 |
31 | (((Q Ú P) Þ (A Ú (Q Ú P))) Þ ((P9 Ú (Q Ú P)) Þ (P9 Ú (A Ú (Q Ú P))))) | replace proposition variable P8 by (A Ú (Q Ú P)) in 30 |
32 | ((P9 Ú (Q Ú P)) Þ (P9 Ú (A Ú (Q Ú P)))) | modus ponens with 29, 31 |
33 | ((ØQ Ú (Q Ú P)) Þ (ØQ Ú (A Ú (Q Ú P)))) | replace proposition variable P9 by ØQ in 32 |
34 | ((Q Þ (Q Ú P)) Þ (ØQ Ú (A Ú (Q Ú P)))) | reverse abbreviation impl in 33 at occurence 1 |
35 | ((Q Þ (Q Ú P)) Þ (Q Þ (A Ú (Q Ú P)))) | reverse abbreviation impl in 34 at occurence 1 |
36 | (Q Þ (A Ú (Q Ú P))) | modus ponens with 26, 35 |
37 | ((Q Þ P8) Þ ((P9 Ú Q) Þ (P9 Ú P8))) | replace proposition variable P7 by Q in 4 |
38 | ((Q Þ (A Ú (Q Ú P))) Þ ((P9 Ú Q) Þ (P9 Ú (A Ú (Q Ú P))))) | replace proposition variable P8 by (A Ú (Q Ú P)) in 37 |
39 | ((P9 Ú Q) Þ (P9 Ú (A Ú (Q Ú P)))) | modus ponens with 36, 38 |
40 | (((A Ú (Q Ú P)) Ú Q) Þ ((A Ú (Q Ú P)) Ú (A Ú (Q Ú P)))) | replace proposition variable P9 by (A Ú (Q Ú P)) in 39 |
41 | ((P Ú P) Þ P) | add axiom axiom1 |
42 | (((A Ú (Q Ú P)) Ú (A Ú (Q Ú P))) Þ (A Ú (Q Ú P))) | replace proposition variable P by (A Ú (Q Ú P)) in 41 |
43 | ((((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 |
44 | ((((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 43 |
45 | ((P9 Ú ((A Ú (Q Ú P)) Ú (A Ú (Q Ú P)))) Þ (P9 Ú (A Ú (Q Ú P)))) | modus ponens with 42, 44 |
46 | ((Ø((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 45 |
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)) Ú (A Ú (Q Ú P)))) Þ (((A Ú (Q Ú P)) Ú Q) Þ (A Ú (Q Ú P)))) | reverse abbreviation impl in 47 at occurence 1 |
49 | (((A Ú (Q Ú P)) Ú Q) Þ (A Ú (Q Ú P))) | modus ponens with 40, 48 |
50 | ((((A Ú (Q Ú P)) Ú Q) Þ P8) Þ ((P9 Ú ((A Ú (Q Ú P)) Ú Q)) Þ (P9 Ú P8))) | replace proposition variable P7 by ((A Ú (Q Ú P)) Ú Q) in 4 |
51 | ((((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 50 |
52 | ((P9 Ú ((A Ú (Q Ú P)) Ú Q)) Þ (P9 Ú (A Ú (Q Ú P)))) | modus ponens with 49, 51 |
53 | ((Ø(Q Ú (A Ú P)) Ú ((A Ú (Q Ú P)) Ú Q)) Þ (Ø(Q Ú (A Ú P)) Ú (A Ú (Q Ú P)))) | replace proposition variable P9 by Ø(Q Ú (A Ú P)) in 52 |
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)) Ú Q)) Þ ((Q Ú (A Ú P)) Þ (A Ú (Q Ú P)))) | reverse abbreviation impl in 54 at occurence 1 |
56 | ((Q Ú (A Ú P)) Þ (A Ú (Q Ú P))) | modus ponens with 22, 55 |
57 | ((P7 Ú (A Ú P)) Þ (A Ú (P7 Ú P))) | replace proposition variable Q by P7 in 56 |
58 | ((P7 Ú (Q Ú P)) Þ (Q Ú (P7 Ú P))) | replace proposition variable A by Q in 57 |
59 | ((P7 Ú (Q Ú A)) Þ (Q Ú (P7 Ú A))) | replace proposition variable P by A in 58 |
60 | ((P Ú (Q Ú A)) Þ (Q Ú (P Ú A))) | replace proposition variable P7 by P in 59 |
qed |
The fifth primitive proposition is our fourth axiom:
Proposition 6
((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) (prin5)
1 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
qed |