Negation of a conjunction:
1. Proposition
¬(P ∧ Q) → (¬P ∨ ¬Q) (hilb18)
1 | ¬¬P → P | add proposition hilb6 |
2 | ¬¬Q → Q | replace proposition variable P by Q in 1 |
3 | ¬¬(¬P ∨ ¬Q) → (¬P ∨ ¬Q) | replace proposition variable Q by ¬P ∨ ¬Q in 2 |
4 | ¬(P ∧ Q) → (¬P ∨ ¬Q) | reverse abbreviation and in 3 at occurence 1 |
qed |
The reverse of a negation of a conjunction:
2. Proposition
(¬P ∨ ¬Q) → ¬(P ∧ Q) (hilb19)
1 | P → ¬¬P | add proposition hilb5 |
2 | Q → ¬¬Q | replace proposition variable P by Q in 1 |
3 | (¬P ∨ ¬Q) → ¬¬(¬P ∨ ¬Q) | replace proposition variable Q by ¬P ∨ ¬Q in 2 |
4 | (¬P ∨ ¬Q) → ¬(P ∧ Q) | reverse abbreviation and in 3 at occurence 1 |
qed |
Negation of a disjunction:
3. Proposition
¬(P ∨ Q) → (¬P ∧ ¬Q) (hilb20)
1 | P → P | add proposition hilb2 |
2 | Q → Q | replace proposition variable P by Q in 1 |
3 | ¬(P ∨ Q) → ¬(P ∨ Q) | replace proposition variable Q by ¬(P ∨ Q) in 2 |
4 | ¬(P ∨ Q) → ¬(¬¬P ∨ Q) | elementary equivalence in 3 at 8 of hilb5 with hilb6 |
5 | ¬(P ∨ Q) → ¬(¬¬P ∨ ¬¬Q) | elementary equivalence in 4 at 11 of hilb5 with hilb6 |
6 | ¬(P ∨ Q) → (¬P ∧ ¬Q) | reverse abbreviation and in 5 at occurence 1 |
qed |
Reverse of a negation of a disjunction:
4. Proposition
(¬P ∧ ¬Q) → ¬(P ∨ Q) (hilb21)
1 | P → P | add proposition hilb2 |
2 | Q → Q | replace proposition variable P by Q in 1 |
3 | ¬(P ∨ Q) → ¬(P ∨ Q) | replace proposition variable Q by ¬(P ∨ Q) in 2 |
4 | ¬(¬¬P ∨ Q) → ¬(P ∨ Q) | elementary equivalence in 3 at 4 of hilb5 with hilb6 |
5 | ¬(¬¬P ∨ ¬¬Q) → ¬(P ∨ Q) | elementary equivalence in 4 at 7 of hilb5 with hilb6 |
6 | (¬P ∧ ¬Q) → ¬(P ∨ Q) | reverse abbreviation and in 5 at occurence 1 |
qed |
The Conjunction is commutative:
5. Proposition
(P ∧ Q) → (Q ∧ P) (hilb22)
1 | P → P | add proposition hilb2 |
2 | Q → Q | replace proposition variable P by Q in 1 |
3 | (P ∧ Q) → (P ∧ Q) | replace proposition variable Q by P ∧ Q in 2 |
4 | (P ∧ Q) → ¬(¬P ∨ ¬Q) | use abbreviation and in 3 at occurence 2 |
5 | (P ∧ Q) → ¬(¬Q ∨ ¬P) | elementary equivalence in 4 at 1 of hilb9 with hilb10 |
6 | (P ∧ Q) → (Q ∧ P) | reverse abbreviation and in 5 at occurence 1 |
qed |
A technical lemma that is simular to the previous one:
6. Proposition
(Q ∧ P) → (P ∧ Q) (hilb23)
1 | (P ∧ Q) → (Q ∧ P) | add proposition hilb22 |
2 | (P ∧ A) → (A ∧ P) | replace proposition variable Q by A in 1 |
3 | (B ∧ A) → (A ∧ B) | replace proposition variable P by B in 2 |
4 | (B ∧ P) → (P ∧ B) | replace proposition variable A by P in 3 |
5 | (Q ∧ P) → (P ∧ Q) | replace proposition variable B by Q in 4 |
qed |
Reduction of a conjunction:
7. Proposition
(P ∧ Q) → P (hilb24)
1 | P → (P ∨ Q) | add axiom axiom2 |
2 | P → (P ∨ A) | replace proposition variable Q by A in 1 |
3 | B → (B ∨ A) | replace proposition variable P by B in 2 |
4 | B → (B ∨ ¬Q) | replace proposition variable A by ¬Q in 3 |
5 | ¬P → (¬P ∨ ¬Q) | replace proposition variable B by ¬P in 4 |
6 | (P → Q) → (¬Q → ¬P) | add proposition hilb7 |
7 | (P → A) → (¬A → ¬P) | replace proposition variable Q by A in 6 |
8 | (B → A) → (¬A → ¬B) | replace proposition variable P by B in 7 |
9 | (B → (¬P ∨ ¬Q)) → (¬(¬P ∨ ¬Q) → ¬B) | replace proposition variable A by ¬P ∨ ¬Q in 8 |
10 | (¬P → (¬P ∨ ¬Q)) → (¬(¬P ∨ ¬Q) → ¬¬P) | replace proposition variable B by ¬P in 9 |
11 | ¬(¬P ∨ ¬Q) → ¬¬P | modus ponens with 5, 10 |
12 | (P ∧ Q) → ¬¬P | reverse abbreviation and in 11 at occurence 1 |
13 | (P ∧ Q) → P | elementary equivalence in 12 at 1 of hilb6 with hilb5 |
qed |
Another form of a reduction of a conjunction:
8. Proposition
(P ∧ Q) → Q (hilb25)
1 | (P ∧ Q) → P | add proposition hilb24 |
2 | (P ∧ A) → P | replace proposition variable Q by A in 1 |
3 | (B ∧ A) → B | replace proposition variable P by B in 2 |
4 | (B ∧ P) → B | replace proposition variable A by P in 3 |
5 | (Q ∧ P) → Q | replace proposition variable B by Q in 4 |
6 | (P ∧ Q) → Q | elementary equivalence in 5 at 1 of hilb22 with hilb23 |
qed |
The conjunction is associative too (first implication):
9. Proposition
(P ∧ (Q ∧ A)) → ((P ∧ Q) ∧ A) (hilb26)
1 | ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) | add proposition hilb15 |
2 | (P → Q) → (¬Q → ¬P) | add proposition hilb7 |
3 | (P → A) → (¬A → ¬P) | replace proposition variable Q by A in 2 |
4 | (B → A) → (¬A → ¬B) | replace proposition variable P by B in 3 |
5 | (B → (P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) → ¬B) | replace proposition variable A by P ∨ (Q ∨ A) in 4 |
6 | (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))) → (¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A)) | replace proposition variable B by (P ∨ Q) ∨ A in 5 |
7 | ¬(P ∨ (Q ∨ A)) → ¬((P ∨ Q) ∨ A) | modus ponens with 1, 6 |
8 | ¬(P ∨ ¬¬(Q ∨ A)) → ¬((P ∨ Q) ∨ A) | elementary equivalence in 7 at 5 of hilb5 with hilb6 |
9 | ¬(P ∨ ¬¬(Q ∨ A)) → ¬(¬¬(P ∨ Q) ∨ A) | elementary equivalence in 8 at 12 of hilb5 with hilb6 |
10 | ¬(P ∨ ¬¬(Q ∨ B)) → ¬(¬¬(P ∨ Q) ∨ B) | replace proposition variable A by B in 9 |
11 | ¬(P ∨ ¬¬(C ∨ B)) → ¬(¬¬(P ∨ C) ∨ B) | replace proposition variable Q by C in 10 |
12 | ¬(D ∨ ¬¬(C ∨ B)) → ¬(¬¬(D ∨ C) ∨ B) | replace proposition variable P by D in 11 |
13 | ¬(D ∨ ¬¬(C ∨ ¬A)) → ¬(¬¬(D ∨ C) ∨ ¬A) | replace proposition variable B by ¬A in 12 |
14 | ¬(D ∨ ¬¬(¬Q ∨ ¬A)) → ¬(¬¬(D ∨ ¬Q) ∨ ¬A) | replace proposition variable C by ¬Q in 13 |
15 | ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) → ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) | replace proposition variable D by ¬P in 14 |
16 | (P ∧ ¬(¬Q ∨ ¬A)) → ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) | reverse abbreviation and in 15 at occurence 1 |
17 | (P ∧ (Q ∧ A)) → ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) | reverse abbreviation and in 16 at occurence 1 |
18 | (P ∧ (Q ∧ A)) → (¬(¬P ∨ ¬Q) ∧ A) | reverse abbreviation and in 17 at occurence 1 |
19 | (P ∧ (Q ∧ A)) → ((P ∧ Q) ∧ A) | reverse abbreviation and in 18 at occurence 1 |
qed |
The conjunction is associative (second implication):
10. Proposition
((P ∧ Q) ∧ A) → (P ∧ (Q ∧ A)) (hilb27)
1 | (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) | add proposition hilb14 |
2 | (P → Q) → (¬Q → ¬P) | add proposition hilb7 |
3 | (P → A) → (¬A → ¬P) | replace proposition variable Q by A in 2 |
4 | (B → A) → (¬A → ¬B) | replace proposition variable P by B in 3 |
5 | (B → ((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) → ¬B) | replace proposition variable A by (P ∨ Q) ∨ A in 4 |
6 | ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A))) | replace proposition variable B by P ∨ (Q ∨ A) in 5 |
7 | ¬((P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A)) | modus ponens with 1, 6 |
8 | ¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ (Q ∨ A)) | elementary equivalence in 7 at 4 of hilb5 with hilb6 |
9 | ¬(¬¬(P ∨ Q) ∨ A) → ¬(P ∨ ¬¬(Q ∨ A)) | elementary equivalence in 8 at 13 of hilb5 with hilb6 |
10 | ¬(¬¬(P ∨ Q) ∨ B) → ¬(P ∨ ¬¬(Q ∨ B)) | replace proposition variable A by B in 9 |
11 | ¬(¬¬(P ∨ C) ∨ B) → ¬(P ∨ ¬¬(C ∨ B)) | replace proposition variable Q by C in 10 |
12 | ¬(¬¬(D ∨ C) ∨ B) → ¬(D ∨ ¬¬(C ∨ B)) | replace proposition variable P by D in 11 |
13 | ¬(¬¬(D ∨ C) ∨ ¬A) → ¬(D ∨ ¬¬(C ∨ ¬A)) | replace proposition variable B by ¬A in 12 |
14 | ¬(¬¬(D ∨ ¬Q) ∨ ¬A) → ¬(D ∨ ¬¬(¬Q ∨ ¬A)) | replace proposition variable C by ¬Q in 13 |
15 | ¬(¬¬(¬P ∨ ¬Q) ∨ ¬A) → ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) | replace proposition variable D by ¬P in 14 |
16 | (¬(¬P ∨ ¬Q) ∧ A) → ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) | reverse abbreviation and in 15 at occurence 1 |
17 | ((P ∧ Q) ∧ A) → ¬(¬P ∨ ¬¬(¬Q ∨ ¬A)) | reverse abbreviation and in 16 at occurence 1 |
18 | ((P ∧ Q) ∧ A) → (P ∧ ¬(¬Q ∨ ¬A)) | reverse abbreviation and in 17 at occurence 1 |
19 | ((P ∧ Q) ∧ A) → (P ∧ (Q ∧ A)) | reverse abbreviation and in 18 at occurence 1 |
qed |
Form for the conjunction rule:
11. Proposition
P → (Q → (P ∧ Q)) (hilb28)
1 | P ∨ ¬P | add proposition hilb4 |
2 | (¬P ∨ ¬Q) ∨ ¬(¬P ∨ ¬Q) | replace proposition variable P by ¬P ∨ ¬Q in 1 |
3 | ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) | add proposition hilb15 |
4 | ((P ∨ Q) ∨ B) → (P ∨ (Q ∨ B)) | replace proposition variable A by B in 3 |
5 | ((P ∨ C) ∨ B) → (P ∨ (C ∨ B)) | replace proposition variable Q by C in 4 |
6 | ((D ∨ C) ∨ B) → (D ∨ (C ∨ B)) | replace proposition variable P by D in 5 |
7 | ((D ∨ C) ∨ ¬(¬P ∨ ¬Q)) → (D ∨ (C ∨ ¬(¬P ∨ ¬Q))) | replace proposition variable B by ¬(¬P ∨ ¬Q) in 6 |
8 | ((D ∨ ¬Q) ∨ ¬(¬P ∨ ¬Q)) → (D ∨ (¬Q ∨ ¬(¬P ∨ ¬Q))) | replace proposition variable C by ¬Q in 7 |
9 | ((¬P ∨ ¬Q) ∨ ¬(¬P ∨ ¬Q)) → (¬P ∨ (¬Q ∨ ¬(¬P ∨ ¬Q))) | replace proposition variable D by ¬P in 8 |
10 | ¬P ∨ (¬Q ∨ ¬(¬P ∨ ¬Q)) | modus ponens with 2, 9 |
11 | P → (¬Q ∨ ¬(¬P ∨ ¬Q)) | reverse abbreviation impl in 10 at occurence 1 |
12 | P → (Q → ¬(¬P ∨ ¬Q)) | reverse abbreviation impl in 11 at occurence 1 |
13 | P → (Q → (P ∧ Q)) | reverse abbreviation and in 12 at occurence 1 |
qed |
Preconditions could be put together in a conjunction (first direction):
12. Proposition
(P → (Q → A)) → ((P ∧ Q) → A) (hilb29)
1 | P → P | add proposition hilb2 |
2 | Q → Q | replace proposition variable P by Q in 1 |
3 | (P → (Q → A)) → (P → (Q → A)) | replace proposition variable Q by P → (Q → A) in 2 |
4 | (P → (Q → A)) → (¬P ∨ (Q → A)) | use abbreviation impl in 3 at occurence 4 |
5 | (P → (Q → A)) → (¬P ∨ (¬Q ∨ A)) | use abbreviation impl in 4 at occurence 4 |
6 | (P → (Q → A)) → ((¬P ∨ ¬Q) ∨ A) | elementary equivalence in 5 at 1 of hilb14 with hilb15 |
7 | (P → (Q → A)) → (¬¬(¬P ∨ ¬Q) ∨ A) | elementary equivalence in 6 at 8 of hilb5 with hilb6 |
8 | (P → (Q → A)) → (¬(¬P ∨ ¬Q) → A) | reverse abbreviation impl in 7 at occurence 1 |
9 | (P → (Q → A)) → ((P ∧ Q) → A) | reverse abbreviation and in 8 at occurence 1 |
qed |
Preconditions could be put together in a conjunction (second direction):
13. Proposition
((P ∧ Q) → A) → (P → (Q → A)) (hilb30)
1 | P → P | add proposition hilb2 |
2 | Q → Q | replace proposition variable P by Q in 1 |
3 | (P → (Q → A)) → (P → (Q → A)) | replace proposition variable Q by P → (Q → A) in 2 |
4 | (¬P ∨ (Q → A)) → (P → (Q → A)) | use abbreviation impl in 3 at occurence 2 |
5 | (¬P ∨ (¬Q ∨ A)) → (P → (Q → A)) | use abbreviation impl in 4 at occurence 2 |
6 | ((¬P ∨ ¬Q) ∨ A) → (P → (Q → A)) | elementary equivalence in 5 at 1 of hilb14 with hilb15 |
7 | (¬¬(¬P ∨ ¬Q) ∨ A) → (P → (Q → A)) | elementary equivalence in 6 at 3 of hilb5 with hilb6 |
8 | (¬(¬P ∨ ¬Q) → A) → (P → (Q → A)) | reverse abbreviation impl in 7 at occurence 1 |
9 | ((P ∧ Q) → A) → (P → (Q → A)) | reverse abbreviation and in 8 at occurence 1 |
qed |
Absorbtion of a conjunction (first direction):
14. Proposition
(P ∧ P) → P (hilb31)
1 | (P ∧ Q) → P | add proposition hilb24 |
2 | (P ∧ P) → P | replace proposition variable Q by P in 1 |
qed |
Absorbtion of a conjunction (second direction):
15. Proposition
P → (P ∧ P) (hilb32)
1 | (P ∨ P) → P | add proposition hilb11 |
2 | (P → Q) → (¬Q → ¬P) | add proposition hilb7 |
3 | (P → A) → (¬A → ¬P) | replace proposition variable Q by A in 2 |
4 | (B → A) → (¬A → ¬B) | replace proposition variable P by B in 3 |
5 | (B → P) → (¬P → ¬B) | replace proposition variable A by P in 4 |
6 | ((P ∨ P) → P) → (¬P → ¬(P ∨ P)) | replace proposition variable B by P ∨ P in 5 |
7 | ¬P → ¬(P ∨ P) | modus ponens with 1, 6 |
8 | ¬Q → ¬(Q ∨ Q) | replace proposition variable P by Q in 7 |
9 | ¬¬P → ¬(¬P ∨ ¬P) | replace proposition variable Q by ¬P in 8 |
10 | P → ¬(¬P ∨ ¬P) | elementary equivalence in 9 at 1 of hilb6 with hilb5 |
11 | P → (P ∧ P) | reverse abbreviation and in 10 at occurence 1 |
qed |
Absorbtion of identical preconditions (first direction):
16. Proposition
(P → (P → Q)) → (P → Q) (hilb33)
1 | (P → (Q → A)) → ((P ∧ Q) → A) | add proposition hilb29 |
2 | (P → (Q → B)) → ((P ∧ Q) → B) | replace proposition variable A by B in 1 |
3 | (P → (C → B)) → ((P ∧ C) → B) | replace proposition variable Q by C in 2 |
4 | (D → (C → B)) → ((D ∧ C) → B) | replace proposition variable P by D in 3 |
5 | (D → (C → Q)) → ((D ∧ C) → Q) | replace proposition variable B by Q in 4 |
6 | (D → (P → Q)) → ((D ∧ P) → Q) | replace proposition variable C by P in 5 |
7 | (P → (P → Q)) → ((P ∧ P) → Q) | replace proposition variable D by P in 6 |
8 | (P → (P → Q)) → (P → Q) | elementary equivalence in 7 at 1 of hilb31 with hilb32 |
qed |
Absorbtion of identical preconditions (second direction):
17. Proposition
(P → Q) → (P → (P → Q)) (hilb34)
1 | ((P ∧ Q) → A) → (P → (Q → A)) | add proposition hilb30 |
2 | ((P ∧ Q) → B) → (P → (Q → B)) | replace proposition variable A by B in 1 |
3 | ((P ∧ C) → B) → (P → (C → B)) | replace proposition variable Q by C in 2 |
4 | ((D ∧ C) → B) → (D → (C → B)) | replace proposition variable P by D in 3 |
5 | ((D ∧ C) → Q) → (D → (C → Q)) | replace proposition variable B by Q in 4 |
6 | ((D ∧ P) → Q) → (D → (P → Q)) | replace proposition variable C by P in 5 |
7 | ((P ∧ P) → Q) → (P → (P → Q)) | replace proposition variable D by P in 6 |
8 | (P → Q) → (P → (P → Q)) | elementary equivalence in 7 at 1 of hilb31 with hilb32 |
qed |