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
38 ((B Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú B)) replace proposition variable A by Ø(P Ú Q) in 13
39 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 36
40 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 39
41 ((B ® Ø(P Ú Q)) ® (ØB Ú Ø(P Ú Q))) replace proposition variable A by Ø(P Ú Q) in 40
42 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 37
43 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 42
44 ((ØB Ú Ø(P Ú Q)) ® (B ® Ø(P Ú Q))) replace proposition variable A by Ø(P Ú Q) in 43
45 ((D ® C) ® ((ØØP Ú D) ® (ØØP Ú C))) replace proposition variable B by ØØP in 6
46 ((D ® ØØQ) ® ((ØØP Ú D) ® (ØØP Ú ØØQ))) replace proposition variable C by ØØQ in 45
47 ((Q ® ØØQ) ® ((ØØP Ú Q) ® (ØØP Ú ØØQ))) replace proposition variable D by Q in 46
48 ((ØØP Ú Q) ® (ØØP Ú ØØQ)) modus ponens with 2, 47
49 ((B ® (ØØP Ú ØØQ)) ® (Ø(ØØP Ú ØØQ) ® ØB)) replace proposition variable A by (ØØP Ú ØØQ) in 32
50 (((ØØP Ú Q) ® (ØØP Ú ØØQ)) ® (Ø(ØØP Ú ØØQ) ® Ø(ØØP Ú Q))) replace proposition variable B by (ØØP Ú Q) in 49
51 (Ø(ØØP Ú ØØQ) ® Ø(ØØP Ú Q)) modus ponens with 48, 50
52 ((B ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØB)) replace proposition variable A by Ø(ØØP Ú Q) in 32
53 ((Ø(ØØP Ú ØØQ) ® Ø(ØØP Ú Q)) ® (ØØ(ØØP Ú Q) ® ØØ(ØØP Ú ØØQ))) replace proposition variable B by Ø(ØØP Ú ØØQ) in 52
54 (ØØ(ØØP Ú Q) ® ØØ(ØØP Ú ØØQ)) modus ponens with 51, 53
55 ((D ® C) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú C))) replace proposition variable B by Ø(P Ú Q) in 6
56 ((D ® ØØ(ØØP Ú ØØQ)) ® ((Ø(P Ú Q) Ú D) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)))) replace proposition variable C by ØØ(ØØP Ú ØØQ) in 55
57 ((ØØ(ØØP Ú Q) ® ØØ(ØØP Ú ØØQ)) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)))) replace proposition variable D by ØØ(ØØP Ú Q) in 56
58 ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) modus ponens with 54, 57
59 ((B Ú ØØ(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) Ú B)) replace proposition variable A by ØØ(ØØP Ú ØØQ) in 13
60 ((Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) replace proposition variable B by Ø(P Ú Q) in 59
61 ((D ® C) ® (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® D) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® C))) replace proposition variable B by (Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) in 19
62 ((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 61
63 (((Ø(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 62
64 (((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú ØØQ))) ® ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) modus ponens with 60, 63
65 ((Ø(P Ú Q) Ú ØØ(ØØP Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) modus ponens with 58, 64
66 ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) replace proposition variable B by ØØ(ØØP Ú Q) in 38
67 ((D ® C) ® (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® D) ® ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® C))) replace proposition variable B by (ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) in 19
68 ((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 67
69 (((Ø(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 68
70 (((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (Ø(P Ú Q) Ú ØØ(ØØP Ú Q))) ® ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) modus ponens with 65, 69
71 ((ØØ(ØØP Ú Q) Ú Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) modus ponens with 66, 70
72 ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) replace proposition variable B by Ø(ØØP Ú Q) in 41
73 ((D ® C) ® (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® D) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® C))) replace proposition variable B by (Ø(ØØP Ú Q) ® Ø(P Ú Q)) in 19
74 ((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 73
75 (((ØØ(ØØ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 74
76 (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú Q) Ú Ø(P Ú Q))) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)))) modus ponens with 71, 75
77 ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) modus ponens with 72, 76
78 ((ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))) replace proposition variable B by Ø(ØØP Ú ØØQ) in 44
79 ((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 73
80 (((ØØ(ØØ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 79
81 (((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (ØØ(ØØP Ú ØØQ) Ú Ø(P Ú Q))) ® ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q)))) modus ponens with 78, 80
82 ((Ø(ØØP Ú Q) ® Ø(P Ú Q)) ® (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q))) modus ponens with 77, 81
83 (Ø(ØØP Ú ØØQ) ® Ø(P Ú Q)) modus ponens with 35, 82
84 ((ØP Ù ØQ) ® Ø(P Ú Q)) reverse abbreviation and in 83 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 ((Q Ú P) ® (P Ú Q)) add proposition hilb10
6 ((A Ú P) ® (P Ú A)) replace proposition variable Q by A in 5
7 ((A Ú B) ® (B Ú A)) replace proposition variable P by B in 6
8 ((ØQ Ú B) ® (B Ú ØQ)) replace proposition variable A by ØQ in 7
9 ((ØQ Ú ØP) ® (ØP Ú ØQ)) replace proposition variable B by ØP in 8
10 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7
11 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 10
12 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 11
13 ((B ® (ØP Ú ØQ)) ® (Ø(ØP Ú ØQ) ® ØB)) replace proposition variable A by (ØP Ú ØQ) in 12
14 (((ØQ Ú ØP) ® (ØP Ú ØQ)) ® (Ø(ØP Ú ØQ) ® Ø(ØQ Ú ØP))) replace proposition variable B by (ØQ Ú ØP) in 13
15 (Ø(ØP Ú ØQ) ® Ø(ØQ Ú ØP)) modus ponens with 9, 14
16 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
17 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2
18 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
19 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 18
20 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 19
21 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 20
22 ((D ® C) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú C))) replace proposition variable B by Ø(P Ù Q) in 21
23 ((D ® Ø(ØQ Ú ØP)) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) replace proposition variable C by Ø(ØQ Ú ØP) in 22
24 ((Ø(ØP Ú ØQ) ® Ø(ØQ Ú ØP)) ® ((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) replace proposition variable D by Ø(ØP Ú ØQ) in 23
25 ((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) modus ponens with 15, 24
26 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 16
27 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 26
28 ((B ® Ø(ØP Ú ØQ)) ® (ØB Ú Ø(ØP Ú ØQ))) replace proposition variable A by Ø(ØP Ú ØQ) in 27
29 (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) replace proposition variable B by (P Ù Q) in 28
30 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1
31 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 30
32 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 31
33 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 32
34 ((D ® C) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® D) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® C))) replace proposition variable B by ((P Ù Q) ® Ø(ØP Ú ØQ)) in 33
35 ((D ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® D) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))))) replace proposition variable C by (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) in 34
36 (((Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))))) replace proposition variable D by (Ø(P Ù Q) Ú Ø(ØP Ú ØQ)) in 35
37 ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØP Ú ØQ))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)))) modus ponens with 25, 36
38 (((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) modus ponens with 29, 37
39 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 17
40 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 39
41 ((ØB Ú Ø(ØQ Ú ØP)) ® (B ® Ø(ØQ Ú ØP))) replace proposition variable A by Ø(ØQ Ú ØP) in 40
42 ((Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))) replace proposition variable B by (P Ù Q) in 41
43 ((D ® ((P Ù Q) ® Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® D) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))))) replace proposition variable C by ((P Ù Q) ® Ø(ØQ Ú ØP)) in 34
44 (((Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))) ® ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))))) replace proposition variable D by (Ø(P Ù Q) Ú Ø(ØQ Ú ØP)) in 43
45 ((((P Ù Q) ® Ø(ØP Ú ØQ)) ® (Ø(P Ù Q) Ú Ø(ØQ Ú ØP))) ® (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP)))) modus ponens with 42, 44
46 (((P Ù Q) ® Ø(ØP Ú ØQ)) ® ((P Ù Q) ® Ø(ØQ Ú ØP))) modus ponens with 38, 45
47 ((P Ù Q) ® Ø(ØQ Ú ØP)) modus ponens with 4, 46
48 ((P Ù Q) ® (Q Ù P)) reverse abbreviation and in 47 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 ® P) add proposition hilb6
14 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
15 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2
16 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
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) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú C))) replace proposition variable B by Ø(P Ù Q) in 19
21 ((D ® P) ® ((Ø(P Ù Q) Ú D) ® (Ø(P Ù Q) Ú P))) replace proposition variable C by P in 20
22 ((ØØP ® P) ® ((Ø(P Ù Q) Ú ØØP) ® (Ø(P Ù Q) Ú P))) replace proposition variable D by ØØP in 21
23 ((Ø(P Ù Q) Ú ØØP) ® (Ø(P Ù Q) Ú P)) modus ponens with 13, 22
24 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 14
25 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 24
26 ((B ® ØØP) ® (ØB Ú ØØP)) replace proposition variable A by ØØP in 25
27 (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú ØØP)) replace proposition variable B by (P Ù Q) in 26
28 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1
29 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 28
30 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 29
31 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 30
32 ((D ® C) ® ((((P Ù Q) ® ØØP) ® D) ® (((P Ù Q) ® ØØP) ® C))) replace proposition variable B by ((P Ù Q) ® ØØP) in 31
33 ((D ® (Ø(P Ù Q) Ú P)) ® ((((P Ù Q) ® ØØP) ® D) ® (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)))) replace proposition variable C by (Ø(P Ù Q) Ú P) in 32
34 (((Ø(P Ù Q) Ú ØØP) ® (Ø(P Ù Q) Ú P)) ® ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú ØØP)) ® (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)))) replace proposition variable D by (Ø(P Ù Q) Ú ØØP) in 33
35 ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú ØØP)) ® (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P))) modus ponens with 23, 34
36 (((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)) modus ponens with 27, 35
37 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 15
38 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 37
39 ((ØB Ú P) ® (B ® P)) replace proposition variable A by P in 38
40 ((Ø(P Ù Q) Ú P) ® ((P Ù Q) ® P)) replace proposition variable B by (P Ù Q) in 39
41 ((D ® ((P Ù Q) ® P)) ® ((((P Ù Q) ® ØØP) ® D) ® (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P)))) replace proposition variable C by ((P Ù Q) ® P) in 32
42 (((Ø(P Ù Q) Ú P) ® ((P Ù Q) ® P)) ® ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)) ® (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P)))) replace proposition variable D by (Ø(P Ù Q) Ú P) in 41
43 ((((P Ù Q) ® ØØP) ® (Ø(P Ù Q) Ú P)) ® (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P))) modus ponens with 40, 42
44 (((P Ù Q) ® ØØP) ® ((P Ù Q) ® P)) modus ponens with 36, 43
45 ((P Ù Q) ® P) modus ponens with 12, 44
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 ((Q Ù P) ® (P Ù Q)) add proposition hilb23
7 ((A Ù P) ® (P Ù A)) replace proposition variable Q by A in 6
8 ((A Ù B) ® (B Ù A)) replace proposition variable P by B in 7
9 ((P Ù B) ® (B Ù P)) replace proposition variable A by P in 8
10 ((P Ù Q) ® (Q Ù P)) replace proposition variable B by Q in 9
11 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
12 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2
13 ((P ® Q) ® (ØQ ® ØP)) add proposition hilb7
14 ((P ® A) ® (ØA ® ØP)) replace proposition variable Q by A in 13
15 ((B ® A) ® (ØA ® ØB)) replace proposition variable P by B in 14
16 ((B ® (Q Ù P)) ® (Ø(Q Ù P) ® ØB)) replace proposition variable A by (Q Ù P) in 15
17 (((P Ù Q) ® (Q Ù P)) ® (Ø(Q Ù P) ® Ø(P Ù Q))) replace proposition variable B by (P Ù Q) in 16
18 (Ø(Q Ù P) ® Ø(P Ù Q)) modus ponens with 10, 17
19 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
20 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 19
21 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 20
22 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 21
23 ((D ® C) ® ((Q Ú D) ® (Q Ú C))) replace proposition variable B by Q in 22
24 ((D ® Ø(P Ù Q)) ® ((Q Ú D) ® (Q Ú Ø(P Ù Q)))) replace proposition variable C by Ø(P Ù Q) in 23
25 ((Ø(Q Ù P) ® Ø(P Ù Q)) ® ((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q)))) replace proposition variable D by Ø(Q Ù P) in 24
26 ((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q))) modus ponens with 18, 25
27 ((P Ú Q) ® (Q Ú P)) add axiom axiom3
28 ((P Ú A) ® (A Ú P)) replace proposition variable Q by A in 27
29 ((B Ú A) ® (A Ú B)) replace proposition variable P by B in 28
30 ((B Ú Ø(P Ù Q)) ® (Ø(P Ù Q) Ú B)) replace proposition variable A by Ø(P Ù Q) in 29
31 ((Q Ú Ø(P Ù Q)) ® (Ø(P Ù Q) Ú Q)) replace proposition variable B by Q in 30
32 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1
33 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 32
34 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 33
35 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 34
36 ((D ® C) ® (((Q Ú Ø(Q Ù P)) ® D) ® ((Q Ú Ø(Q Ù P)) ® C))) replace proposition variable B by (Q Ú Ø(Q Ù P)) in 35
37 ((D ® (Ø(P Ù Q) Ú Q)) ® (((Q Ú Ø(Q Ù P)) ® D) ® ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable C by (Ø(P Ù Q) Ú Q) in 36
38 (((Q Ú Ø(P Ù Q)) ® (Ø(P Ù Q) Ú Q)) ® (((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q))) ® ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable D by (Q Ú Ø(P Ù Q)) in 37
39 (((Q Ú Ø(Q Ù P)) ® (Q Ú Ø(P Ù Q))) ® ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q))) modus ponens with 31, 38
40 ((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)) modus ponens with 26, 39
41 ((B Ú Q) ® (Q Ú B)) replace proposition variable A by Q in 29
42 ((Ø(Q Ù P) Ú Q) ® (Q Ú Ø(Q Ù P))) replace proposition variable B by Ø(Q Ù P) in 41
43 ((D ® C) ® (((Ø(Q Ù P) Ú Q) ® D) ® ((Ø(Q Ù P) Ú Q) ® C))) replace proposition variable B by (Ø(Q Ù P) Ú Q) in 35
44 ((D ® (Ø(P Ù Q) Ú Q)) ® (((Ø(Q Ù P) Ú Q) ® D) ® ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable C by (Ø(P Ù Q) Ú Q) in 43
45 (((Q Ú Ø(Q Ù P)) ® (Ø(P Ù Q) Ú Q)) ® (((Ø(Q Ù P) Ú Q) ® (Q Ú Ø(Q Ù P))) ® ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable D by (Q Ú Ø(Q Ù P)) in 44
46 (((Ø(Q Ù P) Ú Q) ® (Q Ú Ø(Q Ù P))) ® ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q))) modus ponens with 40, 45
47 ((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)) modus ponens with 42, 46
48 ((P ® A) ® (ØP Ú A)) replace proposition variable Q by A in 11
49 ((B ® A) ® (ØB Ú A)) replace proposition variable P by B in 48
50 ((B ® Q) ® (ØB Ú Q)) replace proposition variable A by Q in 49
51 (((Q Ù P) ® Q) ® (Ø(Q Ù P) Ú Q)) replace proposition variable B by (Q Ù P) in 50
52 ((D ® C) ® ((((Q Ù P) ® Q) ® D) ® (((Q Ù P) ® Q) ® C))) replace proposition variable B by ((Q Ù P) ® Q) in 35
53 ((D ® (Ø(P Ù Q) Ú Q)) ® ((((Q Ù P) ® Q) ® D) ® (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable C by (Ø(P Ù Q) Ú Q) in 52
54 (((Ø(Q Ù P) Ú Q) ® (Ø(P Ù Q) Ú Q)) ® ((((Q Ù P) ® Q) ® (Ø(Q Ù P) Ú Q)) ® (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)))) replace proposition variable D by (Ø(Q Ù P) Ú Q) in 53
55 ((((Q Ù P) ® Q) ® (Ø(Q Ù P) Ú Q)) ® (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q))) modus ponens with 47, 54
56 (((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)) modus ponens with 51, 55
57 ((ØP Ú A) ® (P ® A)) replace proposition variable Q by A in 12
58 ((ØB Ú A) ® (B ® A)) replace proposition variable P by B in 57
59 ((ØB Ú Q) ® (B ® Q)) replace proposition variable A by Q in 58
60 ((Ø(P Ù Q) Ú Q) ® ((P Ù Q) ® Q)) replace proposition variable B by (P Ù Q) in 59
61 ((D ® ((P Ù Q) ® Q)) ® ((((Q Ù P) ® Q) ® D) ® (((Q Ù P) ® Q) ® ((P Ù Q) ® Q)))) replace proposition variable C by ((P Ù Q) ® Q) in 52
62 (((Ø(P Ù Q) Ú Q) ® ((P Ù Q) ® Q)) ® ((((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)) ® (((Q Ù P) ® Q) ® ((P Ù Q) ® Q)))) replace proposition variable D by (Ø(P Ù Q) Ú Q) in 61
63 ((((Q Ù P) ® Q) ® (Ø(P Ù Q) Ú Q)) ® (((Q Ù P) ® Q) ® ((P Ù Q) ® Q))) modus ponens with 60, 62
64 (((Q Ù P) ® Q) ® ((P Ù Q) ® Q)) modus ponens with 56, 63
65 ((P Ù Q) ® Q) modus ponens with 5, 64
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 ® ØØP) add proposition hilb5
9 (B ® ØØB) replace proposition variable P by B in 8
10 ((Q Ú A) ® ØØ(Q Ú A)) replace proposition variable B by (Q Ú A) in 9
11 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4
12 ((P ® Q) ® ((B Ú P) ® (B Ú Q))) replace proposition variable A by B in 11
13 ((P ® C) ® ((B Ú P) ® (B Ú C))) replace proposition variable Q by C in 12
14 ((D ® C) ® ((B Ú D) ® (B Ú C))) replace proposition variable P by D in 13
15 ((D ® C) ® ((P Ú D) ® (P Ú C))) replace proposition variable B by P in 14
16 ((D ® ØØ(Q Ú A)) ® ((P Ú D) ® (P Ú ØØ(Q Ú A)))) replace proposition variable C by ØØ(Q Ú A) in 15
17 (((Q Ú A) ® ØØ(Q Ú A)) ® ((P Ú (Q Ú A)) ® (P Ú ØØ(Q Ú A)))) replace proposition variable D by (Q Ú A) in 16
18 ((P Ú (Q Ú A)) ® (P Ú ØØ(Q Ú A))) modus ponens with 10, 17
19 ((P ® B) ® (ØB ® ØP)) replace proposition variable Q by B in 2
20 ((C ® B) ® (ØB ® ØC)) replace proposition variable P by C in 19
21 ((C ® (P Ú ØØ(Q Ú A))) ® (Ø(P Ú ØØ(Q Ú A)) ® ØC)) replace proposition variable B by (P Ú ØØ(Q Ú A)) in 20
22 (((P Ú (Q Ú A)) ® (P Ú ØØ(Q Ú A))) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø(P Ú (Q Ú A)))) replace proposition variable C by (P Ú (Q Ú A)) in 21
23 (Ø(P Ú ØØ(Q Ú A)) ® Ø(P Ú (Q Ú A))) modus ponens with 18, 22
24 ((P ® Q) ® (ØP Ú Q)) add proposition defimpl1
25 ((ØP Ú Q) ® (P ® Q)) add proposition defimpl2
26 ((C ® Ø(P Ú (Q Ú A))) ® (ØØ(P Ú (Q Ú A)) ® ØC)) replace proposition variable B by Ø(P Ú (Q Ú A)) in 20
27 ((Ø(P Ú ØØ(Q Ú A)) ® Ø(P Ú (Q Ú A))) ® (ØØ(P Ú (Q Ú A)) ® ØØ(P Ú ØØ(Q Ú A)))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 26
28 (ØØ(P Ú (Q Ú A)) ® ØØ(P Ú ØØ(Q Ú A))) modus ponens with 23, 27
29 ((D ® C) ® ((Ø((P Ú Q) Ú A) Ú D) ® (Ø((P Ú Q) Ú A) Ú C))) replace proposition variable B by Ø((P Ú Q) Ú A) in 14
30 ((D ® ØØ(P Ú ØØ(Q Ú A))) ® ((Ø((P Ú Q) Ú A) Ú D) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))))) replace proposition variable C by ØØ(P Ú ØØ(Q Ú A)) in 29
31 ((ØØ(P Ú (Q Ú A)) ® ØØ(P Ú ØØ(Q Ú A))) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))))) replace proposition variable D by ØØ(P Ú (Q Ú A)) in 30
32 ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) modus ponens with 28, 31
33 ((P Ú Q) ® (Q Ú P)) add axiom axiom3
34 ((P Ú B) ® (B Ú P)) replace proposition variable Q by B in 33
35 ((C Ú B) ® (B Ú C)) replace proposition variable P by C in 34
36 ((C Ú ØØ(P Ú ØØ(Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú C)) replace proposition variable B by ØØ(P Ú ØØ(Q Ú A)) in 35
37 ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) replace proposition variable C by Ø((P Ú Q) Ú A) in 36
38 ((P ® Q) ® ((A ® P) ® (A ® Q))) add proposition hilb1
39 ((P ® Q) ® ((B ® P) ® (B ® Q))) replace proposition variable A by B in 38
40 ((P ® C) ® ((B ® P) ® (B ® C))) replace proposition variable Q by C in 39
41 ((D ® C) ® ((B ® D) ® (B ® C))) replace proposition variable P by D in 40
42 ((D ® C) ® (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® C))) replace proposition variable B by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) in 41
43 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® D) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 42
44 (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable D by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A))) in 43
45 (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú ØØ(Q Ú A)))) ® ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) modus ponens with 37, 44
46 ((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) modus ponens with 32, 45
47 ((C Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú C)) replace proposition variable B by Ø((P Ú Q) Ú A) in 35
48 ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) replace proposition variable C by ØØ(P Ú (Q Ú A)) in 47
49 ((D ® C) ® (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® D) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® C))) replace proposition variable B by (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 41
50 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® D) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 49
51 (((Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable D by (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A))) in 50
52 (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø((P Ú Q) Ú A) Ú ØØ(P Ú (Q Ú A)))) ® ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) modus ponens with 46, 51
53 ((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) modus ponens with 48, 52
54 ((P ® B) ® (ØP Ú B)) replace proposition variable Q by B in 24
55 ((C ® B) ® (ØC Ú B)) replace proposition variable P by C in 54
56 ((C ® Ø((P Ú Q) Ú A)) ® (ØC Ú Ø((P Ú Q) Ú A))) replace proposition variable B by Ø((P Ú Q) Ú A) in 55
57 ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) replace proposition variable C by Ø(P Ú (Q Ú A)) in 56
58 ((D ® C) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® C))) replace proposition variable B by (Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) in 41
59 ((D ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable C by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 58
60 (((ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))))) replace proposition variable D by (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 59
61 (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú (Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)))) modus ponens with 53, 60
62 ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) modus ponens with 57, 61
63 ((ØP Ú B) ® (P ® B)) replace proposition variable Q by B in 25
64 ((ØC Ú B) ® (C ® B)) replace proposition variable P by C in 63
65 ((ØC Ú Ø((P Ú Q) Ú A)) ® (C ® Ø((P Ú Q) Ú A))) replace proposition variable B by Ø((P Ú Q) Ú A) in 64
66 ((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) replace proposition variable C by Ø(P Ú ØØ(Q Ú A)) in 65
67 ((D ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® D) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))))) replace proposition variable C by (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) in 58
68 (((ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) ® (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))))) replace proposition variable D by (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A)) in 67
69 (((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (ØØ(P Ú ØØ(Q Ú A)) Ú Ø((P Ú Q) Ú A))) ® ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)))) modus ponens with 66, 68
70 ((Ø(P Ú (Q Ú A)) ® Ø((P Ú Q) Ú A)) ® (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A))) modus ponens with 62, 69
71 (Ø(P Ú ØØ(Q Ú A)) ® Ø((P Ú Q) Ú A)) modus ponens with 7, 70
72 (ØØP ® P) add proposition hilb6
73 (ØØA ® A) replace proposition variable P by A in 72
74 (ØØ(P Ú Q) ® (P Ú Q)) replace proposition variable A by (P Ú Q) in 73
75 ((D ® C) ® ((A Ú D) ® (A Ú C))) replace proposition variable B by A in 14
76 ((D ® (P Ú Q)) ® ((A Ú D) ® (A Ú (P Ú Q)))) replace proposition variable C by (P Ú Q) in 75
77 ((ØØ(P Ú Q) ® (P Ú Q)) ® ((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q)))) replace proposition variable D by ØØ(P Ú Q) in 76
78 ((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q))) modus ponens with 74, 77
79 ((C Ú (P Ú Q)) ® ((P Ú Q) Ú C)) replace proposition variable B by (P Ú Q) in 35
80 ((A Ú (P Ú Q)) ® ((P Ú Q) Ú A)) replace proposition variable C by A in 79
81 ((D ® C) ® (((A Ú ØØ(P Ú Q)) ® D) ® ((A Ú ØØ(P Ú Q)) ® C))) replace proposition variable B by (A Ú ØØ(P Ú Q)) in 41
82 ((D ® ((P Ú Q) Ú A)) ® (((A Ú ØØ(P Ú Q)) ® D) ® ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)))) replace proposition variable C by ((P Ú Q) Ú A) in 81
83 (((A Ú (P Ú Q)) ® ((P Ú Q) Ú A)) ® (((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q))) ® ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)))) replace proposition variable D by (A Ú (P Ú Q)) in 82
84 (((A Ú ØØ(P Ú Q)) ® (A Ú (P Ú Q))) ® ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A))) modus ponens with 80, 83
85 ((A Ú ØØ(P Ú Q)) ® ((P Ú Q) Ú A)) modus ponens with 78, 84
86 ((C Ú A) ® (A Ú C)) replace proposition variable B by A in 35
87 ((ØØ(P Ú Q) Ú A) ® (A Ú ØØ(P Ú Q))) replace proposition variable C by ØØ(P Ú Q) in 86
88 ((D ® C) ® (((ØØ(P Ú Q) Ú A) ® D) ® ((ØØ(P Ú Q) Ú A) ® C))) replace proposition variable B by (ØØ(P Ú Q) Ú A) in 41
89 ((D ® ((P Ú Q) Ú A)) ® (((ØØ(P Ú Q) Ú A) ® D) ® ((Ø