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 |