for questions or link request: module admin

Further Theorems of Propositional Calculus

name: prophilbert2, module version: 1.00.00, rule version: 1.02.00, orignal: 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)

Uses the following modules:

Is used by the following modules:


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

This module is used by the following modules: