Uses the following modules:
Is used by the following modules:
Negation of a conjunction:
1. Proposition
(Ø(P Ù Q) Þ (ØP Ú ØQ)) (hilb18)
1 | (ØØP Þ P) | add proposition hilb6 |
2 | (ØØQ Þ Q) | replace proposition variable P by Q in 1 |
3 | (ØØ(ØP Ú ØQ) Þ (ØP Ú ØQ)) | replace proposition variable Q by (ØP Ú ØQ) in 2 |
4 | (Ø(P Ù Q) Þ (ØP Ú ØQ)) | reverse abbreviation and in 3 at occurence 1 |
qed |
The reverse of a negation of a conjunction:
2. Proposition
((ØP Ú ØQ) Þ Ø(P Ù Q)) (hilb19)
1 | (P Þ ØØP) | add proposition hilb5 |
2 | (Q Þ ØØQ) | replace proposition variable P by Q in 1 |
3 | ((ØP Ú ØQ) Þ ØØ(ØP Ú ØQ)) | replace proposition variable Q by (ØP Ú ØQ) in 2 |
4 | ((ØP Ú ØQ) Þ Ø(P Ù Q)) | reverse abbreviation and in 3 at occurence 1 |
qed |
Negation of a disjunction:
3. Proposition
(Ø(P Ú Q) Þ (ØP Ù ØQ)) (hilb20)
1 | (ØØP Þ P) | add proposition hilb6 |
2 | (ØØQ Þ Q) | replace proposition variable P by Q in 1 |
3 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
4 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 3 |
5 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 4 |
6 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 5 |
7 | ((D Þ C) Þ ((Q Ú D) Þ (Q Ú C))) | replace proposition variable B by Q in 6 |
8 | ((D Þ P) Þ ((Q Ú D) Þ (Q Ú P))) | replace proposition variable C by P in 7 |
9 | ((ØØP Þ P) Þ ((Q Ú ØØP) Þ (Q Ú P))) | replace proposition variable D by ØØP in 8 |
10 | ((Q Ú ØØP) Þ (Q Ú P)) | modus ponens with 1, 9 |
11 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
12 | ((P Ú A) Þ (A Ú P)) | replace proposition variable Q by A in 11 |
13 | ((B Ú A) Þ (A Ú B)) | replace proposition variable P by B in 12 |
14 | ((B Ú P) Þ (P Ú B)) | replace proposition variable A by P in 13 |
15 | ((Q Ú P) Þ (P Ú Q)) | replace proposition variable B by Q in 14 |
16 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
17 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 16 |
18 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 17 |
19 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 18 |
20 | ((D Þ C) Þ (((Q Ú ØØP) Þ D) Þ ((Q Ú ØØP) Þ C))) | replace proposition variable B by (Q Ú ØØP) in 19 |
21 | ((D Þ (P Ú Q)) Þ (((Q Ú ØØP) Þ D) Þ ((Q Ú ØØP) Þ (P Ú Q)))) | replace proposition variable C by (P Ú Q) in 20 |
22 | (((Q Ú P) Þ (P Ú Q)) Þ (((Q Ú ØØP) Þ (Q Ú P)) Þ ((Q Ú ØØP) Þ (P Ú Q)))) | replace proposition variable D by (Q Ú P) in 21 |
23 | (((Q Ú ØØP) Þ (Q Ú P)) Þ ((Q Ú ØØP) Þ (P Ú Q))) | modus ponens with 15, 22 |
24 | ((Q Ú ØØP) Þ (P Ú Q)) | modus ponens with 10, 23 |
25 | ((B Ú Q) Þ (Q Ú B)) | replace proposition variable A by Q in 13 |
26 | ((ØØP Ú Q) Þ (Q Ú ØØP)) | replace proposition variable B by ØØP in 25 |
27 | ((D Þ C) Þ (((ØØP Ú Q) Þ D) Þ ((ØØP Ú Q) Þ C))) | replace proposition variable B by (ØØP Ú Q) in 19 |
28 | ((D Þ (P Ú Q)) Þ (((ØØP Ú Q) Þ D) Þ ((ØØP Ú Q) Þ (P Ú Q)))) | replace proposition variable C by (P Ú Q) in 27 |
29 | (((Q Ú ØØP) Þ (P Ú Q)) Þ (((ØØP Ú Q) Þ (Q Ú ØØP)) Þ ((ØØP Ú Q) Þ (P Ú Q)))) | replace proposition variable D by (Q Ú ØØP) in 28 |
30 | (((ØØP Ú Q) Þ (Q Ú ØØP)) Þ ((ØØP Ú Q) Þ (P Ú Q))) | modus ponens with 24, 29 |
31 | ((ØØP Ú Q) Þ (P Ú Q)) | modus ponens with 26, 30 |
32 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
33 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 32 |
34 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 33 |
35 | ((B Þ (P Ú Q)) Þ (Ø(P Ú Q) Þ ØB)) | replace proposition variable A by (P Ú Q) in 34 |
36 | (((ØØP Ú Q) Þ (P Ú Q)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú Q))) | replace proposition variable B by (ØØP Ú Q) in 35 |
37 | (Ø(P Ú Q) Þ Ø(ØØP Ú Q)) | modus ponens with 31, 36 |
38 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
39 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
40 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 38 |
41 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 40 |
42 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 39 |
43 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 42 |
44 | ((D Þ C) Þ ((ØØP Ú D) Þ (ØØP Ú C))) | replace proposition variable B by ØØP in 6 |
45 | ((D Þ Q) Þ ((ØØP Ú D) Þ (ØØP Ú Q))) | replace proposition variable C by Q in 44 |
46 | ((ØØQ Þ Q) Þ ((ØØP Ú ØØQ) Þ (ØØP Ú Q))) | replace proposition variable D by ØØQ in 45 |
47 | ((ØØP Ú ØØQ) Þ (ØØP Ú Q)) | modus ponens with 2, 46 |
48 | ((B Þ (ØØP Ú Q)) Þ (Ø(ØØP Ú Q) Þ ØB)) | replace proposition variable A by (ØØP Ú Q) in 34 |
49 | (((ØØP Ú ØØQ) Þ (ØØP Ú Q)) Þ (Ø(ØØP Ú Q) Þ Ø(ØØP Ú ØØQ))) | replace proposition variable B by (ØØP Ú ØØQ) in 48 |
50 | (Ø(ØØP Ú Q) Þ Ø(ØØP Ú ØØQ)) | modus ponens with 47, 49 |
51 | ((D Þ C) Þ ((ØØ(P Ú Q) Ú D) Þ (ØØ(P Ú Q) Ú C))) | replace proposition variable B by ØØ(P Ú Q) in 6 |
52 | ((D Þ Ø(ØØP Ú ØØQ)) Þ ((ØØ(P Ú Q) Ú D) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) | replace proposition variable C by Ø(ØØP Ú ØØQ) in 51 |
53 | ((Ø(ØØP Ú Q) Þ Ø(ØØP Ú ØØQ)) Þ ((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) | replace proposition variable D by Ø(ØØP Ú Q) in 52 |
54 | ((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) | modus ponens with 50, 53 |
55 | ((B Þ Ø(ØØP Ú Q)) Þ (ØB Ú Ø(ØØP Ú Q))) | replace proposition variable A by Ø(ØØP Ú Q) in 41 |
56 | ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) | replace proposition variable B by Ø(P Ú Q) in 55 |
57 | ((D Þ C) Þ (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ D) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ C))) | replace proposition variable B by (Ø(P Ú Q) Þ Ø(ØØP Ú Q)) in 19 |
58 | ((D Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) Þ (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ D) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))))) | replace proposition variable C by (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) in 57 |
59 | (((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) Þ (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))))) | replace proposition variable D by (ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) in 58 |
60 | (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) | modus ponens with 54, 59 |
61 | ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) | modus ponens with 56, 60 |
62 | ((ØB Ú Ø(ØØP Ú ØØQ)) Þ (B Þ Ø(ØØP Ú ØØQ))) | replace proposition variable A by Ø(ØØP Ú ØØQ) in 43 |
63 | ((ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))) | replace proposition variable B by Ø(P Ú Q) in 62 |
64 | ((D Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))) Þ (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ D) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))))) | replace proposition variable C by (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ)) in 57 |
65 | (((ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))) Þ (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))))) | replace proposition variable D by (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) in 64 |
66 | (((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) Þ ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ)))) | modus ponens with 63, 65 |
67 | ((Ø(P Ú Q) Þ Ø(ØØP Ú Q)) Þ (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))) | modus ponens with 61, 66 |
68 | (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ)) | modus ponens with 37, 67 |
69 | (Ø(P Ú Q) Þ (ØP Ù ØQ)) | reverse abbreviation and in 68 at occurence 1 |
qed |
Reverse of a negation of a disjunction:
4. Proposition
((ØP Ù ØQ) Þ Ø(P Ú Q)) (hilb21)
1 | (P Þ ØØP) | add proposition hilb5 |
2 | (Q Þ ØØQ) | replace proposition variable P by Q in 1 |
3 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
4 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 3 |
5 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 4 |
6 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 5 |
7 | ((D Þ C) Þ ((Q Ú D) Þ (Q Ú C))) | replace proposition variable B by Q in 6 |
8 | ((D Þ ØØP) Þ ((Q Ú D) Þ (Q Ú ØØP))) | replace proposition variable C by ØØP in 7 |
9 | ((P Þ ØØP) Þ ((Q Ú P) Þ (Q Ú ØØP))) | replace proposition variable D by P in 8 |
10 | ((Q Ú P) Þ (Q Ú ØØP)) | modus ponens with 1, 9 |
11 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
12 | ((P Ú A) Þ (A Ú P)) | replace proposition variable Q by A in 11 |
13 | ((B Ú A) Þ (A Ú B)) | replace proposition variable P by B in 12 |
14 | ((B Ú ØØP) Þ (ØØP Ú B)) | replace proposition variable A by ØØP in 13 |
15 | ((Q Ú ØØP) Þ (ØØP Ú Q)) | replace proposition variable B by Q in 14 |
16 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
17 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 16 |
18 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 17 |
19 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 18 |
20 | ((D Þ C) Þ (((Q Ú P) Þ D) Þ ((Q Ú P) Þ C))) | replace proposition variable B by (Q Ú P) in 19 |
21 | ((D Þ (ØØP Ú Q)) Þ (((Q Ú P) Þ D) Þ ((Q Ú P) Þ (ØØP Ú Q)))) | replace proposition variable C by (ØØP Ú Q) in 20 |
22 | (((Q Ú ØØP) Þ (ØØP Ú Q)) Þ (((Q Ú P) Þ (Q Ú ØØP)) Þ ((Q Ú P) Þ (ØØP Ú Q)))) | replace proposition variable D by (Q Ú ØØP) in 21 |
23 | (((Q Ú P) Þ (Q Ú ØØP)) Þ ((Q Ú P) Þ (ØØP Ú Q))) | modus ponens with 15, 22 |
24 | ((Q Ú P) Þ (ØØP Ú Q)) | modus ponens with 10, 23 |
25 | ((D Þ C) Þ (((P Ú Q) Þ D) Þ ((P Ú Q) Þ C))) | replace proposition variable B by (P Ú Q) in 19 |
26 | ((D Þ (ØØP Ú Q)) Þ (((P Ú Q) Þ D) Þ ((P Ú Q) Þ (ØØP Ú Q)))) | replace proposition variable C by (ØØP Ú Q) in 25 |
27 | (((Q Ú P) Þ (ØØP Ú Q)) Þ (((P Ú Q) Þ (Q Ú P)) Þ ((P Ú Q) Þ (ØØP Ú Q)))) | replace proposition variable D by (Q Ú P) in 26 |
28 | (((P Ú Q) Þ (Q Ú P)) Þ ((P Ú Q) Þ (ØØP Ú Q))) | modus ponens with 24, 27 |
29 | ((P Ú Q) Þ (ØØP Ú Q)) | modus ponens with 11, 28 |
30 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
31 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 30 |
32 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 31 |
33 | ((B Þ (ØØP Ú Q)) Þ (Ø(ØØP Ú Q) Þ ØB)) | replace proposition variable A by (ØØP Ú Q) in 32 |
34 | (((P Ú Q) Þ (ØØP Ú Q)) Þ (Ø(ØØP Ú Q) Þ Ø(P Ú Q))) | replace proposition variable B by (P Ú Q) in 33 |
35 | (Ø(ØØP Ú Q) Þ Ø(P Ú Q)) | modus ponens with 29, 34 |
36 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
37 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
38 | ((B Ú Ø(P Ú Q)) Þ (Ø(P Ú Q) Ú B)) | replace proposition variable A by Ø(P Ú Q) in 13 |
39 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 36 |
40 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 39 |
41 | ((B Þ Ø(P Ú Q)) Þ (ØB Ú Ø(P Ú Q))) | replace proposition variable A by Ø(P Ú Q) in 40 |
42 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 37 |
43 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 42 |
44 | ((ØB Ú Ø(P Ú Q)) Þ (B Þ Ø(P Ú Q))) | replace proposition variable A by Ø(P Ú Q) in 43 |
45 | ((D Þ C) Þ ((ØØP Ú D) Þ (ØØP Ú C))) | replace proposition variable B by ØØP in 6 |
46 | ((D Þ ØØQ) Þ ((ØØP Ú D) Þ (ØØP Ú ØØQ))) | replace proposition variable C by ØØQ in 45 |
47 | ((Q Þ ØØQ) Þ ((ØØP Ú Q) Þ (ØØP Ú ØØQ))) | replace proposition variable D by Q in 46 |
48 | ((ØØP Ú Q) Þ (ØØP Ú ØØQ)) | modus ponens with 2, 47 |
49 | ((B Þ (ØØP Ú ØØQ)) Þ (Ø(ØØP Ú ØØQ) Þ ØB)) | replace proposition variable A by (ØØP Ú ØØQ) in 32 |
50 | (((ØØP Ú Q) Þ (ØØP Ú ØØQ)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(ØØP Ú Q))) | replace proposition variable B by (ØØP Ú Q) in 49 |
51 | (Ø(ØØP Ú ØØQ) Þ Ø(ØØP Ú Q)) | modus ponens with 48, 50 |
52 | ((B Þ Ø(ØØP Ú Q)) Þ (ØØ(ØØP Ú Q) Þ ØB)) | replace proposition variable A by Ø(ØØP Ú Q) in 32 |
53 | ((Ø(ØØP Ú ØØQ) Þ Ø(ØØP Ú Q)) Þ (ØØ(ØØP Ú Q) Þ ØØ(ØØP Ú ØØQ))) | replace proposition variable B by Ø(ØØP Ú ØØQ) in 52 |
54 | (ØØ(ØØP Ú Q) Þ ØØ(ØØP Ú ØØQ)) | modus ponens with 51, 53 |
55 | ((D Þ C) Þ ((Ø(P Ú Q) Ú D) Þ (Ø(P Ú Q) Ú C))) | replace proposition variable B by Ø(P Ú Q) in 6 |
56 | ((D Þ ØØ(ØØP Ú ØØQ)) Þ ((Ø(P Ú Q) Ú D) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)))) | replace proposition variable C by ØØ(ØØP Ú ØØQ) in 55 |
57 | ((ØØ(ØØP Ú Q) Þ ØØ(ØØP Ú ØØQ)) Þ ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)))) | replace proposition variable D by ØØ(ØØP Ú Q) in 56 |
58 | ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) | modus ponens with 54, 57 |
59 | ((B Ú ØØ(ØØP Ú ØØQ)) Þ (ØØ(ØØP Ú ØØQ) Ú B)) | replace proposition variable A by ØØ(ØØP Ú ØØQ) in 13 |
60 | ((Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) | replace proposition variable B by Ø(P Ú Q) in 59 |
61 | ((D Þ C) Þ (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ D) Þ ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ C))) | replace proposition variable B by (Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) in 19 |
62 | ((D Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ D) Þ ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) | replace proposition variable C by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 61 |
63 | (((Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) Þ ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) | replace proposition variable D by (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) in 62 |
64 | (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) Þ ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) | modus ponens with 60, 63 |
65 | ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) | modus ponens with 58, 64 |
66 | ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) | replace proposition variable B by ØØ(ØØP Ú Q) in 38 |
67 | ((D Þ C) Þ (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ D) Þ ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ C))) | replace proposition variable B by (ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) in 19 |
68 | ((D Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ D) Þ ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) | replace proposition variable C by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 67 |
69 | (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) Þ ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) | replace proposition variable D by (Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) in 68 |
70 | (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) Þ ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) | modus ponens with 65, 69 |
71 | ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) | modus ponens with 66, 70 |
72 | ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) | replace proposition variable B by Ø(ØØP Ú Q) in 41 |
73 | ((D Þ C) Þ (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ D) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ C))) | replace proposition variable B by (Ø(ØØP Ú Q) Þ Ø(P Ú Q)) in 19 |
74 | ((D Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ D) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) | replace proposition variable C by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 73 |
75 | (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))))) | replace proposition variable D by (ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) in 74 |
76 | (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) | modus ponens with 71, 75 |
77 | ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) | modus ponens with 72, 76 |
78 | ((ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q))) | replace proposition variable B by Ø(ØØP Ú ØØQ) in 44 |
79 | ((D Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q))) Þ (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ D) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q))))) | replace proposition variable C by (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q)) in 73 |
80 | (((ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q))) Þ (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q))))) | replace proposition variable D by (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) in 79 |
81 | (((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) Þ ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q)))) | modus ponens with 78, 80 |
82 | ((Ø(ØØP Ú Q) Þ Ø(P Ú Q)) Þ (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q))) | modus ponens with 77, 81 |
83 | (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q)) | modus ponens with 35, 82 |
84 | ((ØP Ù ØQ) Þ Ø(P Ú Q)) | reverse abbreviation and in 83 at occurence 1 |
qed |
The Conjunction is commutative:
5. Proposition
((P Ù Q) Þ (Q Ù P)) (hilb22)
1 | (P Þ P) | add proposition hilb2 |
2 | (Q Þ Q) | replace proposition variable P by Q in 1 |
3 | ((P Ù Q) Þ (P Ù Q)) | replace proposition variable Q by (P Ù Q) in 2 |
4 | ((P Ù Q) Þ Ø(ØP Ú ØQ)) | use abbreviation and in 3 at occurence 2 |
5 | ((Q Ú P) Þ (P Ú Q)) | add proposition hilb10 |
6 | ((A Ú P) Þ (P Ú A)) | replace proposition variable Q by A in 5 |
7 | ((A Ú B) Þ (B Ú A)) | replace proposition variable P by B in 6 |
8 | ((ØQ Ú B) Þ (B Ú ØQ)) | replace proposition variable A by ØQ in 7 |
9 | ((ØQ Ú ØP) Þ (ØP Ú ØQ)) | replace proposition variable B by ØP in 8 |
10 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
11 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 10 |
12 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 11 |
13 | ((B Þ (ØP Ú ØQ)) Þ (Ø(ØP Ú ØQ) Þ ØB)) | replace proposition variable A by (ØP Ú ØQ) in 12 |
14 | (((ØQ Ú ØP) Þ (ØP Ú ØQ)) Þ (Ø(ØP Ú ØQ) Þ Ø(ØQ Ú ØP))) | replace proposition variable B by (ØQ Ú ØP) in 13 |
15 | (Ø(ØP Ú ØQ) Þ Ø(ØQ Ú ØP)) | modus ponens with 9, 14 |
16 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
17 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
18 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
19 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 18 |
20 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 19 |
21 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 20 |
22 | ((D Þ C) Þ ((Ø(P Ù Q) Ú D) Þ (Ø(P Ù Q) Ú C))) | replace proposition variable B by Ø(P Ù Q) in 21 |
23 | ((D Þ Ø(ØQ Ú ØP)) Þ ((Ø(P Ù Q) Ú D) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) | replace proposition variable C by Ø(ØQ Ú ØP) in 22 |
24 | ((Ø(ØP Ú ØQ) Þ Ø(ØQ Ú ØP)) Þ ((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) | replace proposition variable D by Ø(ØP Ú ØQ) in 23 |
25 | ((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) | modus ponens with 15, 24 |
26 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 16 |
27 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 26 |
28 | ((B Þ Ø(ØP Ú ØQ)) Þ (ØB Ú Ø(ØP Ú ØQ))) | replace proposition variable A by Ø(ØP Ú ØQ) in 27 |
29 | (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) | replace proposition variable B by (P Ù Q) in 28 |
30 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
31 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 30 |
32 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 31 |
33 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 32 |
34 | ((D Þ C) Þ ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ D) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ C))) | replace proposition variable B by ((P Ù Q) Þ Ø(ØP Ú ØQ)) in 33 |
35 | ((D Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) Þ ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ D) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))))) | replace proposition variable C by (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) in 34 |
36 | (((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) Þ ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))))) | replace proposition variable D by (Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) in 35 |
37 | ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) | modus ponens with 25, 36 |
38 | (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) | modus ponens with 29, 37 |
39 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 17 |
40 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 39 |
41 | ((ØB Ú Ø(ØQ Ú ØP)) Þ (B Þ Ø(ØQ Ú ØP))) | replace proposition variable A by Ø(ØQ Ú ØP) in 40 |
42 | ((Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) Þ ((P Ù Q) Þ Ø(ØQ Ú ØP))) | replace proposition variable B by (P Ù Q) in 41 |
43 | ((D Þ ((P Ù Q) Þ Ø(ØQ Ú ØP))) Þ ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ D) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ ((P Ù Q) Þ Ø(ØQ Ú ØP))))) | replace proposition variable C by ((P Ù Q) Þ Ø(ØQ Ú ØP)) in 34 |
44 | (((Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) Þ ((P Ù Q) Þ Ø(ØQ Ú ØP))) Þ ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ ((P Ù Q) Þ Ø(ØQ Ú ØP))))) | replace proposition variable D by (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) in 43 |
45 | ((((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) Þ (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ ((P Ù Q) Þ Ø(ØQ Ú ØP)))) | modus ponens with 42, 44 |
46 | (((P Ù Q) Þ Ø(ØP Ú ØQ)) Þ ((P Ù Q) Þ Ø(ØQ Ú ØP))) | modus ponens with 38, 45 |
47 | ((P Ù Q) Þ Ø(ØQ Ú ØP)) | modus ponens with 4, 46 |
48 | ((P Ù Q) Þ (Q Ù P)) | reverse abbreviation and in 47 at occurence 1 |
qed |
A technical lemma that is simular to the previous one:
6. Proposition
((Q Ù P) Þ (P Ù Q)) (hilb23)
1 | ((P Ù Q) Þ (Q Ù P)) | add proposition hilb22 |
2 | ((P Ù A) Þ (A Ù P)) | replace proposition variable Q by A in 1 |
3 | ((B Ù A) Þ (A Ù B)) | replace proposition variable P by B in 2 |
4 | ((B Ù P) Þ (P Ù B)) | replace proposition variable A by P in 3 |
5 | ((Q Ù P) Þ (P Ù Q)) | replace proposition variable B by Q in 4 |
qed |
Reduction of a conjunction:
7. Proposition
((P Ù Q) Þ P) (hilb24)
1 | (P Þ (P Ú Q)) | add axiom axiom2 |
2 | (P Þ (P Ú A)) | replace proposition variable Q by A in 1 |
3 | (B Þ (B Ú A)) | replace proposition variable P by B in 2 |
4 | (B Þ (B Ú ØQ)) | replace proposition variable A by ØQ in 3 |
5 | (ØP Þ (ØP Ú ØQ)) | replace proposition variable B by ØP in 4 |
6 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
7 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 6 |
8 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 7 |
9 | ((B Þ (ØP Ú ØQ)) Þ (Ø(ØP Ú ØQ) Þ ØB)) | replace proposition variable A by (ØP Ú ØQ) in 8 |
10 | ((ØP Þ (ØP Ú ØQ)) Þ (Ø(ØP Ú ØQ) Þ ØØP)) | replace proposition variable B by ØP in 9 |
11 | (Ø(ØP Ú ØQ) Þ ØØP) | modus ponens with 5, 10 |
12 | ((P Ù Q) Þ ØØP) | reverse abbreviation and in 11 at occurence 1 |
13 | (ØØP Þ P) | add proposition hilb6 |
14 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
15 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
16 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
17 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 16 |
18 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 17 |
19 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 18 |
20 | ((D Þ C) Þ ((Ø(P Ù Q) Ú D) Þ (Ø(P Ù Q) Ú C))) | replace proposition variable B by Ø(P Ù Q) in 19 |
21 | ((D Þ P) Þ ((Ø(P Ù Q) Ú D) Þ (Ø(P Ù Q) Ú P))) | replace proposition variable C by P in 20 |
22 | ((ØØP Þ P) Þ ((Ø(P Ù Q) Ú ØØP) Þ (Ø(P Ù Q) Ú P))) | replace proposition variable D by ØØP in 21 |
23 | ((Ø(P Ù Q) Ú ØØP) Þ (Ø(P Ù Q) Ú P)) | modus ponens with 13, 22 |
24 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 14 |
25 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 24 |
26 | ((B Þ ØØP) Þ (ØB Ú ØØP)) | replace proposition variable A by ØØP in 25 |
27 | (((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú ØØP)) | replace proposition variable B by (P Ù Q) in 26 |
28 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
29 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 28 |
30 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 29 |
31 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 30 |
32 | ((D Þ C) Þ ((((P Ù Q) Þ ØØP) Þ D) Þ (((P Ù Q) Þ ØØP) Þ C))) | replace proposition variable B by ((P Ù Q) Þ ØØP) in 31 |
33 | ((D Þ (Ø(P Ù Q) Ú P)) Þ ((((P Ù Q) Þ ØØP) Þ D) Þ (((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú P)))) | replace proposition variable C by (Ø(P Ù Q) Ú P) in 32 |
34 | (((Ø(P Ù Q) Ú ØØP) Þ (Ø(P Ù Q) Ú P)) Þ ((((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú ØØP)) Þ (((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú P)))) | replace proposition variable D by (Ø(P Ù Q) Ú ØØP) in 33 |
35 | ((((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú ØØP)) Þ (((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú P))) | modus ponens with 23, 34 |
36 | (((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú P)) | modus ponens with 27, 35 |
37 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 15 |
38 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 37 |
39 | ((ØB Ú P) Þ (B Þ P)) | replace proposition variable A by P in 38 |
40 | ((Ø(P Ù Q) Ú P) Þ ((P Ù Q) Þ P)) | replace proposition variable B by (P Ù Q) in 39 |
41 | ((D Þ ((P Ù Q) Þ P)) Þ ((((P Ù Q) Þ ØØP) Þ D) Þ (((P Ù Q) Þ ØØP) Þ ((P Ù Q) Þ P)))) | replace proposition variable C by ((P Ù Q) Þ P) in 32 |
42 | (((Ø(P Ù Q) Ú P) Þ ((P Ù Q) Þ P)) Þ ((((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú P)) Þ (((P Ù Q) Þ ØØP) Þ ((P Ù Q) Þ P)))) | replace proposition variable D by (Ø(P Ù Q) Ú P) in 41 |
43 | ((((P Ù Q) Þ ØØP) Þ (Ø(P Ù Q) Ú P)) Þ (((P Ù Q) Þ ØØP) Þ ((P Ù Q) Þ P))) | modus ponens with 40, 42 |
44 | (((P Ù Q) Þ ØØP) Þ ((P Ù Q) Þ P)) | modus ponens with 36, 43 |
45 | ((P Ù Q) Þ P) | modus ponens with 12, 44 |
qed |
Another form of a reduction of a conjunction:
8. Proposition
((P Ù Q) Þ Q) (hilb25)
1 | ((P Ù Q) Þ P) | add proposition hilb24 |
2 | ((P Ù A) Þ P) | replace proposition variable Q by A in 1 |
3 | ((B Ù A) Þ B) | replace proposition variable P by B in 2 |
4 | ((B Ù P) Þ B) | replace proposition variable A by P in 3 |
5 | ((Q Ù P) Þ Q) | replace proposition variable B by Q in 4 |
6 | ((Q Ù P) Þ (P Ù Q)) | add proposition hilb23 |
7 | ((A Ù P) Þ (P Ù A)) | replace proposition variable Q by A in 6 |
8 | ((A Ù B) Þ (B Ù A)) | replace proposition variable P by B in 7 |
9 | ((P Ù B) Þ (B Ù P)) | replace proposition variable A by P in 8 |
10 | ((P Ù Q) Þ (Q Ù P)) | replace proposition variable B by Q in 9 |
11 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
12 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
13 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
14 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 13 |
15 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 14 |
16 | ((B Þ (Q Ù P)) Þ (Ø(Q Ù P) Þ ØB)) | replace proposition variable A by (Q Ù P) in 15 |
17 | (((P Ù Q) Þ (Q Ù P)) Þ (Ø(Q Ù P) Þ Ø(P Ù Q))) | replace proposition variable B by (P Ù Q) in 16 |
18 | (Ø(Q Ù P) Þ Ø(P Ù Q)) | modus ponens with 10, 17 |
19 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
20 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 19 |
21 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 20 |
22 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 21 |
23 | ((D Þ C) Þ ((Q Ú D) Þ (Q Ú C))) | replace proposition variable B by Q in 22 |
24 | ((D Þ Ø(P Ù Q)) Þ ((Q Ú D) Þ (Q Ú Ø(P Ù Q)))) | replace proposition variable C by Ø(P Ù Q) in 23 |
25 | ((Ø(Q Ù P) Þ Ø(P Ù Q)) Þ ((Q Ú Ø(Q Ù P)) Þ (Q Ú Ø(P Ù Q)))) | replace proposition variable D by Ø(Q Ù P) in 24 |
26 | ((Q Ú Ø(Q Ù P)) Þ (Q Ú Ø(P Ù Q))) | modus ponens with 18, 25 |
27 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
28 | ((P Ú A) Þ (A Ú P)) | replace proposition variable Q by A in 27 |
29 | ((B Ú A) Þ (A Ú B)) | replace proposition variable P by B in 28 |
30 | ((B Ú Ø(P Ù Q)) Þ (Ø(P Ù Q) Ú B)) | replace proposition variable A by Ø(P Ù Q) in 29 |
31 | ((Q Ú Ø(P Ù Q)) Þ (Ø(P Ù Q) Ú Q)) | replace proposition variable B by Q in 30 |
32 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
33 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 32 |
34 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 33 |
35 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 34 |
36 | ((D Þ C) Þ (((Q Ú Ø(Q Ù P)) Þ D) Þ ((Q Ú Ø(Q Ù P)) Þ C))) | replace proposition variable B by (Q Ú Ø(Q Ù P)) in 35 |
37 | ((D Þ (Ø(P Ù Q) Ú Q)) Þ (((Q Ú Ø(Q Ù P)) Þ D) Þ ((Q Ú Ø(Q Ù P)) Þ (Ø(P Ù Q) Ú Q)))) | replace proposition variable C by (Ø(P Ù Q) Ú Q) in 36 |
38 | (((Q Ú Ø(P Ù Q)) Þ (Ø(P Ù Q) Ú Q)) Þ (((Q Ú Ø(Q Ù P)) Þ (Q Ú Ø(P Ù Q))) Þ ((Q Ú Ø(Q Ù P)) Þ (Ø(P Ù Q) Ú Q)))) | replace proposition variable D by (Q Ú Ø(P Ù Q)) in 37 |
39 | (((Q Ú Ø(Q Ù P)) Þ (Q Ú Ø(P Ù Q))) Þ ((Q Ú Ø(Q Ù P)) Þ (Ø(P Ù Q) Ú Q))) | modus ponens with 31, 38 |
40 | ((Q Ú Ø(Q Ù P)) Þ (Ø(P Ù Q) Ú Q)) | modus ponens with 26, 39 |
41 | ((B Ú Q) Þ (Q Ú B)) | replace proposition variable A by Q in 29 |
42 | ((Ø(Q Ù P) Ú Q) Þ (Q Ú Ø(Q Ù P))) | replace proposition variable B by Ø(Q Ù P) in 41 |
43 | ((D Þ C) Þ (((Ø(Q Ù P) Ú Q) Þ D) Þ ((Ø(Q Ù P) Ú Q) Þ C))) | replace proposition variable B by (Ø(Q Ù P) Ú Q) in 35 |
44 | ((D Þ (Ø(P Ù Q) Ú Q)) Þ (((Ø(Q Ù P) Ú Q) Þ D) Þ ((Ø(Q Ù P) Ú Q) Þ (Ø(P Ù Q) Ú Q)))) | replace proposition variable C by (Ø(P Ù Q) Ú Q) in 43 |
45 | (((Q Ú Ø(Q Ù P)) Þ (Ø(P Ù Q) Ú Q)) Þ (((Ø(Q Ù P) Ú Q) Þ (Q Ú Ø(Q Ù P))) Þ ((Ø(Q Ù P) Ú Q) Þ (Ø(P Ù Q) Ú Q)))) | replace proposition variable D by (Q Ú Ø(Q Ù P)) in 44 |
46 | (((Ø(Q Ù P) Ú Q) Þ (Q Ú Ø(Q Ù P))) Þ ((Ø(Q Ù P) Ú Q) Þ (Ø(P Ù Q) Ú Q))) | modus ponens with 40, 45 |
47 | ((Ø(Q Ù P) Ú Q) Þ (Ø(P Ù Q) Ú Q)) | modus ponens with 42, 46 |
48 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 11 |
49 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 48 |
50 | ((B Þ Q) Þ (ØB Ú Q)) | replace proposition variable A by Q in 49 |
51 | (((Q Ù P) Þ Q) Þ (Ø(Q Ù P) Ú Q)) | replace proposition variable B by (Q Ù P) in 50 |
52 | ((D Þ C) Þ ((((Q Ù P) Þ Q) Þ D) Þ (((Q Ù P) Þ Q) Þ C))) | replace proposition variable B by ((Q Ù P) Þ Q) in 35 |
53 | ((D Þ (Ø(P Ù Q) Ú Q)) Þ ((((Q Ù P) Þ Q) Þ D) Þ (((Q Ù P) Þ Q) Þ (Ø(P Ù Q) Ú Q)))) | replace proposition variable C by (Ø(P Ù Q) Ú Q) in 52 |
54 | (((Ø(Q Ù P) Ú Q) Þ (Ø(P Ù Q) Ú Q)) Þ ((((Q Ù P) Þ Q) Þ (Ø(Q Ù P) Ú Q)) Þ (((Q Ù P) Þ Q) Þ (Ø(P Ù Q) Ú Q)))) | replace proposition variable D by (Ø(Q Ù P) Ú Q) in 53 |
55 | ((((Q Ù P) Þ Q) Þ (Ø(Q Ù P) Ú Q)) Þ (((Q Ù P) Þ Q) Þ (Ø(P Ù Q) Ú Q))) | modus ponens with 47, 54 |
56 | (((Q Ù P) Þ Q) Þ (Ø(P Ù Q) Ú Q)) | modus ponens with 51, 55 |
57 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 12 |
58 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 57 |
59 | ((ØB Ú Q) Þ (B Þ Q)) | replace proposition variable A by Q in 58 |
60 | ((Ø(P Ù Q) Ú Q) Þ ((P Ù Q) Þ Q)) | replace proposition variable B by (P Ù Q) in 59 |
61 | ((D Þ ((P Ù Q) Þ Q)) Þ ((((Q Ù P) Þ Q) Þ D) Þ (((Q Ù P) Þ Q) Þ ((P Ù Q) Þ Q)))) | replace proposition variable C by ((P Ù Q) Þ Q) in 52 |
62 | (((Ø(P Ù Q) Ú Q) Þ ((P Ù Q) Þ Q)) Þ ((((Q Ù P) Þ Q) Þ (Ø(P Ù Q) Ú Q)) Þ (((Q Ù P) Þ Q) Þ ((P Ù Q) Þ Q)))) | replace proposition variable D by (Ø(P Ù Q) Ú Q) in 61 |
63 | ((((Q Ù P) Þ Q) Þ (Ø(P Ù Q) Ú Q)) Þ (((Q Ù P) Þ Q) Þ ((P Ù Q) Þ Q))) | modus ponens with 60, 62 |
64 | (((Q Ù P) Þ Q) Þ ((P Ù Q) Þ Q)) | modus ponens with 56, 63 |
65 | ((P Ù Q) Þ Q) | modus ponens with 5, 64 |
qed |
The conjunction is associative too (first implication):
9. Proposition
((P Ù (Q Ù A)) Þ ((P Ù Q) Ù A)) (hilb26)
1 | (((P Ú Q) Ú A) Þ (P Ú (Q Ú A))) | add proposition hilb15 |
2 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
3 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 2 |
4 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 3 |
5 | ((B Þ (P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Þ ØB)) | replace proposition variable A by (P Ú (Q Ú A)) in 4 |
6 | ((((P Ú Q) Ú A) Þ (P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A))) | replace proposition variable B by ((P Ú Q) Ú A) in 5 |
7 | (Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) | modus ponens with 1, 6 |
8 | (P Þ ØØP) | add proposition hilb5 |
9 | (B Þ ØØB) | replace proposition variable P by B in 8 |
10 | ((Q Ú A) Þ ØØ(Q Ú A)) | replace proposition variable B by (Q Ú A) in 9 |
11 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
12 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 11 |
13 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 12 |
14 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 13 |
15 | ((D Þ C) Þ ((P Ú D) Þ (P Ú C))) | replace proposition variable B by P in 14 |
16 | ((D Þ ØØ(Q Ú A)) Þ ((P Ú D) Þ (P Ú ØØ(Q Ú A)))) | replace proposition variable C by ØØ(Q Ú A) in 15 |
17 | (((Q Ú A) Þ ØØ(Q Ú A)) Þ ((P Ú (Q Ú A)) Þ (P Ú ØØ(Q Ú A)))) | replace proposition variable D by (Q Ú A) in 16 |
18 | ((P Ú (Q Ú A)) Þ (P Ú ØØ(Q Ú A))) | modus ponens with 10, 17 |
19 | ((P Þ B) Þ (ØB Þ ØP)) | replace proposition variable Q by B in 2 |
20 | ((C Þ B) Þ (ØB Þ ØC)) | replace proposition variable P by C in 19 |
21 | ((C Þ (P Ú ØØ(Q Ú A))) Þ (Ø(P Ú ØØ(Q Ú A)) Þ ØC)) | replace proposition variable B by (P Ú ØØ(Q Ú A)) in 20 |
22 | (((P Ú (Q Ú A)) Þ (P Ú ØØ(Q Ú A))) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(P Ú (Q Ú A)))) | replace proposition variable C by (P Ú (Q Ú A)) in 21 |
23 | (Ø(P Ú ØØ(Q Ú A)) Þ Ø(P Ú (Q Ú A))) | modus ponens with 18, 22 |
24 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
25 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
26 | ((C Þ Ø(P Ú (Q Ú A))) Þ (ØØ(P Ú (Q Ú A)) Þ ØC)) | replace proposition variable B by Ø(P Ú (Q Ú A)) in 20 |
27 | ((Ø(P Ú ØØ(Q Ú A)) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(P Ú (Q Ú A)) Þ ØØ(P Ú ØØ(Q Ú A)))) | replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 26 |
28 | (ØØ(P Ú (Q Ú A)) Þ ØØ(P Ú ØØ(Q Ú A))) | modus ponens with 23, 27 |
29 | ((D Þ C) Þ ((Ø((P Ú Q) Ú A) Ú D) Þ (Ø((P Ú Q) Ú A) Ú C))) | replace proposition variable B by Ø((P Ú Q) Ú A) in 14 |
30 | ((D Þ ØØ(P Ú ØØ(Q Ú A))) Þ ((Ø((P Ú Q) Ú A) Ú D) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))))) | replace proposition variable C by ØØ(P Ú ØØ(Q Ú A)) in 29 |
31 | ((ØØ(P Ú (Q Ú A)) Þ ØØ(P Ú ØØ(Q Ú A))) Þ ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))))) | replace proposition variable D by ØØ(P Ú (Q Ú A)) in 30 |
32 | ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) | modus ponens with 28, 31 |
33 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
34 | ((P Ú B) Þ (B Ú P)) | replace proposition variable Q by B in 33 |
35 | ((C Ú B) Þ (B Ú C)) | replace proposition variable P by C in 34 |
36 | ((C Ú ØØ(P Ú ØØ(Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú C)) | replace proposition variable B by ØØ(P Ú ØØ(Q Ú A)) in 35 |
37 | ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) | replace proposition variable C by Ø((P Ú Q) Ú A) in 36 |
38 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
39 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 38 |
40 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 39 |
41 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 40 |
42 | ((D Þ C) Þ (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ D) Þ ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ C))) | replace proposition variable B by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) in 41 |
43 | ((D Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ D) Þ ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) | replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 42 |
44 | (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) Þ ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) | replace proposition variable D by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) in 43 |
45 | (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) Þ ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) | modus ponens with 37, 44 |
46 | ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) | modus ponens with 32, 45 |
47 | ((C Ú Ø((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Ú C)) | replace proposition variable B by Ø((P Ú Q) Ú A) in 35 |
48 | ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) | replace proposition variable C by ØØ(P Ú (Q Ú A)) in 47 |
49 | ((D Þ C) Þ (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ D) Þ ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ C))) | replace proposition variable B by (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 41 |
50 | ((D Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ D) Þ ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) | replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 49 |
51 | (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) Þ ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) | replace proposition variable D by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) in 50 |
52 | (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) Þ ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) | modus ponens with 46, 51 |
53 | ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) | modus ponens with 48, 52 |
54 | ((P Þ B) Þ (ØP Ú B)) | replace proposition variable Q by B in 24 |
55 | ((C Þ B) Þ (ØC Ú B)) | replace proposition variable P by C in 54 |
56 | ((C Þ Ø((P Ú Q) Ú A)) Þ (ØC Ú Ø((P Ú Q) Ú A))) | replace proposition variable B by Ø((P Ú Q) Ú A) in 55 |
57 | ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) | replace proposition variable C by Ø(P Ú (Q Ú A)) in 56 |
58 | ((D Þ C) Þ (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ C))) | replace proposition variable B by (Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) in 41 |
59 | ((D Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) | replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 58 |
60 | (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) | replace proposition variable D by (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 59 |
61 | (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) | modus ponens with 53, 60 |
62 | ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) | modus ponens with 57, 61 |
63 | ((ØP Ú B) Þ (P Þ B)) | replace proposition variable Q by B in 25 |
64 | ((ØC Ú B) Þ (C Þ B)) | replace proposition variable P by C in 63 |
65 | ((ØC Ú Ø((P Ú Q) Ú A)) Þ (C Þ Ø((P Ú Q) Ú A))) | replace proposition variable B by Ø((P Ú Q) Ú A) in 64 |
66 | ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A))) | replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 65 |
67 | ((D Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A))) Þ (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A))))) | replace proposition variable C by (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) in 58 |
68 | (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A))) Þ (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A))))) | replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 67 |
69 | (((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)))) | modus ponens with 66, 68 |
70 | ((Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A))) | modus ponens with 62, 69 |
71 | (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) | modus ponens with 7, 70 |
72 | (ØØP Þ P) | add proposition hilb6 |
73 | (ØØA Þ A) | replace proposition variable P by A in 72 |
74 | (ØØ(P Ú Q) Þ (P Ú Q)) | replace proposition variable A by (P Ú Q) in 73 |
75 | ((D Þ C) Þ ((A Ú D) Þ (A Ú C))) | replace proposition variable B by A in 14 |
76 | ((D Þ (P Ú Q)) Þ ((A Ú D) Þ (A Ú (P Ú Q)))) | replace proposition variable C by (P Ú Q) in 75 |
77 | ((ØØ(P Ú Q) Þ (P Ú Q)) Þ ((A Ú ØØ(P Ú Q)) Þ (A Ú (P Ú Q)))) | replace proposition variable D by ØØ(P Ú Q) in 76 |
78 | ((A Ú ØØ(P Ú Q)) Þ (A Ú (P Ú Q))) | modus ponens with 74, 77 |
79 | ((C Ú (P Ú Q)) Þ ((P Ú Q) Ú C)) | replace proposition variable B by (P Ú Q) in 35 |
80 | ((A Ú (P Ú Q)) Þ ((P Ú Q) Ú A)) | replace proposition variable C by A in 79 |
81 | ((D Þ C) Þ (((A Ú ØØ(P Ú Q)) Þ D) Þ ((A Ú ØØ(P Ú Q)) Þ C))) | replace proposition variable B by (A Ú ØØ(P Ú Q)) in 41 |
82 | ((D Þ ((P Ú Q) Ú A)) Þ (((A Ú ØØ(P Ú Q)) Þ D) Þ ((A Ú ØØ(P Ú Q)) Þ ((P Ú Q) Ú A)))) | replace proposition variable C by ((P Ú Q) Ú A) in 81 |
83 | (((A Ú (P Ú Q)) Þ ((P Ú Q) Ú A)) Þ (((A Ú ØØ(P Ú Q)) Þ (A Ú (P Ú Q))) Þ ((A Ú ØØ(P Ú Q)) Þ ((P Ú Q) Ú A)))) | replace proposition variable D by (A Ú (P Ú Q)) in 82 |
84 | (((A Ú ØØ(P Ú Q)) Þ (A Ú (P Ú Q))) Þ ((A Ú ØØ(P Ú Q)) Þ ((P Ú Q) Ú A))) | modus ponens with 80, 83 |
85 | ((A Ú ØØ(P Ú Q)) Þ ((P Ú Q) Ú A)) | modus ponens with 78, 84 |
86 | ((C Ú A) Þ (A Ú C)) | replace proposition variable B by A in 35 |
87 | ((ØØ(P Ú Q) Ú A) Þ (A Ú ØØ(P Ú Q))) | replace proposition variable C by ØØ(P Ú Q) in 86 |
88 | ((D Þ C) Þ (((ØØ(P Ú Q) Ú A) Þ D) Þ ((ØØ(P Ú Q) Ú A) Þ C))) | replace proposition variable B by (ØØ(P Ú Q) Ú A) in 41 |
89 | ((D Þ ((P Ú Q) Ú A)) Þ (((ØØ(P Ú Q) Ú A) Þ D) Þ ((ØØ(P Ú Q) Ú A) Þ ((P Ú Q) Ú A)))) | replace proposition variable C by ((P Ú Q) Ú A) in 88 |
90 | (((A Ú ØØ(P Ú Q)) Þ ((P Ú Q) Ú A)) Þ (((ØØ(P Ú Q) Ú A) Þ (A Ú ØØ(P Ú Q))) Þ ((ØØ(P Ú Q) Ú A) Þ ((P Ú Q) Ú A)))) | replace proposition variable D by (A Ú ØØ(P Ú Q)) in 89 |
91 | (((ØØ(P Ú Q) Ú A) Þ (A Ú ØØ(P Ú Q))) Þ ((ØØ(P Ú Q) Ú A) Þ ((P Ú Q) Ú A))) | modus ponens with 85, 90 |
92 | ((ØØ(P Ú Q) Ú A) Þ ((P Ú Q) Ú A)) | modus ponens with 87, 91 |
93 | ((C Þ ((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Þ ØC)) | replace proposition variable B by ((P Ú Q) Ú A) in 20 |
94 | (((ØØ(P Ú Q) Ú A) Þ ((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Þ Ø(ØØ(P Ú Q) Ú A))) | replace proposition variable C by (ØØ(P Ú Q) Ú A) in 93 |
95 | (Ø((P Ú Q) Ú A) Þ Ø(ØØ(P Ú Q) Ú A)) | modus ponens with 92, 94 |
96 | ((D Þ C) Þ ((ØØ(P Ú ØØ(Q Ú A)) Ú D) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú C))) | replace proposition variable B by ØØ(P Ú ØØ(Q Ú A)) in 14 |
97 | ((D Þ Ø(ØØ(P Ú Q) Ú A)) Þ ((ØØ(P Ú ØØ(Q Ú A)) Ú D) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)))) | replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 96 |
98 | ((Ø((P Ú Q) Ú A) Þ Ø(ØØ(P Ú Q) Ú A)) Þ ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)))) | replace proposition variable D by Ø((P Ú Q) Ú A) in 97 |
99 | ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) | modus ponens with 95, 98 |
100 | ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) | replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 56 |
101 | ((D Þ C) Þ (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ C))) | replace proposition variable B by (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) in 41 |
102 | ((D Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) Þ (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))))) | replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) in 101 |
103 | (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) Þ (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))))) | replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 102 |
104 | (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)))) | modus ponens with 99, 103 |
105 | ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) | modus ponens with 100, 104 |
106 | ((ØC Ú Ø(ØØ(P Ú Q) Ú A)) Þ (C Þ Ø(ØØ(P Ú Q) Ú A))) | replace proposition variable B by Ø(ØØ(P Ú Q) Ú A) in 64 |
107 | ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A))) | replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 106 |
108 | ((D Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A))) Þ (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A))))) | replace proposition variable C by (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A)) in 101 |
109 | (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A))) Þ (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A))))) | replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A)) in 108 |
110 | (((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (ØØ(P Ú ØØ(Q Ú A)) Ú Ø(ØØ(P Ú Q) Ú A))) Þ ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A)))) | modus ponens with 107, 109 |
111 | ((Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) Þ (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A))) | modus ponens with 105, 110 |
112 | (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A)) | modus ponens with 71, 111 |
113 | (Ø(P Ú ØØ(Q Ú B)) Þ Ø(ØØ(P Ú Q) Ú B)) | replace proposition variable A by B in 112 |
114 | (Ø(P Ú ØØ(C Ú B)) Þ Ø(ØØ(P Ú C) Ú B)) | replace proposition variable Q by C in 113 |
115 | (Ø(D Ú ØØ(C Ú B)) Þ Ø(ØØ(D Ú C) Ú B)) | replace proposition variable P by D in 114 |
116 | (Ø(D Ú ØØ(C Ú ØA)) Þ Ø(ØØ(D Ú C) Ú ØA)) | replace proposition variable B by ØA in 115 |
117 | (Ø(D Ú ØØ(ØQ Ú ØA)) Þ Ø(ØØ(D Ú ØQ) Ú ØA)) | replace proposition variable C by ØQ in 116 |
118 | (Ø(ØP Ú ØØ(ØQ Ú ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ú ØA)) | replace proposition variable D by ØP in 117 |
119 | ((P Ù Ø(ØQ Ú ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ú ØA)) | reverse abbreviation and in 118 at occurence 1 |
120 | ((P Ù (Q Ù A)) Þ Ø(ØØ(ØP Ú ØQ) Ú ØA)) | reverse abbreviation and in 119 at occurence 1 |
121 | ((P Ù (Q Ù A)) Þ (Ø(ØP Ú ØQ) Ù A)) | reverse abbreviation and in 120 at occurence 1 |
122 | ((P Ù (Q Ù A)) Þ ((P Ù Q) Ù A)) | reverse abbreviation and in 121 at occurence 1 |
qed |
The conjunction is associative (second implication):
10. Proposition
(((P Ù Q) Ù A) Þ (P Ù (Q Ù A))) (hilb27)
1 | ((P Ú (Q Ú A)) Þ ((P Ú Q) Ú A)) | add proposition hilb14 |
2 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
3 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 2 |
4 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 3 |
5 | ((B Þ ((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Þ ØB)) | replace proposition variable A by ((P Ú Q) Ú A) in 4 |
6 | (((P Ú (Q Ú A)) Þ ((P Ú Q) Ú A)) Þ (Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))) | replace proposition variable B by (P Ú (Q Ú A)) in 5 |
7 | (Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) | modus ponens with 1, 6 |
8 | (P Þ ØØP) | add proposition hilb5 |
9 | (A Þ ØØA) | replace proposition variable P by A in 8 |
10 | ((P Ú Q) Þ ØØ(P Ú Q)) | replace proposition variable A by (P Ú Q) in 9 |
11 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
12 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 11 |
13 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 12 |
14 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 13 |
15 | ((D Þ C) Þ ((A Ú D) Þ (A Ú C))) | replace proposition variable B by A in 14 |
16 | ((D Þ ØØ(P Ú Q)) Þ ((A Ú D) Þ (A Ú ØØ(P Ú Q)))) | replace proposition variable C by ØØ(P Ú Q) in 15 |
17 | (((P Ú Q) Þ ØØ(P Ú Q)) Þ ((A Ú (P Ú Q)) Þ (A Ú ØØ(P Ú Q)))) | replace proposition variable D by (P Ú Q) in 16 |
18 | ((A Ú (P Ú Q)) Þ (A Ú ØØ(P Ú Q))) | modus ponens with 10, 17 |
19 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
20 | ((P Ú B) Þ (B Ú P)) | replace proposition variable Q by B in 19 |
21 | ((C Ú B) Þ (B Ú C)) | replace proposition variable P by C in 20 |
22 | ((C Ú ØØ(P Ú Q)) Þ (ØØ(P Ú Q) Ú C)) | replace proposition variable B by ØØ(P Ú Q) in 21 |
23 | ((A Ú ØØ(P Ú Q)) Þ (ØØ(P Ú Q) Ú A)) | replace proposition variable C by A in 22 |
24 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
25 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 24 |
26 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 25 |
27 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 26 |
28 | ((D Þ C) Þ (((A Ú (P Ú Q)) Þ D) Þ ((A Ú (P Ú Q)) Þ C))) | replace proposition variable B by (A Ú (P Ú Q)) in 27 |
29 | ((D Þ (ØØ(P Ú Q) Ú A)) Þ (((A Ú (P Ú Q)) Þ D) Þ ((A Ú (P Ú Q)) Þ (ØØ(P Ú Q) Ú A)))) | replace proposition variable C by (ØØ(P Ú Q) Ú A) in 28 |
30 | (((A Ú ØØ(P Ú Q)) Þ (ØØ(P Ú Q) Ú A)) Þ (((A Ú (P Ú Q)) Þ (A Ú ØØ(P Ú Q))) Þ ((A Ú (P Ú Q)) Þ (ØØ(P Ú Q) Ú A)))) | replace proposition variable D by (A Ú ØØ(P Ú Q)) in 29 |
31 | (((A Ú (P Ú Q)) Þ (A Ú ØØ(P Ú Q))) Þ ((A Ú (P Ú Q)) Þ (ØØ(P Ú Q) Ú A))) | modus ponens with 23, 30 |
32 | ((A Ú (P Ú Q)) Þ (ØØ(P Ú Q) Ú A)) | modus ponens with 18, 31 |
33 | ((C Ú A) Þ (A Ú C)) | replace proposition variable B by A in 21 |
34 | (((P Ú Q) Ú A) Þ (A Ú (P Ú Q))) | replace proposition variable C by (P Ú Q) in 33 |
35 | ((D Þ C) Þ ((((P Ú Q) Ú A) Þ D) Þ (((P Ú Q) Ú A) Þ C))) | replace proposition variable B by ((P Ú Q) Ú A) in 27 |
36 | ((D Þ (ØØ(P Ú Q) Ú A)) Þ ((((P Ú Q) Ú A) Þ D) Þ (((P Ú Q) Ú A) Þ (ØØ(P Ú Q) Ú A)))) | replace proposition variable C by (ØØ(P Ú Q) Ú A) in 35 |
37 | (((A Ú (P Ú Q)) Þ (ØØ(P Ú Q) Ú A)) Þ ((((P Ú Q) Ú A) Þ (A Ú (P Ú Q))) Þ (((P Ú Q) Ú A) Þ (ØØ(P Ú Q) Ú A)))) | replace proposition variable D by (A Ú (P Ú Q)) in 36 |
38 | ((((P Ú Q) Ú A) Þ (A Ú (P Ú Q))) Þ (((P Ú Q) Ú A) Þ (ØØ(P Ú Q) Ú A))) | modus ponens with 32, 37 |
39 | (((P Ú Q) Ú A) Þ (ØØ(P Ú Q) Ú A)) | modus ponens with 34, 38 |
40 | ((P Þ B) Þ (ØB Þ ØP)) | replace proposition variable Q by B in 2 |
41 | ((C Þ B) Þ (ØB Þ ØC)) | replace proposition variable P by C in 40 |
42 | ((C Þ (ØØ(P Ú Q) Ú A)) Þ (Ø(ØØ(P Ú Q) Ú A) Þ ØC)) | replace proposition variable B by (ØØ(P Ú Q) Ú A) in 41 |
43 | ((((P Ú Q) Ú A) Þ (ØØ(P Ú Q) Ú A)) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø((P Ú Q) Ú A))) | replace proposition variable C by ((P Ú Q) Ú A) in 42 |
44 | (Ø(ØØ(P Ú Q) Ú A) Þ Ø((P Ú Q) Ú A)) | modus ponens with 39, 43 |
45 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
46 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
47 | ((C Þ Ø((P Ú Q) Ú A)) Þ (ØØ((P Ú Q) Ú A) Þ ØC)) | replace proposition variable B by Ø((P Ú Q) Ú A) in 41 |
48 | ((Ø(ØØ(P Ú Q) Ú A) Þ Ø((P Ú Q) Ú A)) Þ (ØØ((P Ú Q) Ú A) Þ ØØ(ØØ(P Ú Q) Ú A))) | replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 47 |
49 | (ØØ((P Ú Q) Ú A) Þ ØØ(ØØ(P Ú Q) Ú A)) | modus ponens with 44, 48 |
50 | ((D Þ C) Þ ((Ø(P Ú (Q Ú A)) Ú D) Þ (Ø(P Ú (Q Ú A)) Ú C))) | replace proposition variable B by Ø(P Ú (Q Ú A)) in 14 |
51 | ((D Þ ØØ(ØØ(P Ú Q) Ú A)) Þ ((Ø(P Ú (Q Ú A)) Ú D) Þ (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)))) | replace proposition variable C by ØØ(ØØ(P Ú Q) Ú A) in 50 |
52 | ((ØØ((P Ú Q) Ú A) Þ ØØ(ØØ(P Ú Q) Ú A)) Þ ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)))) | replace proposition variable D by ØØ((P Ú Q) Ú A) in 51 |
53 | ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A))) | modus ponens with 49, 52 |
54 | ((C Ú ØØ(ØØ(P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú C)) | replace proposition variable B by ØØ(ØØ(P Ú Q) Ú A) in 21 |
55 | ((Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) | replace proposition variable C by Ø(P Ú (Q Ú A)) in 54 |
56 | ((D Þ C) Þ (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ C))) | replace proposition variable B by (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) in 27 |
57 | ((D Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ D) Þ ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) | replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 56 |
58 | (((Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A))) Þ ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) | replace proposition variable D by (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A)) in 57 |
59 | (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (Ø(P Ú (Q Ú A)) Ú ØØ(ØØ(P Ú Q) Ú A))) Þ ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))))) | modus ponens with 55, 58 |
60 | ((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) | modus ponens with 53, 59 |
61 | ((C Ú Ø(P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Ú C)) | replace proposition variable B by Ø(P Ú (Q Ú A)) in 21 |
62 | ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A))) | replace proposition variable C by ØØ((P Ú Q) Ú A) in 61 |
63 | ((D Þ C) Þ (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ D) Þ ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ C))) | replace proposition variable B by (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 27 |
64 | ((D Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ D) Þ ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) | replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 63 |
65 | (((Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A))) Þ ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) | replace proposition variable D by (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A)) in 64 |
66 | (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Ú ØØ((P Ú Q) Ú A))) Þ ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))))) | modus ponens with 60, 65 |
67 | ((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) | modus ponens with 62, 66 |
68 | ((P Þ B) Þ (ØP Ú B)) | replace proposition variable Q by B in 45 |
69 | ((C Þ B) Þ (ØC Ú B)) | replace proposition variable P by C in 68 |
70 | ((C Þ Ø(P Ú (Q Ú A))) Þ (ØC Ú Ø(P Ú (Q Ú A)))) | replace proposition variable B by Ø(P Ú (Q Ú A)) in 69 |
71 | ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) | replace proposition variable C by Ø((P Ú Q) Ú A) in 70 |
72 | ((D Þ C) Þ (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ D) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ C))) | replace proposition variable B by (Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) in 27 |
73 | ((D Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ D) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) | replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 72 |
74 | (((ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))))) | replace proposition variable D by (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 73 |
75 | (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ((P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))))) | modus ponens with 67, 74 |
76 | ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) | modus ponens with 71, 75 |
77 | ((ØP Ú B) Þ (P Þ B)) | replace proposition variable Q by B in 46 |
78 | ((ØC Ú B) Þ (C Þ B)) | replace proposition variable P by C in 77 |
79 | ((ØC Ú Ø(P Ú (Q Ú A))) Þ (C Þ Ø(P Ú (Q Ú A)))) | replace proposition variable B by Ø(P Ú (Q Ú A)) in 78 |
80 | ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))) | replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 79 |
81 | ((D Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))) Þ (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ D) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))))) | replace proposition variable C by (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) in 72 |
82 | (((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))) Þ (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))))) | replace proposition variable D by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 81 |
83 | (((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))))) | modus ponens with 80, 82 |
84 | ((Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A)))) | modus ponens with 76, 83 |
85 | (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) | modus ponens with 7, 84 |
86 | (ØØP Þ P) | add proposition hilb6 |
87 | (ØØB Þ B) | replace proposition variable P by B in 86 |
88 | (ØØ(Q Ú A) Þ (Q Ú A)) | replace proposition variable B by (Q Ú A) in 87 |
89 | ((D Þ C) Þ ((P Ú D) Þ (P Ú C))) | replace proposition variable B by P in 14 |
90 | ((D Þ (Q Ú A)) Þ ((P Ú D) Þ (P Ú (Q Ú A)))) | replace proposition variable C by (Q Ú A) in 89 |
91 | ((ØØ(Q Ú A) Þ (Q Ú A)) Þ ((P Ú ØØ(Q Ú A)) Þ (P Ú (Q Ú A)))) | replace proposition variable D by ØØ(Q Ú A) in 90 |
92 | ((P Ú ØØ(Q Ú A)) Þ (P Ú (Q Ú A))) | modus ponens with 88, 91 |
93 | ((C Þ (P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Þ ØC)) | replace proposition variable B by (P Ú (Q Ú A)) in 41 |
94 | (((P Ú ØØ(Q Ú A)) Þ (P Ú (Q Ú A))) Þ (Ø(P Ú (Q Ú A)) Þ Ø(P Ú ØØ(Q Ú A)))) | replace proposition variable C by (P Ú ØØ(Q Ú A)) in 93 |
95 | (Ø(P Ú (Q Ú A)) Þ Ø(P Ú ØØ(Q Ú A))) | modus ponens with 92, 94 |
96 | ((D Þ C) Þ ((ØØ(ØØ(P Ú Q) Ú A) Ú D) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú C))) | replace proposition variable B by ØØ(ØØ(P Ú Q) Ú A) in 14 |
97 | ((D Þ Ø(P Ú ØØ(Q Ú A))) Þ ((ØØ(ØØ(P Ú Q) Ú A) Ú D) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))))) | replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 96 |
98 | ((Ø(P Ú (Q Ú A)) Þ Ø(P Ú ØØ(Q Ú A))) Þ ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))))) | replace proposition variable D by Ø(P Ú (Q Ú A)) in 97 |
99 | ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) | modus ponens with 95, 98 |
100 | ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) | replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 70 |
101 | ((D Þ C) Þ (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ D) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ C))) | replace proposition variable B by (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) in 27 |
102 | ((D Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) Þ (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ D) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))))) | replace proposition variable C by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) in 101 |
103 | (((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) Þ (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))))) | replace proposition variable D by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A))) in 102 |
104 | (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú (Q Ú A)))) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))))) | modus ponens with 99, 103 |
105 | ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) | modus ponens with 100, 104 |
106 | ((ØC Ú Ø(P Ú ØØ(Q Ú A))) Þ (C Þ Ø(P Ú ØØ(Q Ú A)))) | replace proposition variable B by Ø(P Ú ØØ(Q Ú A)) in 78 |
107 | ((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A)))) | replace proposition variable C by Ø(ØØ(P Ú Q) Ú A) in 106 |
108 | ((D Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A)))) Þ (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ D) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A)))))) | replace proposition variable C by (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A))) in 101 |
109 | (((ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A)))) Þ (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A)))))) | replace proposition variable D by (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A))) in 108 |
110 | (((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (ØØ(ØØ(P Ú Q) Ú A) Ú Ø(P Ú ØØ(Q Ú A)))) Þ ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A))))) | modus ponens with 107, 109 |
111 | ((Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Þ (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A)))) | modus ponens with 105, 110 |
112 | (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A))) | modus ponens with 85, 111 |
113 | (Ø(ØØ(P Ú Q) Ú B) Þ Ø(P Ú ØØ(Q Ú B))) | replace proposition variable A by B in 112 |
114 | (Ø(ØØ(P Ú C) Ú B) Þ Ø(P Ú ØØ(C Ú B))) | replace proposition variable Q by C in 113 |
115 | (Ø(ØØ(D Ú C) Ú B) Þ Ø(D Ú ØØ(C Ú B))) | replace proposition variable P by D in 114 |
116 | (Ø(ØØ(D Ú C) Ú ØA) Þ Ø(D Ú ØØ(C Ú ØA))) | replace proposition variable B by ØA in 115 |
117 | (Ø(ØØ(D Ú ØQ) Ú ØA) Þ Ø(D Ú ØØ(ØQ Ú ØA))) | replace proposition variable C by ØQ in 116 |
118 | (Ø(ØØ(ØP Ú ØQ) Ú ØA) Þ Ø(ØP Ú ØØ(ØQ Ú ØA))) | replace proposition variable D by ØP in 117 |
119 | ((Ø(ØP Ú ØQ) Ù A) Þ Ø(ØP Ú ØØ(ØQ Ú ØA))) | reverse abbreviation and in 118 at occurence 1 |
120 | (((P Ù Q) Ù A) Þ Ø(ØP Ú ØØ(ØQ Ú ØA))) | reverse abbreviation and in 119 at occurence 1 |
121 | (((P Ù Q) Ù A) Þ (P Ù Ø(ØQ Ú ØA))) | reverse abbreviation and in 120 at occurence 1 |
122 | (((P Ù Q) Ù A) Þ (P Ù (Q Ù A))) | reverse abbreviation and in 121 at occurence 1 |
qed |
Form for the conjunction rule:
11. Proposition
(P Þ (Q Þ (P Ù Q))) (hilb28)
1 | (P Ú ØP) | add proposition hilb4 |
2 | ((ØP Ú ØQ) Ú Ø(ØP Ú ØQ)) | replace proposition variable P by (ØP Ú ØQ) in 1 |
3 | (((P Ú Q) Ú A) Þ (P Ú (Q Ú A))) | add proposition hilb15 |
4 | (((P Ú Q) Ú B) Þ (P Ú (Q Ú B))) | replace proposition variable A by B in 3 |
5 | (((P Ú C) Ú B) Þ (P Ú (C Ú B))) | replace proposition variable Q by C in 4 |
6 | (((D Ú C) Ú B) Þ (D Ú (C Ú B))) | replace proposition variable P by D in 5 |
7 | (((D Ú C) Ú Ø(ØP Ú ØQ)) Þ (D Ú (C Ú Ø(ØP Ú ØQ)))) | replace proposition variable B by Ø(ØP Ú ØQ) in 6 |
8 | (((D Ú ØQ) Ú Ø(ØP Ú ØQ)) Þ (D Ú (ØQ Ú Ø(ØP Ú ØQ)))) | replace proposition variable C by ØQ in 7 |
9 | (((ØP Ú ØQ) Ú Ø(ØP Ú ØQ)) Þ (ØP Ú (ØQ Ú Ø(ØP Ú ØQ)))) | replace proposition variable D by ØP in 8 |
10 | (ØP Ú (ØQ Ú Ø(ØP Ú ØQ))) | modus ponens with 2, 9 |
11 | (P Þ (ØQ Ú Ø(ØP Ú ØQ))) | reverse abbreviation impl in 10 at occurence 1 |
12 | (P Þ (Q Þ Ø(ØP Ú ØQ))) | reverse abbreviation impl in 11 at occurence 1 |
13 | (P Þ (Q Þ (P Ù Q))) | reverse abbreviation and in 12 at occurence 1 |
qed |
Preconditions could be put together in a conjunction (first direction):
12. Proposition
((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) (hilb29)
1 | (P Þ P) | add proposition hilb2 |
2 | (Q Þ Q) | replace proposition variable P by Q in 1 |
3 | ((P Þ (Q Þ A)) Þ (P Þ (Q Þ A))) | replace proposition variable Q by (P Þ (Q Þ A)) in 2 |
4 | ((P Þ (Q Þ A)) Þ (ØP Ú (Q Þ A))) | use abbreviation impl in 3 at occurence 4 |
5 | ((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) | use abbreviation impl in 4 at occurence 4 |
6 | ((P Ú (Q Ú A)) Þ ((P Ú Q) Ú A)) | add proposition hilb14 |
7 | ((P Ú (Q Ú B)) Þ ((P Ú Q) Ú B)) | replace proposition variable A by B in 6 |
8 | ((P Ú (C Ú B)) Þ ((P Ú C) Ú B)) | replace proposition variable Q by C in 7 |
9 | ((D Ú (C Ú B)) Þ ((D Ú C) Ú B)) | replace proposition variable P by D in 8 |
10 | ((D Ú (C Ú A)) Þ ((D Ú C) Ú A)) | replace proposition variable B by A in 9 |
11 | ((D Ú (ØQ Ú A)) Þ ((D Ú ØQ) Ú A)) | replace proposition variable C by ØQ in 10 |
12 | ((ØP Ú (ØQ Ú A)) Þ ((ØP Ú ØQ) Ú A)) | replace proposition variable D by ØP in 11 |
13 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
14 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
15 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
16 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 15 |
17 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 16 |
18 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 17 |
19 | ((D Þ C) Þ ((Ø(P Þ (Q Þ A)) Ú D) Þ (Ø(P Þ (Q Þ A)) Ú C))) | replace proposition variable B by Ø(P Þ (Q Þ A)) in 18 |
20 | ((D Þ ((ØP Ú ØQ) Ú A)) Þ ((Ø(P Þ (Q Þ A)) Ú D) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)))) | replace proposition variable C by ((ØP Ú ØQ) Ú A) in 19 |
21 | (((ØP Ú (ØQ Ú A)) Þ ((ØP Ú ØQ) Ú A)) Þ ((Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)))) | replace proposition variable D by (ØP Ú (ØQ Ú A)) in 20 |
22 | ((Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) | modus ponens with 12, 21 |
23 | ((P Þ B) Þ (ØP Ú B)) | replace proposition variable Q by B in 13 |
24 | ((C Þ B) Þ (ØC Ú B)) | replace proposition variable P by C in 23 |
25 | ((C Þ (ØP Ú (ØQ Ú A))) Þ (ØC Ú (ØP Ú (ØQ Ú A)))) | replace proposition variable B by (ØP Ú (ØQ Ú A)) in 24 |
26 | (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A)))) | replace proposition variable C by (P Þ (Q Þ A)) in 25 |
27 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
28 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 27 |
29 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 28 |
30 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 29 |
31 | ((D Þ C) Þ ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ D) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ C))) | replace proposition variable B by ((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) in 30 |
32 | ((D Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ D) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))))) | replace proposition variable C by (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) in 31 |
33 | (((Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A)))) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))))) | replace proposition variable D by (Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A))) in 32 |
34 | ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú (ØP Ú (ØQ Ú A)))) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)))) | modus ponens with 22, 33 |
35 | (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) | modus ponens with 26, 34 |
36 | ((ØP Ú B) Þ (P Þ B)) | replace proposition variable Q by B in 14 |
37 | ((ØC Ú B) Þ (C Þ B)) | replace proposition variable P by C in 36 |
38 | ((ØC Ú ((ØP Ú ØQ) Ú A)) Þ (C Þ ((ØP Ú ØQ) Ú A))) | replace proposition variable B by ((ØP Ú ØQ) Ú A) in 37 |
39 | ((Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A))) | replace proposition variable C by (P Þ (Q Þ A)) in 38 |
40 | ((D Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ D) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A))))) | replace proposition variable C by ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) in 31 |
41 | (((Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A))))) | replace proposition variable D by (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) in 40 |
42 | ((((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)))) | modus ponens with 39, 41 |
43 | (((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A))) | modus ponens with 35, 42 |
44 | ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) | modus ponens with 5, 43 |
45 | (P Þ ØØP) | add proposition hilb5 |
46 | (A Þ ØØA) | replace proposition variable P by A in 45 |
47 | ((ØP Ú ØQ) Þ ØØ(ØP Ú ØQ)) | replace proposition variable A by (ØP Ú ØQ) in 46 |
48 | ((D Þ C) Þ ((A Ú D) Þ (A Ú C))) | replace proposition variable B by A in 18 |
49 | ((D Þ ØØ(ØP Ú ØQ)) Þ ((A Ú D) Þ (A Ú ØØ(ØP Ú ØQ)))) | replace proposition variable C by ØØ(ØP Ú ØQ) in 48 |
50 | (((ØP Ú ØQ) Þ ØØ(ØP Ú ØQ)) Þ ((A Ú (ØP Ú ØQ)) Þ (A Ú ØØ(ØP Ú ØQ)))) | replace proposition variable D by (ØP Ú ØQ) in 49 |
51 | ((A Ú (ØP Ú ØQ)) Þ (A Ú ØØ(ØP Ú ØQ))) | modus ponens with 47, 50 |
52 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
53 | ((P Ú B) Þ (B Ú P)) | replace proposition variable Q by B in 52 |
54 | ((C Ú B) Þ (B Ú C)) | replace proposition variable P by C in 53 |
55 | ((C Ú ØØ(ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú C)) | replace proposition variable B by ØØ(ØP Ú ØQ) in 54 |
56 | ((A Ú ØØ(ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A)) | replace proposition variable C by A in 55 |
57 | ((D Þ C) Þ (((A Ú (ØP Ú ØQ)) Þ D) Þ ((A Ú (ØP Ú ØQ)) Þ C))) | replace proposition variable B by (A Ú (ØP Ú ØQ)) in 30 |
58 | ((D Þ (ØØ(ØP Ú ØQ) Ú A)) Þ (((A Ú (ØP Ú ØQ)) Þ D) Þ ((A Ú (ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 57 |
59 | (((A Ú ØØ(ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A)) Þ (((A Ú (ØP Ú ØQ)) Þ (A Ú ØØ(ØP Ú ØQ))) Þ ((A Ú (ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable D by (A Ú ØØ(ØP Ú ØQ)) in 58 |
60 | (((A Ú (ØP Ú ØQ)) Þ (A Ú ØØ(ØP Ú ØQ))) Þ ((A Ú (ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A))) | modus ponens with 56, 59 |
61 | ((A Ú (ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A)) | modus ponens with 51, 60 |
62 | ((C Ú A) Þ (A Ú C)) | replace proposition variable B by A in 54 |
63 | (((ØP Ú ØQ) Ú A) Þ (A Ú (ØP Ú ØQ))) | replace proposition variable C by (ØP Ú ØQ) in 62 |
64 | ((D Þ C) Þ ((((ØP Ú ØQ) Ú A) Þ D) Þ (((ØP Ú ØQ) Ú A) Þ C))) | replace proposition variable B by ((ØP Ú ØQ) Ú A) in 30 |
65 | ((D Þ (ØØ(ØP Ú ØQ) Ú A)) Þ ((((ØP Ú ØQ) Ú A) Þ D) Þ (((ØP Ú ØQ) Ú A) Þ (ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 64 |
66 | (((A Ú (ØP Ú ØQ)) Þ (ØØ(ØP Ú ØQ) Ú A)) Þ ((((ØP Ú ØQ) Ú A) Þ (A Ú (ØP Ú ØQ))) Þ (((ØP Ú ØQ) Ú A) Þ (ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable D by (A Ú (ØP Ú ØQ)) in 65 |
67 | ((((ØP Ú ØQ) Ú A) Þ (A Ú (ØP Ú ØQ))) Þ (((ØP Ú ØQ) Ú A) Þ (ØØ(ØP Ú ØQ) Ú A))) | modus ponens with 61, 66 |
68 | (((ØP Ú ØQ) Ú A) Þ (ØØ(ØP Ú ØQ) Ú A)) | modus ponens with 63, 67 |
69 | ((D Þ (ØØ(ØP Ú ØQ) Ú A)) Þ ((Ø(P Þ (Q Þ A)) Ú D) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 19 |
70 | ((((ØP Ú ØQ) Ú A) Þ (ØØ(ØP Ú ØQ) Ú A)) Þ ((Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable D by ((ØP Ú ØQ) Ú A) in 69 |
71 | ((Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))) | modus ponens with 68, 70 |
72 | ((C Þ ((ØP Ú ØQ) Ú A)) Þ (ØC Ú ((ØP Ú ØQ) Ú A))) | replace proposition variable B by ((ØP Ú ØQ) Ú A) in 24 |
73 | (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) | replace proposition variable C by (P Þ (Q Þ A)) in 72 |
74 | ((D Þ C) Þ ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ D) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ C))) | replace proposition variable B by ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) in 30 |
75 | ((D Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ D) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))))) | replace proposition variable C by (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)) in 74 |
76 | (((Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))))) | replace proposition variable D by (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A)) in 75 |
77 | ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú ((ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)))) | modus ponens with 71, 76 |
78 | (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))) | modus ponens with 73, 77 |
79 | ((ØC Ú (ØØ(ØP Ú ØQ) Ú A)) Þ (C Þ (ØØ(ØP Ú ØQ) Ú A))) | replace proposition variable B by (ØØ(ØP Ú ØQ) Ú A) in 37 |
80 | ((Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A))) | replace proposition variable C by (P Þ (Q Þ A)) in 79 |
81 | ((D Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ D) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A))))) | replace proposition variable C by ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A)) in 74 |
82 | (((Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A))) Þ ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A))))) | replace proposition variable D by (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A)) in 81 |
83 | ((((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø(P Þ (Q Þ A)) Ú (ØØ(ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A)))) | modus ponens with 80, 82 |
84 | (((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A))) | modus ponens with 78, 83 |
85 | ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A)) | modus ponens with 44, 84 |
86 | ((P Þ (Q Þ A)) Þ (Ø(ØP Ú ØQ) Þ A)) | reverse abbreviation impl in 85 at occurence 1 |
87 | ((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) | reverse abbreviation and in 86 at occurence 1 |
qed |
Preconditions could be put together in a conjunction (second direction):
13. Proposition
(((P Ù Q) Þ A) Þ (P Þ (Q Þ A))) (hilb30)
1 | (P Þ P) | add proposition hilb2 |
2 | (Q Þ Q) | replace proposition variable P by Q in 1 |
3 | ((P Þ (Q Þ A)) Þ (P Þ (Q Þ A))) | replace proposition variable Q by (P Þ (Q Þ A)) in 2 |
4 | ((ØP Ú (Q Þ A)) Þ (P Þ (Q Þ A))) | use abbreviation impl in 3 at occurence 2 |
5 | ((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) | use abbreviation impl in 4 at occurence 2 |
6 | (((P Ú Q) Ú A) Þ (P Ú (Q Ú A))) | add proposition hilb15 |
7 | (((P Ú Q) Ú B) Þ (P Ú (Q Ú B))) | replace proposition variable A by B in 6 |
8 | (((P Ú C) Ú B) Þ (P Ú (C Ú B))) | replace proposition variable Q by C in 7 |
9 | (((D Ú C) Ú B) Þ (D Ú (C Ú B))) | replace proposition variable P by D in 8 |
10 | (((D Ú C) Ú A) Þ (D Ú (C Ú A))) | replace proposition variable B by A in 9 |
11 | (((D Ú ØQ) Ú A) Þ (D Ú (ØQ Ú A))) | replace proposition variable C by ØQ in 10 |
12 | (((ØP Ú ØQ) Ú A) Þ (ØP Ú (ØQ Ú A))) | replace proposition variable D by ØP in 11 |
13 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
14 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
15 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
16 | ((P Þ B) Þ (ØB Þ ØP)) | replace proposition variable Q by B in 15 |
17 | ((C Þ B) Þ (ØB Þ ØC)) | replace proposition variable P by C in 16 |
18 | ((C Þ (ØP Ú (ØQ Ú A))) Þ (Ø(ØP Ú (ØQ Ú A)) Þ ØC)) | replace proposition variable B by (ØP Ú (ØQ Ú A)) in 17 |
19 | ((((ØP Ú ØQ) Ú A) Þ (ØP Ú (ØQ Ú A))) Þ (Ø(ØP Ú (ØQ Ú A)) Þ Ø((ØP Ú ØQ) Ú A))) | replace proposition variable C by ((ØP Ú ØQ) Ú A) in 18 |
20 | (Ø(ØP Ú (ØQ Ú A)) Þ Ø((ØP Ú ØQ) Ú A)) | modus ponens with 12, 19 |
21 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
22 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 21 |
23 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 22 |
24 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 23 |
25 | ((D Þ C) Þ (((P Þ (Q Þ A)) Ú D) Þ ((P Þ (Q Þ A)) Ú C))) | replace proposition variable B by (P Þ (Q Þ A)) in 24 |
26 | ((D Þ Ø((ØP Ú ØQ) Ú A)) Þ (((P Þ (Q Þ A)) Ú D) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)))) | replace proposition variable C by Ø((ØP Ú ØQ) Ú A) in 25 |
27 | ((Ø(ØP Ú (ØQ Ú A)) Þ Ø((ØP Ú ØQ) Ú A)) Þ (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)))) | replace proposition variable D by Ø(ØP Ú (ØQ Ú A)) in 26 |
28 | (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A))) | modus ponens with 20, 27 |
29 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
30 | ((P Ú B) Þ (B Ú P)) | replace proposition variable Q by B in 29 |
31 | ((C Ú B) Þ (B Ú C)) | replace proposition variable P by C in 30 |
32 | ((C Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø((ØP Ú ØQ) Ú A) Ú C)) | replace proposition variable B by Ø((ØP Ú ØQ) Ú A) in 31 |
33 | (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | replace proposition variable C by (P Þ (Q Þ A)) in 32 |
34 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
35 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 34 |
36 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 35 |
37 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 36 |
38 | ((D Þ C) Þ ((((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ D) Þ (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ C))) | replace proposition variable B by ((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) in 37 |
39 | ((D Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ D) Þ (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable C by (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 38 |
40 | ((((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable D by ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) in 39 |
41 | ((((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))))) | modus ponens with 33, 40 |
42 | (((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | modus ponens with 28, 41 |
43 | ((C Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú C)) | replace proposition variable B by (P Þ (Q Þ A)) in 31 |
44 | ((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A)))) | replace proposition variable C by Ø(ØP Ú (ØQ Ú A)) in 43 |
45 | ((D Þ C) Þ (((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ D) Þ ((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ C))) | replace proposition variable B by (Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) in 37 |
46 | ((D Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ D) Þ ((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable C by (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 45 |
47 | ((((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A)))) Þ ((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable D by ((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A))) in 46 |
48 | (((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú Ø(ØP Ú (ØQ Ú A)))) Þ ((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))))) | modus ponens with 42, 47 |
49 | ((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | modus ponens with 44, 48 |
50 | ((P Þ B) Þ (ØP Ú B)) | replace proposition variable Q by B in 13 |
51 | ((C Þ B) Þ (ØC Ú B)) | replace proposition variable P by C in 50 |
52 | ((C Þ (P Þ (Q Þ A))) Þ (ØC Ú (P Þ (Q Þ A)))) | replace proposition variable B by (P Þ (Q Þ A)) in 51 |
53 | (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A)))) | replace proposition variable C by (ØP Ú (ØQ Ú A)) in 52 |
54 | ((D Þ C) Þ ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ D) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ C))) | replace proposition variable B by ((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) in 37 |
55 | ((D Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ D) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable C by (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 54 |
56 | (((Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A)))) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable D by (Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A))) in 55 |
57 | ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø(ØP Ú (ØQ Ú A)) Ú (P Þ (Q Þ A)))) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))))) | modus ponens with 49, 56 |
58 | (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | modus ponens with 53, 57 |
59 | ((ØP Ú B) Þ (P Þ B)) | replace proposition variable Q by B in 14 |
60 | ((ØC Ú B) Þ (C Þ B)) | replace proposition variable P by C in 59 |
61 | ((ØC Ú (P Þ (Q Þ A))) Þ (C Þ (P Þ (Q Þ A)))) | replace proposition variable B by (P Þ (Q Þ A)) in 60 |
62 | ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) | replace proposition variable C by ((ØP Ú ØQ) Ú A) in 61 |
63 | ((D Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) Þ ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ D) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))))) | replace proposition variable C by (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) in 54 |
64 | (((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) Þ ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))))) | replace proposition variable D by (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 63 |
65 | ((((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))))) | modus ponens with 62, 64 |
66 | (((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) Þ (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) | modus ponens with 58, 65 |
67 | (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) | modus ponens with 5, 66 |
68 | (ØØP Þ P) | add proposition hilb6 |
69 | (ØØA Þ A) | replace proposition variable P by A in 68 |
70 | (ØØ(ØP Ú ØQ) Þ (ØP Ú ØQ)) | replace proposition variable A by (ØP Ú ØQ) in 69 |
71 | ((D Þ C) Þ ((A Ú D) Þ (A Ú C))) | replace proposition variable B by A in 24 |
72 | ((D Þ (ØP Ú ØQ)) Þ ((A Ú D) Þ (A Ú (ØP Ú ØQ)))) | replace proposition variable C by (ØP Ú ØQ) in 71 |
73 | ((ØØ(ØP Ú ØQ) Þ (ØP Ú ØQ)) Þ ((A Ú ØØ(ØP Ú ØQ)) Þ (A Ú (ØP Ú ØQ)))) | replace proposition variable D by ØØ(ØP Ú ØQ) in 72 |
74 | ((A Ú ØØ(ØP Ú ØQ)) Þ (A Ú (ØP Ú ØQ))) | modus ponens with 70, 73 |
75 | ((C Ú (ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú C)) | replace proposition variable B by (ØP Ú ØQ) in 31 |
76 | ((A Ú (ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A)) | replace proposition variable C by A in 75 |
77 | ((D Þ C) Þ (((A Ú ØØ(ØP Ú ØQ)) Þ D) Þ ((A Ú ØØ(ØP Ú ØQ)) Þ C))) | replace proposition variable B by (A Ú ØØ(ØP Ú ØQ)) in 37 |
78 | ((D Þ ((ØP Ú ØQ) Ú A)) Þ (((A Ú ØØ(ØP Ú ØQ)) Þ D) Þ ((A Ú ØØ(ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A)))) | replace proposition variable C by ((ØP Ú ØQ) Ú A) in 77 |
79 | (((A Ú (ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A)) Þ (((A Ú ØØ(ØP Ú ØQ)) Þ (A Ú (ØP Ú ØQ))) Þ ((A Ú ØØ(ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A)))) | replace proposition variable D by (A Ú (ØP Ú ØQ)) in 78 |
80 | (((A Ú ØØ(ØP Ú ØQ)) Þ (A Ú (ØP Ú ØQ))) Þ ((A Ú ØØ(ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A))) | modus ponens with 76, 79 |
81 | ((A Ú ØØ(ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A)) | modus ponens with 74, 80 |
82 | ((C Ú A) Þ (A Ú C)) | replace proposition variable B by A in 31 |
83 | ((ØØ(ØP Ú ØQ) Ú A) Þ (A Ú ØØ(ØP Ú ØQ))) | replace proposition variable C by ØØ(ØP Ú ØQ) in 82 |
84 | ((D Þ C) Þ (((ØØ(ØP Ú ØQ) Ú A) Þ D) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ C))) | replace proposition variable B by (ØØ(ØP Ú ØQ) Ú A) in 37 |
85 | ((D Þ ((ØP Ú ØQ) Ú A)) Þ (((ØØ(ØP Ú ØQ) Ú A) Þ D) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ ((ØP Ú ØQ) Ú A)))) | replace proposition variable C by ((ØP Ú ØQ) Ú A) in 84 |
86 | (((A Ú ØØ(ØP Ú ØQ)) Þ ((ØP Ú ØQ) Ú A)) Þ (((ØØ(ØP Ú ØQ) Ú A) Þ (A Ú ØØ(ØP Ú ØQ))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ ((ØP Ú ØQ) Ú A)))) | replace proposition variable D by (A Ú ØØ(ØP Ú ØQ)) in 85 |
87 | (((ØØ(ØP Ú ØQ) Ú A) Þ (A Ú ØØ(ØP Ú ØQ))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ ((ØP Ú ØQ) Ú A))) | modus ponens with 81, 86 |
88 | ((ØØ(ØP Ú ØQ) Ú A) Þ ((ØP Ú ØQ) Ú A)) | modus ponens with 83, 87 |
89 | ((C Þ ((ØP Ú ØQ) Ú A)) Þ (Ø((ØP Ú ØQ) Ú A) Þ ØC)) | replace proposition variable B by ((ØP Ú ØQ) Ú A) in 17 |
90 | (((ØØ(ØP Ú ØQ) Ú A) Þ ((ØP Ú ØQ) Ú A)) Þ (Ø((ØP Ú ØQ) Ú A) Þ Ø(ØØ(ØP Ú ØQ) Ú A))) | replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 89 |
91 | (Ø((ØP Ú ØQ) Ú A) Þ Ø(ØØ(ØP Ú ØQ) Ú A)) | modus ponens with 88, 90 |
92 | ((D Þ Ø(ØØ(ØP Ú ØQ) Ú A)) Þ (((P Þ (Q Þ A)) Ú D) Þ ((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable C by Ø(ØØ(ØP Ú ØQ) Ú A) in 25 |
93 | ((Ø((ØP Ú ØQ) Ú A) Þ Ø(ØØ(ØP Ú ØQ) Ú A)) Þ (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)))) | replace proposition variable D by Ø((ØP Ú ØQ) Ú A) in 92 |
94 | (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A))) | modus ponens with 91, 93 |
95 | ((C Ú Ø(ØØ(ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú C)) | replace proposition variable B by Ø(ØØ(ØP Ú ØQ) Ú A) in 31 |
96 | (((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | replace proposition variable C by (P Þ (Q Þ A)) in 95 |
97 | ((D Þ C) Þ ((((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ D) Þ (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ C))) | replace proposition variable B by ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) in 37 |
98 | ((D Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ D) Þ (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable C by (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 97 |
99 | ((((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable D by ((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A)) in 98 |
100 | ((((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ ((P Þ (Q Þ A)) Ú Ø(ØØ(ØP Ú ØQ) Ú A))) Þ (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))))) | modus ponens with 96, 99 |
101 | (((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | modus ponens with 94, 100 |
102 | ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A))) | replace proposition variable C by Ø((ØP Ú ØQ) Ú A) in 43 |
103 | ((D Þ C) Þ (((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ D) Þ ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ C))) | replace proposition variable B by (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 37 |
104 | ((D Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ D) Þ ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable C by (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 103 |
105 | ((((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A))) Þ ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable D by ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A)) in 104 |
106 | (((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ ((P Þ (Q Þ A)) Ú Ø((ØP Ú ØQ) Ú A))) Þ ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))))) | modus ponens with 101, 105 |
107 | ((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | modus ponens with 102, 106 |
108 | ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | replace proposition variable C by ((ØP Ú ØQ) Ú A) in 52 |
109 | ((D Þ C) Þ (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ D) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ C))) | replace proposition variable B by (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) in 37 |
110 | ((D Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ D) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable C by (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 109 |
111 | (((Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))))) | replace proposition variable D by (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 110 |
112 | (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø((ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))))) | modus ponens with 107, 111 |
113 | ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) | modus ponens with 108, 112 |
114 | ((Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) | replace proposition variable C by (ØØ(ØP Ú ØQ) Ú A) in 61 |
115 | ((D Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) Þ (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ D) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))))) | replace proposition variable C by ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) in 109 |
116 | (((Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) Þ (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))))) | replace proposition variable D by (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A))) in 115 |
117 | (((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ (Ø(ØØ(ØP Ú ØQ) Ú A) Ú (P Þ (Q Þ A)))) Þ ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))))) | modus ponens with 114, 116 |
118 | ((((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) Þ ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A)))) | modus ponens with 113, 117 |
119 | ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) | modus ponens with 67, 118 |
120 | ((Ø(ØP Ú ØQ) Þ A) Þ (P Þ (Q Þ A))) | reverse abbreviation impl in 119 at occurence 1 |
121 | (((P Ù Q) Þ A) Þ (P Þ (Q Þ A))) | reverse abbreviation and in 120 at occurence 1 |
qed |
Absorbtion of a conjunction (first direction):
14. Proposition
((P Ù P) Þ P) (hilb31)
1 | ((P Ù Q) Þ P) | add proposition hilb24 |
2 | ((P Ù P) Þ P) | replace proposition variable Q by P in 1 |
qed |
Absorbtion of a conjunction (second direction):
15. Proposition
(P Þ (P Ù P)) (hilb32)
1 | ((P Ú P) Þ P) | add proposition hilb11 |
2 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
3 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 2 |
4 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 3 |
5 | ((B Þ P) Þ (ØP Þ ØB)) | replace proposition variable A by P in 4 |
6 | (((P Ú P) Þ P) Þ (ØP Þ Ø(P Ú P))) | replace proposition variable B by (P Ú P) in 5 |
7 | (ØP Þ Ø(P Ú P)) | modus ponens with 1, 6 |
8 | (ØQ Þ Ø(Q Ú Q)) | replace proposition variable P by Q in 7 |
9 | (ØØP Þ Ø(ØP Ú ØP)) | replace proposition variable Q by ØP in 8 |
10 | (P Þ ØØP) | add proposition hilb5 |
11 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
12 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
13 | ((B Þ ØØP) Þ (ØØØP Þ ØB)) | replace proposition variable A by ØØP in 4 |
14 | ((P Þ ØØP) Þ (ØØØP Þ ØP)) | replace proposition variable B by P in 13 |
15 | (ØØØP Þ ØP) | modus ponens with 10, 14 |
16 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
17 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 16 |
18 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 17 |
19 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 18 |
20 | ((D Þ C) Þ ((Ø(ØP Ú ØP) Ú D) Þ (Ø(ØP Ú ØP) Ú C))) | replace proposition variable B by Ø(ØP Ú ØP) in 19 |
21 | ((D Þ ØP) Þ ((Ø(ØP Ú ØP) Ú D) Þ (Ø(ØP Ú ØP) Ú ØP))) | replace proposition variable C by ØP in 20 |
22 | ((ØØØP Þ ØP) Þ ((Ø(ØP Ú ØP) Ú ØØØP) Þ (Ø(ØP Ú ØP) Ú ØP))) | replace proposition variable D by ØØØP in 21 |
23 | ((Ø(ØP Ú ØP) Ú ØØØP) Þ (Ø(ØP Ú ØP) Ú ØP)) | modus ponens with 15, 22 |
24 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
25 | ((P Ú A) Þ (A Ú P)) | replace proposition variable Q by A in 24 |
26 | ((B Ú A) Þ (A Ú B)) | replace proposition variable P by B in 25 |
27 | ((B Ú ØP) Þ (ØP Ú B)) | replace proposition variable A by ØP in 26 |
28 | ((Ø(ØP Ú ØP) Ú ØP) Þ (ØP Ú Ø(ØP Ú ØP))) | replace proposition variable B by Ø(ØP Ú ØP) in 27 |
29 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
30 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 29 |
31 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 30 |
32 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 31 |
33 | ((D Þ C) Þ (((Ø(ØP Ú ØP) Ú ØØØP) Þ D) Þ ((Ø(ØP Ú ØP) Ú ØØØP) Þ C))) | replace proposition variable B by (Ø(ØP Ú ØP) Ú ØØØP) in 32 |
34 | ((D Þ (ØP Ú Ø(ØP Ú ØP))) Þ (((Ø(ØP Ú ØP) Ú ØØØP) Þ D) Þ ((Ø(ØP Ú ØP) Ú ØØØP) Þ (ØP Ú Ø(ØP Ú ØP))))) | replace proposition variable C by (ØP Ú Ø(ØP Ú ØP)) in 33 |
35 | (((Ø(ØP Ú ØP) Ú ØP) Þ (ØP Ú Ø(ØP Ú ØP))) Þ (((Ø(ØP Ú ØP) Ú ØØØP) Þ (Ø(ØP Ú ØP) Ú ØP)) Þ ((Ø(ØP Ú ØP) Ú ØØØP) Þ (ØP Ú Ø(ØP Ú ØP))))) | replace proposition variable D by (Ø(ØP Ú ØP) Ú ØP) in 34 |
36 | (((Ø(ØP Ú ØP) Ú ØØØP) Þ (Ø(ØP Ú ØP) Ú ØP)) Þ ((Ø(ØP Ú ØP) Ú ØØØP) Þ (ØP Ú Ø(ØP Ú ØP)))) | modus ponens with 28, 35 |
37 | ((Ø(ØP Ú ØP) Ú ØØØP) Þ (ØP Ú Ø(ØP Ú ØP))) | modus ponens with 23, 36 |
38 | ((B Ú Ø(ØP Ú ØP)) Þ (Ø(ØP Ú ØP) Ú B)) | replace proposition variable A by Ø(ØP Ú ØP) in 26 |
39 | ((ØØØP Ú Ø(ØP Ú ØP)) Þ (Ø(ØP Ú ØP) Ú ØØØP)) | replace proposition variable B by ØØØP in 38 |
40 | ((D Þ C) Þ (((ØØØP Ú Ø(ØP Ú ØP)) Þ D) Þ ((ØØØP Ú Ø(ØP Ú ØP)) Þ C))) | replace proposition variable B by (ØØØP Ú Ø(ØP Ú ØP)) in 32 |
41 | ((D Þ (ØP Ú Ø(ØP Ú ØP))) Þ (((ØØØP Ú Ø(ØP Ú ØP)) Þ D) Þ ((ØØØP Ú Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))))) | replace proposition variable C by (ØP Ú Ø(ØP Ú ØP)) in 40 |
42 | (((Ø(ØP Ú ØP) Ú ØØØP) Þ (ØP Ú Ø(ØP Ú ØP))) Þ (((ØØØP Ú Ø(ØP Ú ØP)) Þ (Ø(ØP Ú ØP) Ú ØØØP)) Þ ((ØØØP Ú Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))))) | replace proposition variable D by (Ø(ØP Ú ØP) Ú ØØØP) in 41 |
43 | (((ØØØP Ú Ø(ØP Ú ØP)) Þ (Ø(ØP Ú ØP) Ú ØØØP)) Þ ((ØØØP Ú Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP)))) | modus ponens with 37, 42 |
44 | ((ØØØP Ú Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))) | modus ponens with 39, 43 |
45 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 11 |
46 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 45 |
47 | ((B Þ Ø(ØP Ú ØP)) Þ (ØB Ú Ø(ØP Ú ØP))) | replace proposition variable A by Ø(ØP Ú ØP) in 46 |
48 | ((ØØP Þ Ø(ØP Ú ØP)) Þ (ØØØP Ú Ø(ØP Ú ØP))) | replace proposition variable B by ØØP in 47 |
49 | ((D Þ C) Þ (((ØØP Þ Ø(ØP Ú ØP)) Þ D) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ C))) | replace proposition variable B by (ØØP Þ Ø(ØP Ú ØP)) in 32 |
50 | ((D Þ (ØP Ú Ø(ØP Ú ØP))) Þ (((ØØP Þ Ø(ØP Ú ØP)) Þ D) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))))) | replace proposition variable C by (ØP Ú Ø(ØP Ú ØP)) in 49 |
51 | (((ØØØP Ú Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))) Þ (((ØØP Þ Ø(ØP Ú ØP)) Þ (ØØØP Ú Ø(ØP Ú ØP))) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))))) | replace proposition variable D by (ØØØP Ú Ø(ØP Ú ØP)) in 50 |
52 | (((ØØP Þ Ø(ØP Ú ØP)) Þ (ØØØP Ú Ø(ØP Ú ØP))) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP)))) | modus ponens with 44, 51 |
53 | ((ØØP Þ Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))) | modus ponens with 48, 52 |
54 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 12 |
55 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 54 |
56 | ((ØB Ú Ø(ØP Ú ØP)) Þ (B Þ Ø(ØP Ú ØP))) | replace proposition variable A by Ø(ØP Ú ØP) in 55 |
57 | ((ØP Ú Ø(ØP Ú ØP)) Þ (P Þ Ø(ØP Ú ØP))) | replace proposition variable B by P in 56 |
58 | ((D Þ (P Þ Ø(ØP Ú ØP))) Þ (((ØØP Þ Ø(ØP Ú ØP)) Þ D) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ (P Þ Ø(ØP Ú ØP))))) | replace proposition variable C by (P Þ Ø(ØP Ú ØP)) in 49 |
59 | (((ØP Ú Ø(ØP Ú ØP)) Þ (P Þ Ø(ØP Ú ØP))) Þ (((ØØP Þ Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ (P Þ Ø(ØP Ú ØP))))) | replace proposition variable D by (ØP Ú Ø(ØP Ú ØP)) in 58 |
60 | (((ØØP Þ Ø(ØP Ú ØP)) Þ (ØP Ú Ø(ØP Ú ØP))) Þ ((ØØP Þ Ø(ØP Ú ØP)) Þ (P Þ Ø(ØP Ú ØP)))) | modus ponens with 57, 59 |
61 | ((ØØP Þ Ø(ØP Ú ØP)) Þ (P Þ Ø(ØP Ú ØP))) | modus ponens with 53, 60 |
62 | (P Þ Ø(ØP Ú ØP)) | modus ponens with 9, 61 |
63 | (P Þ (P Ù P)) | reverse abbreviation and in 62 at occurence 1 |
qed |
Absorbtion of identical preconditions (first direction):
16. Proposition
((P Þ (P Þ Q)) Þ (P Þ Q)) (hilb33)
1 | ((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) | add proposition hilb29 |
2 | ((P Þ (Q Þ B)) Þ ((P Ù Q) Þ B)) | replace proposition variable A by B in 1 |
3 | ((P Þ (C Þ B)) Þ ((P Ù C) Þ B)) | replace proposition variable Q by C in 2 |
4 | ((D Þ (C Þ B)) Þ ((D Ù C) Þ B)) | replace proposition variable P by D in 3 |
5 | ((D Þ (C Þ Q)) Þ ((D Ù C) Þ Q)) | replace proposition variable B by Q in 4 |
6 | ((D Þ (P Þ Q)) Þ ((D Ù P) Þ Q)) | replace proposition variable C by P in 5 |
7 | ((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) | replace proposition variable D by P in 6 |
8 | (P Þ (P Ù P)) | add proposition hilb32 |
9 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
10 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
11 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
12 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 11 |
13 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 12 |
14 | ((B Þ (P Ù P)) Þ (Ø(P Ù P) Þ ØB)) | replace proposition variable A by (P Ù P) in 13 |
15 | ((P Þ (P Ù P)) Þ (Ø(P Ù P) Þ ØP)) | replace proposition variable B by P in 14 |
16 | (Ø(P Ù P) Þ ØP) | modus ponens with 8, 15 |
17 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
18 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 17 |
19 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 18 |
20 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 19 |
21 | ((D Þ C) Þ ((Q Ú D) Þ (Q Ú C))) | replace proposition variable B by Q in 20 |
22 | ((D Þ ØP) Þ ((Q Ú D) Þ (Q Ú ØP))) | replace proposition variable C by ØP in 21 |
23 | ((Ø(P Ù P) Þ ØP) Þ ((Q Ú Ø(P Ù P)) Þ (Q Ú ØP))) | replace proposition variable D by Ø(P Ù P) in 22 |
24 | ((Q Ú Ø(P Ù P)) Þ (Q Ú ØP)) | modus ponens with 16, 23 |
25 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
26 | ((P Ú A) Þ (A Ú P)) | replace proposition variable Q by A in 25 |
27 | ((B Ú A) Þ (A Ú B)) | replace proposition variable P by B in 26 |
28 | ((B Ú ØP) Þ (ØP Ú B)) | replace proposition variable A by ØP in 27 |
29 | ((Q Ú ØP) Þ (ØP Ú Q)) | replace proposition variable B by Q in 28 |
30 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
31 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 30 |
32 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 31 |
33 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 32 |
34 | ((D Þ C) Þ (((Q Ú Ø(P Ù P)) Þ D) Þ ((Q Ú Ø(P Ù P)) Þ C))) | replace proposition variable B by (Q Ú Ø(P Ù P)) in 33 |
35 | ((D Þ (ØP Ú Q)) Þ (((Q Ú Ø(P Ù P)) Þ D) Þ ((Q Ú Ø(P Ù P)) Þ (ØP Ú Q)))) | replace proposition variable C by (ØP Ú Q) in 34 |
36 | (((Q Ú ØP) Þ (ØP Ú Q)) Þ (((Q Ú Ø(P Ù P)) Þ (Q Ú ØP)) Þ ((Q Ú Ø(P Ù P)) Þ (ØP Ú Q)))) | replace proposition variable D by (Q Ú ØP) in 35 |
37 | (((Q Ú Ø(P Ù P)) Þ (Q Ú ØP)) Þ ((Q Ú Ø(P Ù P)) Þ (ØP Ú Q))) | modus ponens with 29, 36 |
38 | ((Q Ú Ø(P Ù P)) Þ (ØP Ú Q)) | modus ponens with 24, 37 |
39 | ((B Ú Q) Þ (Q Ú B)) | replace proposition variable A by Q in 27 |
40 | ((Ø(P Ù P) Ú Q) Þ (Q Ú Ø(P Ù P))) | replace proposition variable B by Ø(P Ù P) in 39 |
41 | ((D Þ C) Þ (((Ø(P Ù P) Ú Q) Þ D) Þ ((Ø(P Ù P) Ú Q) Þ C))) | replace proposition variable B by (Ø(P Ù P) Ú Q) in 33 |
42 | ((D Þ (ØP Ú Q)) Þ (((Ø(P Ù P) Ú Q) Þ D) Þ ((Ø(P Ù P) Ú Q) Þ (ØP Ú Q)))) | replace proposition variable C by (ØP Ú Q) in 41 |
43 | (((Q Ú Ø(P Ù P)) Þ (ØP Ú Q)) Þ (((Ø(P Ù P) Ú Q) Þ (Q Ú Ø(P Ù P))) Þ ((Ø(P Ù P) Ú Q) Þ (ØP Ú Q)))) | replace proposition variable D by (Q Ú Ø(P Ù P)) in 42 |
44 | (((Ø(P Ù P) Ú Q) Þ (Q Ú Ø(P Ù P))) Þ ((Ø(P Ù P) Ú Q) Þ (ØP Ú Q))) | modus ponens with 38, 43 |
45 | ((Ø(P Ù P) Ú Q) Þ (ØP Ú Q)) | modus ponens with 40, 44 |
46 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 9 |
47 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 46 |
48 | ((B Þ Q) Þ (ØB Ú Q)) | replace proposition variable A by Q in 47 |
49 | (((P Ù P) Þ Q) Þ (Ø(P Ù P) Ú Q)) | replace proposition variable B by (P Ù P) in 48 |
50 | ((D Þ C) Þ ((((P Ù P) Þ Q) Þ D) Þ (((P Ù P) Þ Q) Þ C))) | replace proposition variable B by ((P Ù P) Þ Q) in 33 |
51 | ((D Þ (ØP Ú Q)) Þ ((((P Ù P) Þ Q) Þ D) Þ (((P Ù P) Þ Q) Þ (ØP Ú Q)))) | replace proposition variable C by (ØP Ú Q) in 50 |
52 | (((Ø(P Ù P) Ú Q) Þ (ØP Ú Q)) Þ ((((P Ù P) Þ Q) Þ (Ø(P Ù P) Ú Q)) Þ (((P Ù P) Þ Q) Þ (ØP Ú Q)))) | replace proposition variable D by (Ø(P Ù P) Ú Q) in 51 |
53 | ((((P Ù P) Þ Q) Þ (Ø(P Ù P) Ú Q)) Þ (((P Ù P) Þ Q) Þ (ØP Ú Q))) | modus ponens with 45, 52 |
54 | (((P Ù P) Þ Q) Þ (ØP Ú Q)) | modus ponens with 49, 53 |
55 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 10 |
56 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 55 |
57 | ((D Þ (P Þ Q)) Þ ((((P Ù P) Þ Q) Þ D) Þ (((P Ù P) Þ Q) Þ (P Þ Q)))) | replace proposition variable C by (P Þ Q) in 50 |
58 | (((ØP Ú Q) Þ (P Þ Q)) Þ ((((P Ù P) Þ Q) Þ (ØP Ú Q)) Þ (((P Ù P) Þ Q) Þ (P Þ Q)))) | replace proposition variable D by (ØP Ú Q) in 57 |
59 | ((((P Ù P) Þ Q) Þ (ØP Ú Q)) Þ (((P Ù P) Þ Q) Þ (P Þ Q))) | modus ponens with 10, 58 |
60 | (((P Ù P) Þ Q) Þ (P Þ Q)) | modus ponens with 54, 59 |
61 | ((D Þ C) Þ ((Ø(P Þ (P Þ Q)) Ú D) Þ (Ø(P Þ (P Þ Q)) Ú C))) | replace proposition variable B by Ø(P Þ (P Þ Q)) in 20 |
62 | ((D Þ (P Þ Q)) Þ ((Ø(P Þ (P Þ Q)) Ú D) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q)))) | replace proposition variable C by (P Þ Q) in 61 |
63 | ((((P Ù P) Þ Q) Þ (P Þ Q)) Þ ((Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q)))) | replace proposition variable D by ((P Ù P) Þ Q) in 62 |
64 | ((Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))) | modus ponens with 60, 63 |
65 | ((B Þ ((P Ù P) Þ Q)) Þ (ØB Ú ((P Ù P) Þ Q))) | replace proposition variable A by ((P Ù P) Þ Q) in 47 |
66 | (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q))) | replace proposition variable B by (P Þ (P Þ Q)) in 65 |
67 | ((D Þ C) Þ ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ D) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ C))) | replace proposition variable B by ((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) in 33 |
68 | ((D Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))) Þ ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ D) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))))) | replace proposition variable C by (Ø(P Þ (P Þ Q)) Ú (P Þ Q)) in 67 |
69 | (((Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))) Þ ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q))) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))))) | replace proposition variable D by (Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q)) in 68 |
70 | ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú ((P Ù P) Þ Q))) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q)))) | modus ponens with 64, 69 |
71 | (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))) | modus ponens with 66, 70 |
72 | ((ØB Ú (P Þ Q)) Þ (B Þ (P Þ Q))) | replace proposition variable A by (P Þ Q) in 56 |
73 | ((Ø(P Þ (P Þ Q)) Ú (P Þ Q)) Þ ((P Þ (P Þ Q)) Þ (P Þ Q))) | replace proposition variable B by (P Þ (P Þ Q)) in 72 |
74 | ((D Þ ((P Þ (P Þ Q)) Þ (P Þ Q))) Þ ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ D) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Þ (P Þ Q))))) | replace proposition variable C by ((P Þ (P Þ Q)) Þ (P Þ Q)) in 67 |
75 | (((Ø(P Þ (P Þ Q)) Ú (P Þ Q)) Þ ((P Þ (P Þ Q)) Þ (P Þ Q))) Þ ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Þ (P Þ Q))))) | replace proposition variable D by (Ø(P Þ (P Þ Q)) Ú (P Þ Q)) in 74 |
76 | ((((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ (Ø(P Þ (P Þ Q)) Ú (P Þ Q))) Þ (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Þ (P Þ Q)))) | modus ponens with 73, 75 |
77 | (((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Þ (P Þ Q))) | modus ponens with 71, 76 |
78 | ((P Þ (P Þ Q)) Þ (P Þ Q)) | modus ponens with 7, 77 |
qed |
Absorbtion of identical preconditions (second direction):
17. Proposition
((P Þ Q) Þ (P Þ (P Þ Q))) (hilb34)
1 | (((P Ù Q) Þ A) Þ (P Þ (Q Þ A))) | add proposition hilb30 |
2 | (((P Ù Q) Þ B) Þ (P Þ (Q Þ B))) | replace proposition variable A by B in 1 |
3 | (((P Ù C) Þ B) Þ (P Þ (C Þ B))) | replace proposition variable Q by C in 2 |
4 | (((D Ù C) Þ B) Þ (D Þ (C Þ B))) | replace proposition variable P by D in 3 |
5 | (((D Ù C) Þ Q) Þ (D Þ (C Þ Q))) | replace proposition variable B by Q in 4 |
6 | (((D Ù P) Þ Q) Þ (D Þ (P Þ Q))) | replace proposition variable C by P in 5 |
7 | (((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) | replace proposition variable D by P in 6 |
8 | ((P Ù P) Þ P) | add proposition hilb31 |
9 | ((P Þ Q) Þ (ØP Ú Q)) | add proposition defimpl1 |
10 | ((ØP Ú Q) Þ (P Þ Q)) | add proposition defimpl2 |
11 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
12 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 11 |
13 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 12 |
14 | ((B Þ P) Þ (ØP Þ ØB)) | replace proposition variable A by P in 13 |
15 | (((P Ù P) Þ P) Þ (ØP Þ Ø(P Ù P))) | replace proposition variable B by (P Ù P) in 14 |
16 | (ØP Þ Ø(P Ù P)) | modus ponens with 8, 15 |
17 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
18 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 17 |
19 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 18 |
20 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 19 |
21 | ((D Þ C) Þ ((Q Ú D) Þ (Q Ú C))) | replace proposition variable B by Q in 20 |
22 | ((D Þ Ø(P Ù P)) Þ ((Q Ú D) Þ (Q Ú Ø(P Ù P)))) | replace proposition variable C by Ø(P Ù P) in 21 |
23 | ((ØP Þ Ø(P Ù P)) Þ ((Q Ú ØP) Þ (Q Ú Ø(P Ù P)))) | replace proposition variable D by ØP in 22 |
24 | ((Q Ú ØP) Þ (Q Ú Ø(P Ù P))) | modus ponens with 16, 23 |
25 | ((P Ú Q) Þ (Q Ú P)) | add axiom axiom3 |
26 | ((P Ú A) Þ (A Ú P)) | replace proposition variable Q by A in 25 |
27 | ((B Ú A) Þ (A Ú B)) | replace proposition variable P by B in 26 |
28 | ((B Ú Ø(P Ù P)) Þ (Ø(P Ù P) Ú B)) | replace proposition variable A by Ø(P Ù P) in 27 |
29 | ((Q Ú Ø(P Ù P)) Þ (Ø(P Ù P) Ú Q)) | replace proposition variable B by Q in 28 |
30 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
31 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 30 |
32 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 31 |
33 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 32 |
34 | ((D Þ C) Þ (((Q Ú ØP) Þ D) Þ ((Q Ú ØP) Þ C))) | replace proposition variable B by (Q Ú ØP) in 33 |
35 | ((D Þ (Ø(P Ù P) Ú Q)) Þ (((Q Ú ØP) Þ D) Þ ((Q Ú ØP) Þ (Ø(P Ù P) Ú Q)))) | replace proposition variable C by (Ø(P Ù P) Ú Q) in 34 |
36 | (((Q Ú Ø(P Ù P)) Þ (Ø(P Ù P) Ú Q)) Þ (((Q Ú ØP) Þ (Q Ú Ø(P Ù P))) Þ ((Q Ú ØP) Þ (Ø(P Ù P) Ú Q)))) | replace proposition variable D by (Q Ú Ø(P Ù P)) in 35 |
37 | (((Q Ú ØP) Þ (Q Ú Ø(P Ù P))) Þ ((Q Ú ØP) Þ (Ø(P Ù P) Ú Q))) | modus ponens with 29, 36 |
38 | ((Q Ú ØP) Þ (Ø(P Ù P) Ú Q)) | modus ponens with 24, 37 |
39 | ((B Ú Q) Þ (Q Ú B)) | replace proposition variable A by Q in 27 |
40 | ((ØP Ú Q) Þ (Q Ú ØP)) | replace proposition variable B by ØP in 39 |
41 | ((D Þ C) Þ (((ØP Ú Q) Þ D) Þ ((ØP Ú Q) Þ C))) | replace proposition variable B by (ØP Ú Q) in 33 |
42 | ((D Þ (Ø(P Ù P) Ú Q)) Þ (((ØP Ú Q) Þ D) Þ ((ØP Ú Q) Þ (Ø(P Ù P) Ú Q)))) | replace proposition variable C by (Ø(P Ù P) Ú Q) in 41 |
43 | (((Q Ú ØP) Þ (Ø(P Ù P) Ú Q)) Þ (((ØP Ú Q) Þ (Q Ú ØP)) Þ ((ØP Ú Q) Þ (Ø(P Ù P) Ú Q)))) | replace proposition variable D by (Q Ú ØP) in 42 |
44 | (((ØP Ú Q) Þ (Q Ú ØP)) Þ ((ØP Ú Q) Þ (Ø(P Ù P) Ú Q))) | modus ponens with 38, 43 |
45 | ((ØP Ú Q) Þ (Ø(P Ù P) Ú Q)) | modus ponens with 40, 44 |
46 | ((P Þ A) Þ (ØP Ú A)) | replace proposition variable Q by A in 9 |
47 | ((B Þ A) Þ (ØB Ú A)) | replace proposition variable P by B in 46 |
48 | ((D Þ C) Þ (((P Þ Q) Þ D) Þ ((P Þ Q) Þ C))) | replace proposition variable B by (P Þ Q) in 33 |
49 | ((D Þ (Ø(P Ù P) Ú Q)) Þ (((P Þ Q) Þ D) Þ ((P Þ Q) Þ (Ø(P Ù P) Ú Q)))) | replace proposition variable C by (Ø(P Ù P) Ú Q) in 48 |
50 | (((ØP Ú Q) Þ (Ø(P Ù P) Ú Q)) Þ (((P Þ Q) Þ (ØP Ú Q)) Þ ((P Þ Q) Þ (Ø(P Ù P) Ú Q)))) | replace proposition variable D by (ØP Ú Q) in 49 |
51 | (((P Þ Q) Þ (ØP Ú Q)) Þ ((P Þ Q) Þ (Ø(P Ù P) Ú Q))) | modus ponens with 45, 50 |
52 | ((P Þ Q) Þ (Ø(P Ù P) Ú Q)) | modus ponens with 9, 51 |
53 | ((ØP Ú A) Þ (P Þ A)) | replace proposition variable Q by A in 10 |
54 | ((ØB Ú A) Þ (B Þ A)) | replace proposition variable P by B in 53 |
55 | ((ØB Ú Q) Þ (B Þ Q)) | replace proposition variable A by Q in 54 |
56 | ((Ø(P Ù P) Ú Q) Þ ((P Ù P) Þ Q)) | replace proposition variable B by (P Ù P) in 55 |
57 | ((D Þ ((P Ù P) Þ Q)) Þ (((P Þ Q) Þ D) Þ ((P Þ Q) Þ ((P Ù P) Þ Q)))) | replace proposition variable C by ((P Ù P) Þ Q) in 48 |
58 | (((Ø(P Ù P) Ú Q) Þ ((P Ù P) Þ Q)) Þ (((P Þ Q) Þ (Ø(P Ù P) Ú Q)) Þ ((P Þ Q) Þ ((P Ù P) Þ Q)))) | replace proposition variable D by (Ø(P Ù P) Ú Q) in 57 |
59 | (((P Þ Q) Þ (Ø(P Ù P) Ú Q)) Þ ((P Þ Q) Þ ((P Ù P) Þ Q))) | modus ponens with 56, 58 |
60 | ((P Þ Q) Þ ((P Ù P) Þ Q)) | modus ponens with 52, 59 |
61 | ((B Þ ((P Ù P) Þ Q)) Þ (Ø((P Ù P) Þ Q) Þ ØB)) | replace proposition variable A by ((P Ù P) Þ Q) in 13 |
62 | (((P Þ Q) Þ ((P Ù P) Þ Q)) Þ (Ø((P Ù P) Þ Q) Þ Ø(P Þ Q))) | replace proposition variable B by (P Þ Q) in 61 |
63 | (Ø((P Ù P) Þ Q) Þ Ø(P Þ Q)) | modus ponens with 60, 62 |
64 | ((D Þ C) Þ (((P Þ (P Þ Q)) Ú D) Þ ((P Þ (P Þ Q)) Ú C))) | replace proposition variable B by (P Þ (P Þ Q)) in 20 |
65 | ((D Þ Ø(P Þ Q)) Þ (((P Þ (P Þ Q)) Ú D) Þ ((P Þ (P Þ Q)) Ú Ø(P Þ Q)))) | replace proposition variable C by Ø(P Þ Q) in 64 |
66 | ((Ø((P Ù P) Þ Q) Þ Ø(P Þ Q)) Þ (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Ú Ø(P Þ Q)))) | replace proposition variable D by Ø((P Ù P) Þ Q) in 65 |
67 | (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Ú Ø(P Þ Q))) | modus ponens with 63, 66 |
68 | ((B Ú Ø(P Þ Q)) Þ (Ø(P Þ Q) Ú B)) | replace proposition variable A by Ø(P Þ Q) in 27 |
69 | (((P Þ (P Þ Q)) Ú Ø(P Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) | replace proposition variable B by (P Þ (P Þ Q)) in 68 |
70 | ((D Þ C) Þ ((((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ D) Þ (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ C))) | replace proposition variable B by ((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) in 33 |
71 | ((D Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ ((((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ D) Þ (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))))) | replace proposition variable C by (Ø(P Þ Q) Ú (P Þ (P Þ Q))) in 70 |
72 | ((((P Þ (P Þ Q)) Ú Ø(P Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ ((((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Ú Ø(P Þ Q))) Þ (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))))) | replace proposition variable D by ((P Þ (P Þ Q)) Ú Ø(P Þ Q)) in 71 |
73 | ((((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ ((P Þ (P Þ Q)) Ú Ø(P Þ Q))) Þ (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q))))) | modus ponens with 69, 72 |
74 | (((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) | modus ponens with 67, 73 |
75 | ((B Ú (P Þ (P Þ Q))) Þ ((P Þ (P Þ Q)) Ú B)) | replace proposition variable A by (P Þ (P Þ Q)) in 27 |
76 | ((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ ((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q))) | replace proposition variable B by Ø((P Ù P) Þ Q) in 75 |
77 | ((D Þ C) Þ (((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ D) Þ ((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ C))) | replace proposition variable B by (Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) in 33 |
78 | ((D Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ (((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ D) Þ ((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))))) | replace proposition variable C by (Ø(P Þ Q) Ú (P Þ (P Þ Q))) in 77 |
79 | ((((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ (((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ ((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q))) Þ ((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))))) | replace proposition variable D by ((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q)) in 78 |
80 | (((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ ((P Þ (P Þ Q)) Ú Ø((P Ù P) Þ Q))) Þ ((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q))))) | modus ponens with 74, 79 |
81 | ((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) | modus ponens with 76, 80 |
82 | ((B Þ (P Þ (P Þ Q))) Þ (ØB Ú (P Þ (P Þ Q)))) | replace proposition variable A by (P Þ (P Þ Q)) in 47 |
83 | ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q)))) | replace proposition variable B by ((P Ù P) Þ Q) in 82 |
84 | ((D Þ C) Þ (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ D) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ C))) | replace proposition variable B by (((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) in 33 |
85 | ((D Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ D) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))))) | replace proposition variable C by (Ø(P Þ Q) Ú (P Þ (P Þ Q))) in 84 |
86 | (((Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q)))) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))))) | replace proposition variable D by (Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q))) in 85 |
87 | (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø((P Ù P) Þ Q) Ú (P Þ (P Þ Q)))) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q))))) | modus ponens with 81, 86 |
88 | ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) | modus ponens with 83, 87 |
89 | ((ØB Ú (P Þ (P Þ Q))) Þ (B Þ (P Þ (P Þ Q)))) | replace proposition variable A by (P Þ (P Þ Q)) in 54 |
90 | ((Ø(P Þ Q) Ú (P Þ (P Þ Q))) Þ ((P Þ Q) Þ (P Þ (P Þ Q)))) | replace proposition variable B by (P Þ Q) in 89 |
91 | ((D Þ ((P Þ Q) Þ (P Þ (P Þ Q)))) Þ (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ D) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ ((P Þ Q) Þ (P Þ (P Þ Q)))))) | replace proposition variable C by ((P Þ Q) Þ (P Þ (P Þ Q))) in 84 |
92 | (((Ø(P Þ Q) Ú (P Þ (P Þ Q))) Þ ((P Þ Q) Þ (P Þ (P Þ Q)))) Þ (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ ((P Þ Q) Þ (P Þ (P Þ Q)))))) | replace proposition variable D by (Ø(P Þ Q) Ú (P Þ (P Þ Q))) in 91 |
93 | (((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ (Ø(P Þ Q) Ú (P Þ (P Þ Q)))) Þ ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ ((P Þ Q) Þ (P Þ (P Þ Q))))) | modus ponens with 90, 92 |
94 | ((((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Þ ((P Þ Q) Þ (P Þ (P Þ Q)))) | modus ponens with 88, 93 |
95 | ((P Þ Q) Þ (P Þ (P Þ Q))) | modus ponens with 7, 94 |
qed |
This module is used by the following modules: