Now we could declare the rule Apply Axiom.
parameters:
p | proof line number |
á link ñ | axiom reference |
1. Rule Declaration
Apply Axiom (rule9)
Analogous to the preceding we declare the rule Apply Sentence.
2. Rule Declaration
Apply Sentence (rule10)
First we prove a simple implication, that follows directly from the fourth axiom:
3. 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.
Now we could declare the rule Hypothetical Syllogism.
parameters:
p | proof line number |
m | proof line number |
4. Rule Declaration
Hypothetical Syllogism (rule11)
References, needed for declaration:
hilb1
The self implication could be derived:
5. 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 ® P) | hypothetical syllogism with 2 and 3 |
qed |
One form of the classical tertium non datur
6. 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:
7. Proposition
(P Ú ØP) (hilb4)
1 | (ØP Ú P) | add proposition hilb3 |
2 | (P Ú ØP) | apply axiom axiom3 in 1 |
qed |
Double negation is implicated:
8. 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:
9. Proposition
(ØØP ® P) (hilb6)
1 | (P ® ØØP) | add proposition hilb5 |
2 | (ØP ® ØØØP) | replace proposition variable P by ØP in 1 |
3 | ((P Ú ØP) ® (P Ú ØØØP)) | apply axiom axiom4 in 2 |
4 | (P Ú ØP) | add proposition hilb4 |
5 | (P Ú ØØØP) | modus ponens with 4, 3 |
6 | (ØØØP Ú P) | apply axiom axiom3 in 5 |
7 | (ØØP ® P) | reverse abbreviation impl in 6 at occurence 1 |
qed |
The correct reverse of an implication:
10. 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) ® (ØP Ú ØØQ)) | apply axiom axiom4 in 2 |
4 | ((P Ú Q) ® (Q Ú P)) | add axiom axiom3 |
5 | ((ØP Ú ØØQ) ® (ØØQ Ú ØP)) | substitute variables in 4 |
6 | ((ØP Ú Q) ® (ØØQ Ú ØP)) | hypothetical syllogism with 3 and 5 |
7 | ((P ® Q) ® (ØØQ Ú ØP)) | reverse abbreviation impl in 6 at occurence 1 |
8 | ((P ® Q) ® (ØQ ® ØP)) | reverse abbreviation impl in 7 at occurence 1 |
qed |
11. Rule Declaration
Correct reverse of an implication (rule12)
References, needed for declaration:
hilb7
12. Rule Declaration
Add a Conjunction on the Left (rule13)
References, needed for declaration:
axiom4
13. Rule Declaration
Add a Conjunction on the Right (rule14)
References, needed for declaration:
axiom3
, axiom4
Definition of an Implication 1. part:
14. Proposition
((P ® Q) ® (ØP Ú Q)) (defimpl1)
1 | (P ® P) | add proposition hilb2 |
2 | ((P ® Q) ® (P ® Q)) | substitute variables in 1 |
3 | ((P ® Q) ® (ØP Ú Q)) | use abbreviation impl in 2 at occurence 3 |
qed |
Definition of an Implication 2. part:
15. Proposition
((ØP Ú Q) ® (P ® Q)) (defimpl2)
1 | (P ® P) | add proposition hilb2 |
2 | ((P ® Q) ® (P ® Q)) | substitute variables in 1 |
3 | ((ØP Ú Q) ® (P ® Q)) | use abbreviation impl in 2 at occurence 2 |
qed |
16. Rule Declaration
Addition of an Implication on the Right (rule17)
References, needed for declaration:
defimpl1
, defimpl2
17. Rule Declaration
Addition of an Implication on the Left (rule18)
References, needed for declaration:
defimpl1
, defimpl2
Definition of a Conjunction 1. part:
18. Proposition
((P Ù Q) ® Ø(ØP Ú ØQ)) (defand1)
1 | (P ® P) | add proposition hilb2 |
2 | ((P Ù Q) ® (P Ù Q)) | substitute variables in 1 |
3 | ((P Ù Q) ® Ø(ØP Ú ØQ)) | use abbreviation and in 2 at occurence 2 |
qed |
Definition of a Conjunction 2. part:
19. Proposition
(Ø(ØP Ú ØQ) ® (P Ù Q)) (defand2)
1 | (P ® P) | add proposition hilb2 |
2 | ((P Ù Q) ® (P Ù Q)) | substitute variables in 1 |
3 | (Ø(ØP Ú ØQ) ® (P Ù Q)) | use abbreviation and in 2 at occurence 1 |
qed |
20. Rule Declaration
Addition of a Conjunction on the Left (rule19)
References, needed for declaration:
defand1
, defand2
21. Rule Declaration
Addition of a Conjunction on the Right (rule20)
References, needed for declaration:
defand1
, defand2
Definition of an Equivalence 1. part:
22. Proposition
((P « Q) ® ((P ® Q) Ù (Q ® P))) (defequi1)
1 | (P ® P) | add proposition hilb2 |
2 | ((P « Q) ® (P « Q)) | substitute variables in 1 |
3 | ((P « Q) ® ((P ® Q) Ù (Q ® P))) | use abbreviation equi in 2 at occurence 2 |
qed |
Definition of an Equivalence 2. part:
23. Proposition
(((P ® Q) Ù (Q ® P)) ® (P « Q)) (defequi2)
1 | (P ® P) | add proposition hilb2 |
2 | ((P « Q) ® (P « Q)) | substitute variables in 1 |
3 | (((P ® Q) Ù (Q ® P)) ® (P « Q)) | use abbreviation equi in 2 at occurence 1 |
qed |
24. Rule Declaration
Addition of an Equivalence on the Left (rule21)
References, needed for declaration:
defequi1
, defequi2
25. Rule Declaration
Addition of an Equivalence on the Right (rule22)
References, needed for declaration:
defequi1
, defequi2
26. Rule Declaration
Elementary equivalence of two formulas (rule30)
A simular formulation for the second axiom:
27. Proposition
(P ® (Q Ú P)) (hilb8)
1 | (P ® (P Ú Q)) | add axiom axiom2 |
2 | ((P Ú Q) ® (Q Ú P)) | add axiom axiom3 |
3 | (P ® (Q Ú P)) | hypothetical syllogism with 1 and 2 |
qed |
A technical lemma (equal to the third axiom):
28. Proposition
((P Ú Q) ® (Q Ú P)) (hilb9)
1 | ((P Ú Q) ® (Q Ú P)) | add axiom axiom3 |
qed |
And another technical lemma (simular to the third axiom):
29. Proposition
((Q Ú P) ® (P Ú Q)) (hilb10)
1 | ((P Ú Q) ® (Q Ú P)) | add axiom axiom3 |
2 | ((Q Ú P) ® (P Ú Q)) | substitute variables in 1 |
qed |
A technical lemma (equal to the first axiom):
30. Proposition
((P Ú P) ® P) (hilb11)
1 | ((P Ú P) ® P) | add axiom axiom1 |
qed |
A simple propositon that follows directly from the second axiom:
31. 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:
32. Proposition
((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) (hilb13)
1 | (P ® (Q Ú P)) | add proposition hilb8 |
2 | (A ® (P Ú A)) | substitute variables in 1 |
3 | ((Q Ú A) ® (Q Ú (P Ú A))) | apply axiom axiom4 in 2 |
4 | ((P Ú (Q Ú A)) ® (P Ú (Q Ú (P Ú A)))) | apply axiom axiom4 in 3 |
5 | ((P Ú (Q Ú A)) ® ((Q Ú (P Ú A)) Ú P)) | elementary equivalence in 4 at 3 of hilb9 with hilb10 |
6 | ((P Ú A) ® (Q Ú (P Ú A))) | replace proposition variable P by (P Ú A) in 1 |
7 | (P ® (P Ú Q)) | add axiom axiom2 |
8 | (P ® (P Ú A)) | replace proposition variable Q by A in 7 |
9 | (P ® (Q Ú (P Ú A))) | hypothetical syllogism with 8 and 6 |
10 | (((Q Ú (P Ú A)) Ú P) ® ((Q Ú (P Ú A)) Ú (Q Ú (P Ú A)))) | apply axiom axiom4 in 9 |
11 | (((Q Ú (P Ú A)) Ú P) ® (Q Ú (P Ú A))) | elementary equivalence in 10 at 1 of hilb11 with hilb12 |
12 | ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) | hypothetical syllogism with 5 and 11 |
qed |
The associative law for the disjunction (first direction):
33. Proposition
((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) (hilb14)
1 | (P ® P) | add proposition hilb2 |
2 | ((P Ú (Q Ú A)) ® (P Ú (Q Ú A))) | substitute variables in 1 |
3 | ((P Ú (Q Ú A)) ® (P Ú (A Ú Q))) | elementary equivalence in 2 at 4 of hilb9 with hilb10 |
4 | ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) | add proposition hilb13 |
5 | ((P Ú (A Ú Q)) ® (A Ú (P Ú Q))) | substitute variables in 4 |
6 | ((P Ú (Q Ú A)) ® (A Ú (P Ú Q))) | hypothetical syllogism with 3 and 5 |
7 | ((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) | elementary equivalence in 6 at 3 of hilb9 with hilb10 |
qed |
The associative law for the disjunction (second direction):
34. Proposition
(((P Ú Q) Ú A) ® (P Ú (Q Ú A))) (hilb15)
1 | ((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) | add proposition hilb14 |
2 | ((A Ú (Q Ú P)) ® ((A Ú Q) Ú P)) | substitute variables in 1 |
3 | (((Q Ú P) Ú A) ® ((A Ú Q) Ú P)) | elementary equivalence in 2 at 1 of hilb9 with hilb10 |
4 | (((P Ú Q) Ú A) ® ((A Ú Q) Ú P)) | elementary equivalence in 3 at 2 of hilb9 with hilb10 |
5 | (((P Ú Q) Ú A) ® (P Ú (A Ú Q))) | elementary equivalence in 4 at 3 of hilb9 with hilb10 |
6 | (((P Ú Q) Ú A) ® (P Ú (Q Ú A))) | elementary equivalence in 5 at 4 of hilb9 with hilb10 |
qed |
Another consequence from hilb13 is the exchange of preconditions:
35. Proposition
((P ® (Q ® A)) ® (Q ® (P ® A))) (hilb16)
1 | ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) | add proposition hilb13 |
2 | ((ØP Ú (ØQ Ú A)) ® (ØQ Ú (ØP Ú A))) | substitute variables in 1 |
3 | ((P ® (ØQ Ú A)) ® (ØQ Ú (ØP Ú A))) | reverse abbreviation impl in 2 at occurence 1 |
4 | ((P ® (Q ® A)) ® (ØQ Ú (ØP Ú A))) | reverse abbreviation impl in 3 at occurence 1 |
5 | ((P ® (Q ® A)) ® (Q ® (ØP Ú A))) | reverse abbreviation impl in 4 at occurence 1 |
6 | ((P ® (Q ® A)) ® (Q ® (P ® A))) | reverse abbreviation impl in 5 at occurence 1 |
qed |
An analogus form for hyperref [hilb16]hilb16:
36. Proposition
((Q ® (P ® A)) ® (P ® (Q ® A))) (hilb17)
1 | ((P ® (Q ® A)) ® (Q ® (P ® A))) | add proposition hilb16 |
2 | ((Q ® (P ® A)) ® (P ® (Q ® A))) | substitute variables in 1 |
qed |