for questions or link request: module admin

Further Theorems of Propositional Calculus

name: prophilbert2, module version: 1.00.00, rule version: 1.00.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 hilb6
2 (ØØQ ® Q) replace proposition variable P by Q in 1
3 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
4 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 3
5 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 4
6 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 5
7 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 6
8 ((D ® P) ® ((Q Ú D) ® (Q Ú P))) replace proposition variable C by P in 7
9 ((ØØP ® P) ® ((Q Ú ØØP) ® (Q Ú P))) replace proposition variable D by ØØP in 8
10 ((Q Ú ØØP) ® (Q Ú P)) modus ponens with 1, 9
11 ((P Ú Q) ® (Q Ú P)) add axiom axiom3
12 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 11
13 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 12
14 ((B Ú P) ® (P Ú B)) replace proposition variable A by P in 13
15 ((Q Ú P) ® (P Ú Q)) replace proposition variable B by Q in 14
16 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1
17 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 16
18 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 17
19 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 18
20 ((D ® C) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® C))) replace proposition variable B by (Q Ú ØØP) in 19
21 ((D ® (P Ú Q)) ® (((Q Ú ØØP) ® D) ® ((Q Ú ØØP) ® (P Ú Q)))) replace proposition variable C by (P Ú Q) in 20
22 (((Q Ú P) ® (P Ú Q)) ® (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q)))) replace proposition variable D by (Q Ú P) in 21
23 (((Q Ú ØØP) ® (Q Ú P)) ® ((Q Ú ØØP) ® (P Ú Q))) modus ponens with 15, 22
24 ((Q Ú ØØP) ® (P Ú Q)) modus ponens with 10, 23
25 ((B Ú Q) ® (Q Ú B)) replace proposition variable A by Q in 13
26 ((ØØP Ú Q) ® (Q Ú ØØP)) replace proposition variable B by ØØP in 25
27 ((D ® C) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® C))) replace proposition variable B by (ØØP Ú Q) in 19
28 ((D ® (P Ú Q)) ® (((ØØP Ú Q) ® D) ® ((ØØP Ú Q) ® (P Ú Q)))) replace proposition variable C by (P Ú Q) in 27
29 (((Q Ú ØØP) ® (P Ú Q)) ® (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q)))) replace proposition variable D by (Q Ú ØØP) in 28
30 (((ØØP Ú Q) ® (Q Ú ØØP)) ® ((ØØP Ú Q) ® (P Ú Q))) modus ponens with 24, 29
31 ((ØØP Ú Q) ® (P Ú Q)) modus ponens with 26, 30
32 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7
33 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 32
34 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 33
35 ((B ® (P Ú Q)) ® (Ø(P Ú Q) ® ØB)) replace proposition variable A by (P Ú Q) in 34
36 (((ØØP Ú Q) ® (P Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú Q))) replace proposition variable B by (ØØP Ú Q) in 35
37 (Ø(P Ú Q) ® Ø(ØØP Ú Q)) modus ponens with 31, 36
38 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
39 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2
40 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 38
41 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 40
42 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 39
43 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 42
44 ((D ® C) ® ((ØØP Ú D) ® (ØØP Ú C))) replace proposition variable B by ØØP in 6
45 ((D ® Q) ® ((ØØP Ú D) ® (ØØP Ú Q))) replace proposition variable C by Q in 44
46 ((ØØQ ® Q) ® ((ØØP Ú ØØQ) ® (ØØP Ú Q))) replace proposition variable D by ØØQ in 45
47 ((ØØP Ú ØØQ) ® (ØØP Ú Q)) modus ponens with 2, 46
48 ((B ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® ØB)) replace proposition variable A by (ØØP Ú Q) in 34
49 (((ØØP Ú ØØQ) ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ))) replace proposition variable B by (ØØP Ú ØØQ) in 48
50 (Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) modus ponens with 47, 49
51 ((D ® C) ® ((ØØ(P Ú Q) Ú D) ® (ØØ(P Ú Q) Ú C))) replace proposition variable B by ØØ(P Ú Q) in 6
52 ((D ® Ø(ØØP Ú ØØQ)) ® ((ØØ(P Ú Q) Ú D) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) replace proposition variable C by Ø(ØØP Ú ØØQ) in 51
53 ((Ø(ØØP Ú Q) ® Ø(ØØP Ú ØØQ)) ® ((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) replace proposition variable D by Ø(ØØP Ú Q) in 52
54 ((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) modus ponens with 50, 53
55 ((B ® Ø(ØØP Ú Q)) ® (ØB Ú Ø(ØØP Ú Q))) replace proposition variable A by Ø(ØØP Ú Q) in 41
56 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) replace proposition variable B by Ø(P Ú Q) in 55
57 ((D ® C) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® C))) replace proposition variable B by (Ø(P Ú Q) ® Ø(ØØP Ú Q)) in 19
58 ((D ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))))) replace proposition variable C by (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) in 57
59 (((ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))))) replace proposition variable D by (ØØ(P Ú Q) Ú Ø(ØØP Ú Q)) in 58
60 (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú Q))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)))) modus ponens with 54, 59
61 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) modus ponens with 56, 60
62 ((ØB Ú Ø(ØØP Ú ØØQ)) ® (B ® Ø(ØØP Ú ØØQ))) replace proposition variable A by Ø(ØØP Ú ØØQ) in 43
63 ((ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) replace proposition variable B by Ø(P Ú Q) in 62
64 ((D ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))))) replace proposition variable C by (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ)) in 57
65 (((ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) ® (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))))) replace proposition variable D by (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ)) in 64
66 (((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (ØØ(P Ú Q) Ú Ø(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ)))) modus ponens with 63, 65
67 ((Ø(P Ú Q) ® Ø(ØØP Ú Q)) ® (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ))) modus ponens with 61, 66
68 (Ø(P Ú Q) ® Ø(ØØP Ú ØØQ)) modus ponens with 37, 67
69 (Ø(P Ú Q) ® (ØP Ù ØQ)) reverse abbreviation and in 68 at occurence 1
qed

Reverse of a negation of a disjunction:

4. Proposition
      ((ØP Ù ØQ) ® Ø(P Ú Q))     (hilb21)

Proof:
1 (P ® ØØP) add proposition hilb5
2 (Q ® ØØQ) replace proposition variable P by Q in 1
3 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
4 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 3
5 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 4
6 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 5
7 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 6
8 ((D ® ØØP) ® ((Q Ú D) ® (Q Ú ØØP))) replace proposition variable C by ØØP in 7
9 ((P ® ØØP) ® ((Q Ú P) ® (Q Ú ØØP))) replace proposition variable D by P in 8
10 ((Q Ú P) ® (Q Ú ØØP)) modus ponens with 1, 9
11 ((P Ú Q) ® (Q Ú P)) add axiom axiom3
12 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 11
13 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 12
14 ((B Ú ØØP) ® (ØØP Ú B)) replace proposition variable A by ØØP in 13
15 ((Q Ú ØØP) ® (ØØP Ú Q)) replace proposition variable B by Q in 14
16 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1
17 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 16
18 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 17
19 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 18
20 ((D ® C) ® (((Q Ú P) ® D) ® ((Q Ú P) ® C))) replace proposition variable B by (Q Ú P) in 19
21 ((D ® (ØØP Ú Q)) ® (((Q Ú P) ® D) ® ((Q Ú P) ® (ØØP Ú Q)))) replace proposition variable C by (ØØP Ú Q) in 20
22 (((Q Ú ØØP) ® (ØØP Ú Q)) ® (((Q Ú P) ® (Q Ú ØØP)) ® ((Q Ú P) ® (ØØP Ú Q)))) replace proposition variable D by (Q Ú ØØP) in 21
23 (((Q Ú P) ® (Q Ú ØØP)) ® ((Q Ú P) ® (ØØP Ú Q))) modus ponens with 15, 22
24 ((Q Ú P) ® (ØØP Ú Q)) modus ponens with 10, 23
25 ((D ® C) ® (((P Ú Q) ® D) ® ((P Ú Q) ® C))) replace proposition variable B by (P Ú Q) in 19
26 ((D ® (ØØP Ú Q)) ® (((P Ú Q) ® D) ® ((P Ú Q) ® (ØØP Ú Q)))) replace proposition variable C by (ØØP Ú Q) in 25
27 (((Q Ú P) ® (ØØP Ú Q)) ® (((P Ú Q) ® (Q Ú P)) ® ((P Ú Q) ® (ØØP Ú Q)))) replace proposition variable D by (Q Ú P) in 26
28 (((P Ú Q) ® (Q Ú P)) ® ((P Ú Q) ® (ØØP Ú Q))) modus ponens with 24, 27
29 ((P Ú Q) ® (ØØP Ú Q)) modus ponens with 11, 28
30 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7
31 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 30
32 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 31
33 ((B ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® ØB)) replace proposition variable A by (ØØP Ú Q) in 32
34 (((P Ú Q) ® (ØØP Ú Q)) ® (Ø(ØØP Ú Q) ® Ø(P Ú Q))) replace proposition variable B by (P Ú Q) in 33
35 (Ø(ØØP Ú Q) ® Ø(P Ú Q)) modus ponens with 29, 34
36 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
37 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2