for questions or link request: module admin

Further Theorems of Propositional Calculus

name: prophilbert2, module version: 1.00.00, rule version: 1.02.00, original: prophilbert2, author of this module: Michael Meyling

Description

This module includes proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)

References

This document uses the results of the following documents:

Content

Negation of a conjunction:

1. Proposition
      ¬(P ∧ Q) → (¬P ∨ ¬Q)     (hilb18)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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)

Proof:
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

Cross References

This document is used by the following documents: