First we prove a simple implication, that follows directly from the fourth axiom:
1. Proposition
(P → Q) → ((A → P) → (A → Q)) (hilb1)
1 | (P → Q) → ((A ∨ P) → (A ∨ Q)) | add axiom axiom4 |
2 | (P → Q) → ((¬A ∨ P) → (¬A ∨ Q)) | replace proposition variable A by ¬A in 1 |
3 | (P → Q) → ((A → P) → (¬A ∨ Q)) | reverse abbreviation impl in 2 at occurence 1 |
4 | (P → Q) → ((A → P) → (A → Q)) | reverse abbreviation impl in 3 at occurence 1 |
qed |
This proposition is the form for the Hypothetical Syllogism.
The self implication could be derived:
2. Proposition
P → P (hilb2)
1 | P → (P ∨ Q) | add axiom axiom2 |
2 | P → (P ∨ P) | replace proposition variable Q by P in 1 |
3 | (P ∨ P) → P | add axiom axiom1 |
4 | (P → Q) → ((A → P) → (A → Q)) | add proposition hilb1 |
5 | (P → Q) → ((B → P) → (B → Q)) | replace proposition variable A by B in 4 |
6 | (P → C) → ((B → P) → (B → C)) | replace proposition variable Q by C in 5 |
7 | (D → C) → ((B → D) → (B → C)) | replace proposition variable P by D in 6 |
8 | (D → C) → ((P → D) → (P → C)) | replace proposition variable B by P in 7 |
9 | (D → P) → ((P → D) → (P → P)) | replace proposition variable C by P in 8 |
10 | ((P ∨ P) → P) → ((P → (P ∨ P)) → (P → P)) | replace proposition variable D by P ∨ P in 9 |
11 | (P → (P ∨ P)) → (P → P) | modus ponens with 3, 10 |
12 | P → P | modus ponens with 2, 11 |
qed |
One form of the classical `tertium non datur'
3. Proposition
¬P ∨ P (hilb3)
1 | P → P | add proposition hilb2 |
2 | ¬P ∨ P | use abbreviation impl in 1 at occurence 1 |
qed |
The standard form of the excluded middle:
4. Proposition
P ∨ ¬P (hilb4)
1 | ¬P ∨ P | add proposition hilb3 |
2 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
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) | replace proposition variable B by ¬P in 5 |
7 | P ∨ ¬P | modus ponens with 1, 6 |
qed |
Double negation is implicated:
5. Proposition
P → ¬¬P (hilb5)
1 | P ∨ ¬P | add proposition hilb4 |
2 | ¬P ∨ ¬¬P | replace proposition variable P by ¬P in 1 |
3 | P → ¬¬P | reverse abbreviation impl in 2 at occurence 1 |
qed |
The reverse is also true:
6. Proposition
¬¬P → P (hilb6)
1 | P → ¬¬P | add proposition hilb5 |
2 | ¬P → ¬¬¬P | replace proposition variable P by ¬P 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) → ((P ∨ D) → (P ∨ C)) | replace proposition variable B by P in 6 |
8 | (D → ¬¬¬P) → ((P ∨ D) → (P ∨ ¬¬¬P)) | replace proposition variable C by ¬¬¬P in 7 |
9 | (¬P → ¬¬¬P) → ((P ∨ ¬P) → (P ∨ ¬¬¬P)) | replace proposition variable D by ¬P in 8 |
10 | (P ∨ ¬P) → (P ∨ ¬¬¬P) | modus ponens with 2, 9 |
11 | P ∨ ¬P | add proposition hilb4 |
12 | P ∨ ¬¬¬P | modus ponens with 11, 10 |
13 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
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 ∨ ¬¬¬P) → (¬¬¬P ∨ B) | replace proposition variable A by ¬¬¬P in 15 |
17 | (P ∨ ¬¬¬P) → (¬¬¬P ∨ P) | replace proposition variable B by P in 16 |
18 | ¬¬¬P ∨ P | modus ponens with 12, 17 |
19 | ¬¬P → P | reverse abbreviation impl in 18 at occurence 1 |
qed |
The correct reverse of an implication:
7. Proposition
(P → Q) → (¬Q → ¬P) (hilb7)
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) → ((¬P ∨ D) → (¬P ∨ C)) | replace proposition variable B by ¬P in 6 |
8 | (D → ¬¬Q) → ((¬P ∨ D) → (¬P ∨ ¬¬Q)) | replace proposition variable C by ¬¬Q in 7 |
9 | (Q → ¬¬Q) → ((¬P ∨ Q) → (¬P ∨ ¬¬Q)) | replace proposition variable D by Q in 8 |
10 | (¬P ∨ Q) → (¬P ∨ ¬¬Q) | modus ponens with 2, 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 ∨ ¬¬Q) → (¬¬Q ∨ B) | replace proposition variable A by ¬¬Q in 13 |
15 | (¬P ∨ ¬¬Q) → (¬¬Q ∨ ¬P) | replace proposition variable B by ¬P 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) → (((¬P ∨ Q) → D) → ((¬P ∨ Q) → C)) | replace proposition variable B by ¬P ∨ Q in 19 |
21 | (D → (¬¬Q ∨ ¬P)) → (((¬P ∨ Q) → D) → ((¬P ∨ Q) → (¬¬Q ∨ ¬P))) | replace proposition variable C by ¬¬Q ∨ ¬P in 20 |
22 | ((¬P ∨ ¬¬Q) → (¬¬Q ∨ ¬P)) → (((¬P ∨ Q) → (¬P ∨ ¬¬Q)) → ((¬P ∨ Q) → (¬¬Q ∨ ¬P))) | replace proposition variable D by ¬P ∨ ¬¬Q in 21 |
23 | ((¬P ∨ Q) → (¬P ∨ ¬¬Q)) → ((¬P ∨ Q) → (¬¬Q ∨ ¬P)) | modus ponens with 15, 22 |
24 | (¬P ∨ Q) → (¬¬Q ∨ ¬P) | modus ponens with 10, 23 |
25 | (P → Q) → (¬¬Q ∨ ¬P) | reverse abbreviation impl in 24 at occurence 1 |
26 | (P → Q) → (¬Q → ¬P) | reverse abbreviation impl in 25 at occurence 1 |
qed |
Definition of an Implication 1. part:
8. Proposition
(P → Q) → (¬P ∨ Q) (defimpl1)
1 | P → P | add proposition hilb2 |
2 | A → A | replace proposition variable P by A in 1 |
3 | (P → Q) → (P → Q) | replace proposition variable A by P → Q in 2 |
4 | (P → Q) → (¬P ∨ Q) | use abbreviation impl in 3 at occurence 3 |
qed |
Definition of an Implication 2. part:
9. Proposition
(¬P ∨ Q) → (P → Q) (defimpl2)
1 | P → P | add proposition hilb2 |
2 | A → A | replace proposition variable P by A in 1 |
3 | (P → Q) → (P → Q) | replace proposition variable A by P → Q in 2 |
4 | (¬P ∨ Q) → (P → Q) | use abbreviation impl in 3 at occurence 2 |
qed |
Definition of a Conjunction 1. part:
10. Proposition
(P ∧ Q) → ¬(¬P ∨ ¬Q) (defand1)
1 | P → P | add proposition hilb2 |
2 | A → A | replace proposition variable P by A in 1 |
3 | (P ∧ Q) → (P ∧ Q) | replace proposition variable A by P ∧ Q in 2 |
4 | (P ∧ Q) → ¬(¬P ∨ ¬Q) | use abbreviation and in 3 at occurence 2 |
qed |
Definition of a Conjunction 2. part:
11. Proposition
¬(¬P ∨ ¬Q) → (P ∧ Q) (defand2)
1 | P → P | add proposition hilb2 |
2 | A → A | replace proposition variable P by A in 1 |
3 | (P ∧ Q) → (P ∧ Q) | replace proposition variable A by P ∧ Q in 2 |
4 | ¬(¬P ∨ ¬Q) → (P ∧ Q) | use abbreviation and in 3 at occurence 1 |
qed |
Definition of an Equivalence 1. part:
12. Proposition
(P ↔ Q) → ((P → Q) ∧ (Q → P)) (defequi1)
1 | P → P | add proposition hilb2 |
2 | A → A | replace proposition variable P by A in 1 |
3 | (P ↔ Q) → (P ↔ Q) | replace proposition variable A by P ↔ Q in 2 |
4 | (P ↔ Q) → ((P → Q) ∧ (Q → P)) | use abbreviation equi in 3 at occurence 2 |
qed |
Definition of an Equivalence 2. part:
13. Proposition
((P → Q) ∧ (Q → P)) → (P ↔ Q) (defequi2)
1 | P → P | add proposition hilb2 |
2 | A → A | replace proposition variable P by A in 1 |
3 | (P ↔ Q) → (P ↔ Q) | replace proposition variable A by P ↔ Q in 2 |
4 | ((P → Q) ∧ (Q → P)) → (P ↔ Q) | use abbreviation equi in 3 at occurence 1 |
qed |
A simular formulation for the second axiom:
14. Proposition
P → (Q ∨ P) (hilb8)
1 | P → (P ∨ Q) | add axiom axiom2 |
2 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
3 | (P → Q) → ((A → P) → (A → Q)) | add proposition hilb1 |
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) → ((P → D) → (P → C)) | replace proposition variable B by P in 6 |
8 | (D → (Q ∨ P)) → ((P → D) → (P → (Q ∨ P))) | replace proposition variable C by Q ∨ P in 7 |
9 | ((P ∨ Q) → (Q ∨ P)) → ((P → (P ∨ Q)) → (P → (Q ∨ P))) | replace proposition variable D by P ∨ Q in 8 |
10 | (P → (P ∨ Q)) → (P → (Q ∨ P)) | modus ponens with 2, 9 |
11 | P → (Q ∨ P) | modus ponens with 1, 10 |
qed |
A technical lemma (equal to the third axiom):
15. Proposition
(P ∨ Q) → (Q ∨ P) (hilb9)
1 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
qed |
And another technical lemma (simular to the third axiom):
16. Proposition
(Q ∨ P) → (P ∨ Q) (hilb10)
1 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |
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 |
A technical lemma (equal to the first axiom):
17. Proposition
(P ∨ P) → P (hilb11)
1 | (P ∨ P) → P | add axiom axiom1 |
qed |
A simple propositon that follows directly from the second axiom:
18. Proposition
P → (P ∨ P) (hilb12)
1 | P → (P ∨ Q) | add axiom axiom2 |
2 | P → (P ∨ P) | replace proposition variable Q by P in 1 |
qed |
This is a pre form for the associative law:
19. Proposition
(P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) (hilb13)
1 | P → (Q ∨ P) | add proposition hilb8 |
2 | P → (B ∨ P) | replace proposition variable Q by B in 1 |
3 | C → (B ∨ C) | replace proposition variable P by C in 2 |
4 | C → (P ∨ C) | replace proposition variable B by P in 3 |
5 | A → (P ∨ A) | replace proposition variable C by A in 4 |
6 | (P → Q) → ((A ∨ P) → (A ∨ Q)) | add axiom axiom4 |
7 | (P → Q) → ((B ∨ P) → (B ∨ Q)) | replace proposition variable A by B in 6 |
8 | (P → C) → ((B ∨ P) → (B ∨ C)) | replace proposition variable Q by C in 7 |
9 | (D → C) → ((B ∨ D) → (B ∨ C)) | replace proposition variable P by D in 8 |
10 | (D → C) → ((Q ∨ D) → (Q ∨ C)) | replace proposition variable B by Q in 9 |
11 | (D → (P ∨ A)) → ((Q ∨ D) → (Q ∨ (P ∨ A))) | replace proposition variable C by P ∨ A in 10 |
12 | (A → (P ∨ A)) → ((Q ∨ A) → (Q ∨ (P ∨ A))) | replace proposition variable D by A in 11 |
13 | (Q ∨ A) → (Q ∨ (P ∨ A)) | modus ponens with 5, 12 |
14 | (D → C) → ((P ∨ D) → (P ∨ C)) | replace proposition variable B by P in 9 |
15 | (D → (Q ∨ (P ∨ A))) → ((P ∨ D) → (P ∨ (Q ∨ (P ∨ A)))) | replace proposition variable C by Q ∨ (P ∨ A) in 14 |
16 | ((Q ∨ A) → (Q ∨ (P ∨ A))) → ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) | replace proposition variable D by Q ∨ A in 15 |
17 | (P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A))) | modus ponens with 13, 16 |
18 | (P ∨ Q) → (Q ∨ P) | add proposition hilb9 |
19 | (P ∨ B) → (B ∨ P) | replace proposition variable Q by B in 18 |
20 | (C ∨ B) → (B ∨ C) | replace proposition variable P by C in 19 |
21 | (C ∨ (Q ∨ (P ∨ A))) → ((Q ∨ (P ∨ A)) ∨ C) | replace proposition variable B by Q ∨ (P ∨ A) in 20 |
22 | (P ∨ (Q ∨ (P ∨ A))) → ((Q ∨ (P ∨ A)) ∨ P) | replace proposition variable C by P in 21 |
23 | (P → Q) → (¬P ∨ Q) | add proposition defimpl1 |
24 | (¬P ∨ Q) → (P → Q) | add proposition defimpl2 |
25 | (D → C) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ C)) | replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 9 |
26 | (D → ((Q ∨ (P ∨ A)) ∨ P)) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) | replace proposition variable C by (Q ∨ (P ∨ A)) ∨ P in 25 |
27 | ((P ∨ (Q ∨ (P ∨ A))) → ((Q ∨ (P ∨ A)) ∨ P)) → ((¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) | replace proposition variable D by P ∨ (Q ∨ (P ∨ A)) in 26 |
28 | (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) | modus ponens with 22, 27 |
29 | (P → B) → (¬P ∨ B) | replace proposition variable Q by B in 23 |
30 | (C → B) → (¬C ∨ B) | replace proposition variable P by C in 29 |
31 | (C → (P ∨ (Q ∨ (P ∨ A)))) → (¬C ∨ (P ∨ (Q ∨ (P ∨ A)))) | replace proposition variable B by P ∨ (Q ∨ (P ∨ A)) in 30 |
32 | ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) | replace proposition variable C by P ∨ (Q ∨ A) in 31 |
33 | (P → Q) → ((A → P) → (A → Q)) | add proposition hilb1 |
34 | (P → Q) → ((B → P) → (B → Q)) | replace proposition variable A by B in 33 |
35 | (P → C) → ((B → P) → (B → C)) | replace proposition variable Q by C in 34 |
36 | (D → C) → ((B → D) → (B → C)) | replace proposition variable P by D in 35 |
37 | (D → C) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → D) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → C)) | replace proposition variable B by (P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A))) in 36 |
38 | (D → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → D) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)))) | replace proposition variable C by ¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P) in 37 |
39 | ((¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A))))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)))) | replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A))) in 38 |
40 | (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A))))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) | modus ponens with 28, 39 |
41 | ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) | modus ponens with 32, 40 |
42 | (¬P ∨ B) → (P → B) | replace proposition variable Q by B in 24 |
43 | (¬C ∨ B) → (C → B) | replace proposition variable P by C in 42 |
44 | (¬C ∨ ((Q ∨ (P ∨ A)) ∨ P)) → (C → ((Q ∨ (P ∨ A)) ∨ P)) | replace proposition variable B by (Q ∨ (P ∨ A)) ∨ P in 43 |
45 | (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) | replace proposition variable C by P ∨ (Q ∨ A) in 44 |
46 | (D → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → D) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)))) | replace proposition variable C by (P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P) in 37 |
47 | ((¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)))) | replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P) in 46 |
48 | (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P))) | modus ponens with 45, 47 |
49 | ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) | modus ponens with 41, 48 |
50 | (P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P) | modus ponens with 17, 49 |
51 | (P ∨ A) → (Q ∨ (P ∨ A)) | replace proposition variable P by P ∨ A in 1 |
52 | P → (P ∨ Q) | add axiom axiom2 |
53 | P → (P ∨ A) | replace proposition variable Q by A in 52 |
54 | (D → C) → ((P → D) → (P → C)) | replace proposition variable B by P in 36 |
55 | (D → (Q ∨ (P ∨ A))) → ((P → D) → (P → (Q ∨ (P ∨ A)))) | replace proposition variable C by Q ∨ (P ∨ A) in 54 |
56 | ((P ∨ A) → (Q ∨ (P ∨ A))) → ((P → (P ∨ A)) → (P → (Q ∨ (P ∨ A)))) | replace proposition variable D by P ∨ A in 55 |
57 | (P → (P ∨ A)) → (P → (Q ∨ (P ∨ A))) | modus ponens with 51, 56 |
58 | P → (Q ∨ (P ∨ A)) | modus ponens with 53, 57 |
59 | (D → C) → (((Q ∨ (P ∨ A)) ∨ D) → ((Q ∨ (P ∨ A)) ∨ C)) | replace proposition variable B by Q ∨ (P ∨ A) in 9 |
60 | (D → (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ D) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) | replace proposition variable C by Q ∨ (P ∨ A) in 59 |
61 | (P → (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) | replace proposition variable D by P in 60 |
62 | ((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) | modus ponens with 58, 61 |
63 | (P ∨ P) → P | add proposition hilb11 |
64 | (B ∨ B) → B | replace proposition variable P by B in 63 |
65 | ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) → (Q ∨ (P ∨ A)) | replace proposition variable B by Q ∨ (P ∨ A) in 64 |
66 | (D → C) → ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ D) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ C)) | replace proposition variable B by ¬((Q ∨ (P ∨ A)) ∨ P) in 9 |
67 | (D → (Q ∨ (P ∨ A))) → ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ D) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) | replace proposition variable C by Q ∨ (P ∨ A) in 66 |
68 | (((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) → (Q ∨ (P ∨ A))) → ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) | replace proposition variable D by (Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)) in 67 |
69 | (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) | modus ponens with 65, 68 |
70 | (C → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬C ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) | replace proposition variable B by (Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)) in 30 |
71 | (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) | replace proposition variable C by (Q ∨ (P ∨ A)) ∨ P in 70 |
72 | (D → C) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → D) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → C)) | replace proposition variable B by ((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) in 36 |
73 | (D → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → D) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))))) | replace proposition variable C by ¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)) in 72 |
74 | ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))))) | replace proposition variable D by ¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) in 73 |
75 | ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) | modus ponens with 69, 74 |
76 | (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) | modus ponens with 71, 75 |
77 | (¬C ∨ (Q ∨ (P ∨ A))) → (C → (Q ∨ (P ∨ A))) | replace proposition variable B by Q ∨ (P ∨ A) in 43 |
78 | (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))) | replace proposition variable C by (Q ∨ (P ∨ A)) ∨ P in 77 |
79 | (D → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → D) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))))) | replace proposition variable C by ((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)) in 72 |
80 | ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))))) | replace proposition variable D by ¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)) in 79 |
81 | ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)))) | modus ponens with 78, 80 |
82 | (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))) | modus ponens with 76, 81 |
83 | ((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)) | modus ponens with 62, 82 |
84 | (D → C) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → C)) | replace proposition variable B by P ∨ (Q ∨ A) in 36 |
85 | (D → (Q ∨ (P ∨ A))) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)))) | replace proposition variable C by Q ∨ (P ∨ A) in 84 |
86 | (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))) → (((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)))) | replace proposition variable D by (Q ∨ (P ∨ A)) ∨ P in 85 |
87 | ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A))) | modus ponens with 83, 86 |
88 | (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) | modus ponens with 50, 87 |
qed |
The associative law for the disjunction (first direction):
20. Proposition
(P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) (hilb14)
1 | (P ∨ Q) → (Q ∨ P) | add proposition hilb9 |
2 | (P ∨ B) → (B ∨ P) | replace proposition variable Q by B in 1 |
3 | (C ∨ B) → (B ∨ C) | replace proposition variable P by C in 2 |
4 | (C ∨ A) → (A ∨ C) | replace proposition variable B by A in 3 |
5 | (Q ∨ A) → (A ∨ Q) | replace proposition variable C by Q in 4 |
6 | (P → Q) → ((A ∨ P) → (A ∨ Q)) | add axiom axiom4 |
7 | (P → Q) → ((B ∨ P) → (B ∨ Q)) | replace proposition variable A by B in 6 |
8 | (P → C) → ((B ∨ P) → (B ∨ C)) | replace proposition variable Q by C in 7 |
9 | (D → C) → ((B ∨ D) → (B ∨ C)) | replace proposition variable P by D in 8 |
10 | (D → C) → ((P ∨ D) → (P ∨ C)) | replace proposition variable B by P in 9 |
11 | (D → (A ∨ Q)) → ((P ∨ D) → (P ∨ (A ∨ Q))) | replace proposition variable C by A ∨ Q in 10 |
12 | ((Q ∨ A) → (A ∨ Q)) → ((P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q))) | replace proposition variable D by Q ∨ A in 11 |
13 | (P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q)) | modus ponens with 5, 12 |
14 | (P → Q) → (¬P ∨ Q) | add proposition defimpl1 |
15 | (¬P ∨ Q) → (P → Q) | add proposition defimpl2 |
16 | (P → B) → (¬P ∨ B) | replace proposition variable Q by B in 14 |
17 | (C → B) → (¬C ∨ B) | replace proposition variable P by C in 16 |
18 | (P → Q) → ((A → P) → (A → Q)) | add proposition hilb1 |
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 | (¬P ∨ B) → (P → B) | replace proposition variable Q by B in 15 |
23 | (¬C ∨ B) → (C → B) | replace proposition variable P by C in 22 |
24 | (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) | add proposition hilb13 |
25 | (P ∨ (Q ∨ B)) → (Q ∨ (P ∨ B)) | replace proposition variable A by B in 24 |
26 | (P ∨ (C ∨ B)) → (C ∨ (P ∨ B)) | replace proposition variable Q by C in 25 |
27 | (D ∨ (C ∨ B)) → (C ∨ (D ∨ B)) | replace proposition variable P by D in 26 |
28 | (D ∨ (C ∨ Q)) → (C ∨ (D ∨ Q)) | replace proposition variable B by Q in 27 |
29 | (D ∨ (A ∨ Q)) → (A ∨ (D ∨ Q)) | replace proposition variable C by A in 28 |
30 | (P ∨ (A ∨ Q)) → (A ∨ (P ∨ Q)) | replace proposition variable D by P in 29 |
31 | (D → C) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → C)) | replace proposition variable B by P ∨ (Q ∨ A) in 21 |
32 | (D → (A ∨ (P ∨ Q))) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)))) | replace proposition variable C by A ∨ (P ∨ Q) in 31 |
33 | ((P ∨ (A ∨ Q)) → (A ∨ (P ∨ Q))) → (((P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q))) → ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)))) | replace proposition variable D by P ∨ (A ∨ Q) in 32 |
34 | ((P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q))) → ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) | modus ponens with 30, 33 |
35 | (P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)) | modus ponens with 13, 34 |
36 | (C ∨ (P ∨ Q)) → ((P ∨ Q) ∨ C) | replace proposition variable B by P ∨ Q in 3 |
37 | (A ∨ (P ∨ Q)) → ((P ∨ Q) ∨ A) | replace proposition variable C by A in 36 |
38 | (D → C) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ C)) | replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 9 |
39 | (D → ((P ∨ Q) ∨ A)) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) | replace proposition variable C by (P ∨ Q) ∨ A in 38 |
40 | ((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 39 |
41 | (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) | modus ponens with 37, 40 |
42 | (C → (A ∨ (P ∨ Q))) → (¬C ∨ (A ∨ (P ∨ Q))) | replace proposition variable B by A ∨ (P ∨ Q) in 17 |
43 | ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) | replace proposition variable C by P ∨ (Q ∨ A) in 42 |
44 | (D → C) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → D) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → C)) | replace proposition variable B by (P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)) in 21 |
45 | (D → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → D) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)))) | replace proposition variable C by ¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A) in 44 |
46 | ((¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q)))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)))) | replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q)) in 45 |
47 | (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q)))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) | modus ponens with 41, 46 |
48 | ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) | modus ponens with 43, 47 |
49 | (¬C ∨ ((P ∨ Q) ∨ A)) → (C → ((P ∨ Q) ∨ A)) | replace proposition variable B by (P ∨ Q) ∨ A in 23 |
50 | (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)) | replace proposition variable C by P ∨ (Q ∨ A) in 49 |
51 | (D → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → D) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)))) | replace proposition variable C by (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) in 44 |
52 | ((¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)))) | replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A) in 51 |
53 | (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A))) | modus ponens with 50, 52 |
54 | ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)) | modus ponens with 48, 53 |
55 | (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) | modus ponens with 35, 54 |
qed |
The associative law for the disjunction (second direction):
21. Proposition
((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) (hilb15)
1 | (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) | add proposition hilb14 |
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 ∨ P)) → ((D ∨ C) ∨ P) | replace proposition variable B by P in 4 |
6 | (D ∨ (Q ∨ P)) → ((D ∨ Q) ∨ P) | replace proposition variable C by Q in 5 |
7 | (A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P) | replace proposition variable D by A in 6 |
8 | (Q ∨ P) → (P ∨ Q) | add proposition hilb10 |
9 | (B ∨ P) → (P ∨ B) | replace proposition variable Q by B in 8 |
10 | (B ∨ C) → (C ∨ B) | replace proposition variable P by C in 9 |
11 | ((Q ∨ P) ∨ C) → (C ∨ (Q ∨ P)) | replace proposition variable B by Q ∨ P in 10 |
12 | ((Q ∨ P) ∨ A) → (A ∨ (Q ∨ P)) | replace proposition variable C by A 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 → (A ∨ (Q ∨ P))) → (¬(A ∨ (Q ∨ P)) → ¬C) | replace proposition variable B by A ∨ (Q ∨ P) in 17 |
19 | (((Q ∨ P) ∨ A) → (A ∨ (Q ∨ P))) → (¬(A ∨ (Q ∨ P)) → ¬((Q ∨ P) ∨ A)) | replace proposition variable C by (Q ∨ P) ∨ A in 18 |
20 | ¬(A ∨ (Q ∨ P)) → ¬((Q ∨ P) ∨ 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) → ((((A ∨ Q) ∨ P) ∨ D) → (((A ∨ Q) ∨ P) ∨ C)) | replace proposition variable B by (A ∨ Q) ∨ P in 24 |
26 | (D → ¬((Q ∨ P) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ D) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) | replace proposition variable C by ¬((Q ∨ P) ∨ A) in 25 |
27 | (¬(A ∨ (Q ∨ P)) → ¬((Q ∨ P) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) | replace proposition variable D by ¬(A ∨ (Q ∨ P)) in 26 |
28 | (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ 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 ∨ ¬((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) ∨ C) | replace proposition variable B by ¬((Q ∨ P) ∨ A) in 31 |
33 | (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) | replace proposition variable C by (A ∨ Q) ∨ P 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) → (((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → D) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → C)) | replace proposition variable B by ((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)) in 37 |
39 | (D → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → D) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable C by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 38 |
40 | ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A) in 39 |
41 | ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) | modus ponens with 33, 40 |
42 | (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) | modus ponens with 28, 41 |
43 | (C ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ C) | replace proposition variable B by (A ∨ Q) ∨ P in 31 |
44 | (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) | replace proposition variable C by ¬(A ∨ (Q ∨ P)) in 43 |
45 | (D → C) → (((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → C)) | replace proposition variable B by ¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P) in 37 |
46 | (D → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable C by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 45 |
47 | ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)))) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)) in 46 |
48 | ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)))) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) | modus ponens with 42, 47 |
49 | (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) | 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 → ((A ∨ Q) ∨ P)) → (¬C ∨ ((A ∨ Q) ∨ P)) | replace proposition variable B by (A ∨ Q) ∨ P in 51 |
53 | ((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) | replace proposition variable C by A ∨ (Q ∨ P) in 52 |
54 | (D → C) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → D) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → C)) | replace proposition variable B by (A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P) in 37 |
55 | (D → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → D) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable C by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 54 |
56 | ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable D by ¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P) in 55 |
57 | (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) | modus ponens with 49, 56 |
58 | ((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) | 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 ∨ ((A ∨ Q) ∨ P)) → (C → ((A ∨ Q) ∨ P)) | replace proposition variable B by (A ∨ Q) ∨ P in 60 |
62 | (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) | replace proposition variable C by (Q ∨ P) ∨ A in 61 |
63 | (D → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → D) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)))) | replace proposition variable C by ((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P) in 54 |
64 | ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)))) | replace proposition variable D by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 63 |
65 | (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P))) | modus ponens with 62, 64 |
66 | ((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) | modus ponens with 58, 65 |
67 | ((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P) | modus ponens with 7, 66 |
68 | (D → C) → ((A ∨ D) → (A ∨ C)) | replace proposition variable B by A in 24 |
69 | (D → (Q ∨ P)) → ((A ∨ D) → (A ∨ (Q ∨ P))) | replace proposition variable C by Q ∨ P in 68 |
70 | ((P ∨ Q) → (Q ∨ P)) → ((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) | replace proposition variable D by P ∨ Q in 69 |
71 | (A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P)) | modus ponens with 29, 70 |
72 | (C ∨ (Q ∨ P)) → ((Q ∨ P) ∨ C) | replace proposition variable B by Q ∨ P in 31 |
73 | (A ∨ (Q ∨ P)) → ((Q ∨ P) ∨ A) | replace proposition variable C by A in 72 |
74 | (D → C) → (((A ∨ (P ∨ Q)) → D) → ((A ∨ (P ∨ Q)) → C)) | replace proposition variable B by A ∨ (P ∨ Q) in 37 |
75 | (D → ((Q ∨ P) ∨ A)) → (((A ∨ (P ∨ Q)) → D) → ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A))) | replace proposition variable C by (Q ∨ P) ∨ A in 74 |
76 | ((A ∨ (Q ∨ P)) → ((Q ∨ P) ∨ A)) → (((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) → ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A))) | replace proposition variable D by A ∨ (Q ∨ P) in 75 |
77 | ((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) → ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A)) | modus ponens with 73, 76 |
78 | (A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A) | modus ponens with 71, 77 |
79 | (C ∨ A) → (A ∨ C) | replace proposition variable B by A in 31 |
80 | ((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q)) | replace proposition variable C by P ∨ Q in 79 |
81 | (D → C) → ((((P ∨ Q) ∨ A) → D) → (((P ∨ Q) ∨ A) → C)) | replace proposition variable B by (P ∨ Q) ∨ A in 37 |
82 | (D → ((Q ∨ P) ∨ A)) → ((((P ∨ Q) ∨ A) → D) → (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A))) | replace proposition variable C by (Q ∨ P) ∨ A in 81 |
83 | ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A)) → ((((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q))) → (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A))) | replace proposition variable D by A ∨ (P ∨ Q) in 82 |
84 | (((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q))) → (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A)) | modus ponens with 78, 83 |
85 | ((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A) | modus ponens with 80, 84 |
86 | (C → ((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) → ¬C) | replace proposition variable B by (Q ∨ P) ∨ A in 17 |
87 | (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) → ¬((P ∨ Q) ∨ A)) | replace proposition variable C by (P ∨ Q) ∨ A in 86 |
88 | ¬((Q ∨ P) ∨ A) → ¬((P ∨ Q) ∨ A) | modus ponens with 85, 87 |
89 | (D → ¬((P ∨ Q) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ D) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) | replace proposition variable C by ¬((P ∨ Q) ∨ A) in 25 |
90 | (¬((Q ∨ P) ∨ A) → ¬((P ∨ Q) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) | replace proposition variable D by ¬((Q ∨ P) ∨ A) in 89 |
91 | (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A)) | modus ponens with 88, 90 |
92 | (C ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ C) | replace proposition variable B by ¬((P ∨ Q) ∨ A) in 31 |
93 | (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) | replace proposition variable C by (A ∨ Q) ∨ P in 92 |
94 | (D → C) → (((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → D) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → C)) | replace proposition variable B by ((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A) in 37 |
95 | (D → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → D) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 94 |
96 | ((((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A) in 95 |
97 | ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) | modus ponens with 93, 96 |
98 | (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) | modus ponens with 91, 97 |
99 | (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) | replace proposition variable C by ¬((Q ∨ P) ∨ A) in 43 |
100 | (D → C) → (((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → C)) | replace proposition variable B by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 37 |
101 | (D → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 100 |
102 | ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A) in 101 |
103 | ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) | modus ponens with 98, 102 |
104 | (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) | modus ponens with 99, 103 |
105 | (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) | replace proposition variable C by (Q ∨ P) ∨ A in 52 |
106 | (D → C) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → C)) | replace proposition variable B by ((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P) in 37 |
107 | (D → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 106 |
108 | ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) | replace proposition variable D by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 107 |
109 | ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) | modus ponens with 104, 108 |
110 | (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) | modus ponens with 105, 109 |
111 | (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) | replace proposition variable C by (P ∨ Q) ∨ A in 61 |
112 | (D → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)))) | replace proposition variable C by ((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P) in 106 |
113 | ((¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)))) | replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 112 |
114 | ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P))) | modus ponens with 111, 113 |
115 | (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) | modus ponens with 110, 114 |
116 | ((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P) | modus ponens with 67, 115 |
117 | (C ∨ P) → (P ∨ C) | replace proposition variable B by P in 31 |
118 | ((A ∨ Q) ∨ P) → (P ∨ (A ∨ Q)) | replace proposition variable C by A ∨ Q in 117 |
119 | (D → C) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ C)) | replace proposition variable B by ¬((P ∨ Q) ∨ A) in 24 |
120 | (D → (P ∨ (A ∨ Q))) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) | replace proposition variable C by P ∨ (A ∨ Q) in 119 |
121 | (((A ∨ Q) ∨ P) → (P ∨ (A ∨ Q))) → ((¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) | replace proposition variable D by (A ∨ Q) ∨ P in 120 |
122 | (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) | modus ponens with 118, 121 |
123 | (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) | replace proposition variable C by (P ∨ Q) ∨ A in 52 |
124 | (D → C) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → C)) | replace proposition variable B by ((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P) in 37 |
125 | (D → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))))) | replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)) in 124 |
126 | ((¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))))) | replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 125 |
127 | ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) | modus ponens with 122, 126 |
128 | (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) | modus ponens with 123, 127 |
129 | (¬C ∨ (P ∨ (A ∨ Q))) → (C → (P ∨ (A ∨ Q))) | replace proposition variable B by P ∨ (A ∨ Q) in 60 |
130 | (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) | replace proposition variable C by (P ∨ Q) ∨ A in 129 |
131 | (D → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))))) | replace proposition variable C by ((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)) in 124 |
132 | ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))))) | replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)) in 131 |
133 | ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)))) | modus ponens with 130, 132 |
134 | (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) | modus ponens with 128, 133 |
135 | ((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)) | modus ponens with 116, 134 |
136 | (C ∨ Q) → (Q ∨ C) | replace proposition variable B by Q in 31 |
137 | (A ∨ Q) → (Q ∨ A) | replace proposition variable C by A in 136 |
138 | (D → C) → ((P ∨ D) → (P ∨ C)) | replace proposition variable B by P in 24 |
139 | (D → (Q ∨ A)) → ((P ∨ D) → (P ∨ (Q ∨ A))) | replace proposition variable C by Q ∨ A in 138 |
140 | ((A ∨ Q) → (Q ∨ A)) → ((P ∨ (A ∨ Q)) → (P ∨ (Q ∨ A))) | replace proposition variable D by A ∨ Q in 139 |
141 | (P ∨ (A ∨ Q)) → (P ∨ (Q ∨ A)) | modus ponens with 137, 140 |
142 | (D → (P ∨ (Q ∨ A))) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) | replace proposition variable C by P ∨ (Q ∨ A) in 119 |
143 | ((P ∨ (A ∨ Q)) → (P ∨ (Q ∨ A))) → ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) | replace proposition variable D by P ∨ (A ∨ Q) in 142 |
144 | (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) | modus ponens with 141, 143 |
145 | (C → (P ∨ (A ∨ Q))) → (¬C ∨ (P ∨ (A ∨ Q))) | replace proposition variable B by P ∨ (A ∨ Q) in 51 |
146 | (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) | replace proposition variable C by (P ∨ Q) ∨ A in 145 |
147 | (D → C) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → D) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → C)) | replace proposition variable B by ((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)) in 37 |
148 | (D → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → D) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))))) | replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)) in 147 |
149 | ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))))) | replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)) in 148 |
150 | ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) | modus ponens with 144, 149 |
151 | (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) | modus ponens with 146, 150 |
152 | (¬C ∨ (P ∨ (Q ∨ A))) → (C → (P ∨ (Q ∨ A))) | replace proposition variable B by P ∨ (Q ∨ A) in 60 |
153 | (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))) | replace proposition variable C by (P ∨ Q) ∨ A in 152 |
154 | (D → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → D) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))))) | replace proposition variable C by ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) in 147 |
155 | ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))))) | replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)) in 154 |
156 | ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)))) | modus ponens with 153, 155 |
157 | (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))) | modus ponens with 151, 156 |
158 | ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) | modus ponens with 135, 157 |
qed |
Another consequence from hilb13 is the exchange of preconditions:
22. Proposition
(P → (Q → A)) → (Q → (P → A)) (hilb16)
1 | (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) | add proposition hilb13 |
2 | (P ∨ (Q ∨ B)) → (Q ∨ (P ∨ B)) | replace proposition variable A by B in 1 |
3 | (P ∨ (C ∨ B)) → (C ∨ (P ∨ B)) | replace proposition variable Q by C in 2 |
4 | (D ∨ (C ∨ B)) → (C ∨ (D ∨ B)) | replace proposition variable P by D in 3 |
5 | (D ∨ (C ∨ A)) → (C ∨ (D ∨ A)) | replace proposition variable B by A in 4 |
6 | (D ∨ (¬Q ∨ A)) → (¬Q ∨ (D ∨ A)) | replace proposition variable C by ¬Q in 5 |
7 | (¬P ∨ (¬Q ∨ A)) → (¬Q ∨ (¬P ∨ A)) | replace proposition variable D by ¬P in 6 |
8 | (P → (¬Q ∨ A)) → (¬Q ∨ (¬P ∨ A)) | reverse abbreviation impl in 7 at occurence 1 |
9 | (P → (Q → A)) → (¬Q ∨ (¬P ∨ A)) | reverse abbreviation impl in 8 at occurence 1 |
10 | (P → (Q → A)) → (Q → (¬P ∨ A)) | reverse abbreviation impl in 9 at occurence 1 |
11 | (P → (Q → A)) → (Q → (P → A)) | reverse abbreviation impl in 10 at occurence 1 |
qed |
An analogus form for hyperref [hilb16]hilb16:
23. Proposition
(Q → (P → A)) → (P → (Q → A)) (hilb17)
1 | (P → (Q → A)) → (Q → (P → A)) | add proposition hilb16 |
2 | (P → (Q → B)) → (Q → (P → B)) | replace proposition variable A by B in 1 |
3 | (P → (C → B)) → (C → (P → B)) | replace proposition variable Q by C in 2 |
4 | (D → (C → B)) → (C → (D → B)) | replace proposition variable P by D in 3 |
5 | (D → (C → A)) → (C → (D → A)) | replace proposition variable B by A in 4 |
6 | (D → (P → A)) → (P → (D → A)) | replace proposition variable C by P in 5 |
7 | (Q → (P → A)) → (P → (Q → A)) | replace proposition variable D by Q in 6 |
qed |