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 |