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 |