for questions or link request: module admin

Further Theorems of Propositional Calculus

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


First distributive law (first direction):

1. Proposition
      ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))     (hilb36)

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 ((Q Ù A) Þ Q) replace proposition variable B by Q in 3
5 ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) add axiom axiom4
6 ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) replace proposition variable A by B in 5
7 ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) replace proposition variable Q by C in 6
8 ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) replace proposition variable P by D in 7
9 ((D Þ C) Þ ((P Ú D) Þ (P Ú C))) replace proposition variable B by P in 8
10 ((D Þ Q) Þ ((P Ú D) Þ (P Ú Q))) replace proposition variable C by Q in 9
11 (((Q Ù A) Þ Q) Þ ((P Ú (Q Ù A)) Þ (P Ú Q))) replace proposition variable D by (Q Ù A) in 10
12 ((P Ú (Q Ù A)) Þ (P Ú Q)) modus ponens with 4, 11
13 ((P Ù Q) Þ Q) add proposition hilb25
14 ((P Ù A) Þ A) replace proposition variable Q by A in 13
15 ((B Ù A) Þ A) replace proposition variable P by B in 14
16 ((Q Ù A) Þ A) replace proposition variable B by Q in 15
17 ((D Þ A) Þ ((P Ú D) Þ (P Ú A))) replace proposition variable C by A in 9
18 (((Q Ù A) Þ A) Þ ((P Ú (Q Ù A)) Þ (P Ú A))) replace proposition variable D by (Q Ù A) in 17
19 ((P Ú (Q Ù A)) Þ (P Ú A)) modus ponens with 16, 18
20 (P Þ (Q Þ (P Ù Q))) add proposition hilb28
21 (P Þ (A Þ (P Ù A))) replace proposition variable Q by A in 20
22 (B Þ (A Þ (B Ù A))) replace proposition variable P by B in 21
23 (B Þ ((P Ú A) Þ (B Ù (P Ú A)))) replace proposition variable A by (P Ú A) in 22
24 ((P Ú Q) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) replace proposition variable B by (P Ú Q) in 23
25 ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) add proposition hilb1
26 ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) replace proposition variable A by B in 25
27 ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) replace proposition variable Q by C in 26
28 ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) replace proposition variable P by D in 27
29 ((D Þ C) Þ (((P Ú (Q Ù A)) Þ D) Þ ((P Ú (Q Ù A)) Þ C))) replace proposition variable B by (P Ú (Q Ù A)) in 28
30 ((D Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ D) Þ ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))))) replace proposition variable C by ((P Ú A) Þ ((P Ú Q) Ù (P Ú A))) in 29
31 (((P Ú Q) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ (P Ú Q)) Þ ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (P Ú Q) in 30
32 (((P Ú (Q Ù A)) Þ (P Ú Q)) Þ ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A))))) modus ponens with 24, 31
33 ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) modus ponens with 12, 32
34 ((P Þ (Q Þ A)) Þ (Q Þ (P Þ A))) add proposition hilb16
35 ((P Þ (Q Þ B)) Þ (Q Þ (P Þ B))) replace proposition variable A by B in 34
36 ((P Þ (C Þ B)) Þ (C Þ (P Þ B))) replace proposition variable Q by C in 35
37 ((D Þ (C Þ B)) Þ (C Þ (D Þ B))) replace proposition variable P by D in 36
38 ((D Þ (C Þ ((P Ú Q) Ù (P Ú A)))) Þ (C Þ (D Þ ((P Ú Q) Ù (P Ú A))))) replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 37
39 ((D Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ ((P Ú A) Þ (D Þ ((P Ú Q) Ù (P Ú A))))) replace proposition variable C by (P Ú A) in 38
40 (((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ ((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))))) replace proposition variable D by (P Ú (Q Ù A)) in 39
41 ((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) modus ponens with 33, 40
42 ((D Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ D) Þ ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))))) replace proposition variable C by ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) in 29
43 (((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ (P Ú A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))))) replace proposition variable D by (P Ú A) in 42
44 (((P Ú (Q Ù A)) Þ (P Ú A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))))) modus ponens with 41, 43
45 ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) modus ponens with 19, 44
46 ((P Þ (P Þ Q)) Þ (P Þ Q)) add proposition hilb33
47 ((P Þ (P Þ A)) Þ (P Þ A)) replace proposition variable Q by A in 46
48 ((B Þ (B Þ A)) Þ (B Þ A)) replace proposition variable P by B in 47
49 ((B Þ (B Þ ((P Ú Q) Ù (P Ú A)))) Þ (B Þ ((P Ú Q) Ù (P Ú A)))) replace proposition variable A by ((P Ú Q) Ù (P Ú A)) in 48
50 (((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) replace proposition variable B by (P Ú (Q Ù A)) in 49
51 ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) modus ponens with 45, 50
qed

First distributive law (second direction):

2. Proposition
      (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A)))     (hilb37)

Proof:
1 (P Þ (Q Þ (P Ù Q))) add proposition hilb28
2 (P Þ (A Þ (P Ù A))) replace proposition variable Q by A in 1
3 (B Þ (A Þ (B Ù A))) replace proposition variable P by B in 2
4 (Q Þ (A Þ (Q Ù A))) replace proposition variable B by Q in 3
5 ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) add axiom axiom4
6 ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) replace proposition variable A by B in 5
7 ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) replace proposition variable Q by C in 6
8 ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) replace proposition variable P by D in 7
9 ((D Þ C) Þ ((P Ú D) Þ (P Ú C))) replace proposition variable B by P in 8
10 ((D Þ (Q Ù A)) Þ ((P Ú D) Þ (P Ú (Q Ù A)))) replace proposition variable C by (Q Ù A) in 9
11 ((A Þ (Q Ù A)) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) replace proposition variable D by A in 10
12 ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) add proposition hilb1
13 ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) replace proposition variable A by B in 12
14 ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) replace proposition variable Q by C in 13
15 ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) replace proposition variable P by D in 14
16 ((D Þ C) Þ ((Q Þ D) Þ (Q Þ C))) replace proposition variable B by Q in 15
17 ((D Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((Q Þ D) Þ (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))))) replace proposition variable C by ((P Ú A) Þ (P Ú (Q Ù A))) in 16
18 (((A Þ (Q Ù A)) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((Q Þ (A Þ (Q Ù A))) Þ (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))))) replace proposition variable D by (A Þ (Q Ù A)) in 17
19 ((Q Þ (A Þ (Q Ù A))) Þ (Q Þ ((P Ú A) Þ (P Ú (Q Ù A))))) modus ponens with 11, 18
20 (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))) modus ponens with 4, 19
21 ((P Þ (Q Þ A)) Þ (Q Þ (P Þ A))) add proposition hilb16
22 ((P Þ (Q Þ B)) Þ (Q Þ (P Þ B))) replace proposition variable A by B in 21
23 ((P Þ (C Þ B)) Þ (C Þ (P Þ B))) replace proposition variable Q by C in 22
24 ((D Þ (C Þ B)) Þ (C Þ (D Þ B))) replace proposition variable P by D in 23
25 ((D Þ (C Þ (P Ú (Q Ù A)))) Þ (C Þ (D Þ (P Ú (Q Ù A))))) replace proposition variable B by (P Ú (Q Ù A)) in 24
26 ((D Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ (D Þ (P Ú (Q Ù A))))) replace proposition variable C by (P Ú A) in 25
27 ((Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ (Q Þ (P Ú (Q Ù A))))) replace proposition variable D by Q in 26
28 ((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) modus ponens with 20, 27
29 ((D Þ (P Ú (Q Ù A))) Þ ((P Ú D) Þ (P Ú (P Ú (Q Ù A))))) replace proposition variable C by (P Ú (Q Ù A)) in 9
30 ((Q Þ (P Ú (Q Ù A))) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) replace proposition variable D by Q in 29
31 ((D Þ C) Þ (((P Ú A) Þ D) Þ ((P Ú A) Þ C))) replace proposition variable B by (P Ú A) in 15
32 ((D Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) Þ (((P Ú A) Þ D) Þ ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))))) replace proposition variable C by ((P Ú Q) Þ (P Ú (P Ú (Q Ù A)))) in 31
33 (((Q Þ (P Ú (Q Ù A))) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) Þ (((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))))) replace proposition variable D by (Q Þ (P Ú (Q Ù A))) in 32
34 (((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A)))))) modus ponens with 30, 33
35 ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) modus ponens with 28, 34
36 ((P Ú A) Þ ((P Ú Q) Þ ((P Ú P) Ú (Q Ù A)))) elementary equivalence in 35 at 1 of hilb14 with hilb15
37 ((P Ú A) Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) elementary equivalence in 36 at 1 of hilb11 with hilb12
38 ((D Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) Þ ((P Ú Q) Þ (D Þ (P Ú (Q Ù A))))) replace proposition variable C by (P Ú Q) in 25
39 (((P Ú A) Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) Þ ((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A))))) replace proposition variable D by (P Ú A) in 38
40 ((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) modus ponens with 37, 39
41 ((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) add proposition hilb29
42 ((P Þ (Q Þ B)) Þ ((P Ù Q) Þ B)) replace proposition variable A by B in 41
43 ((P Þ (C Þ B)) Þ ((P Ù C) Þ B)) replace proposition variable Q by C in 42
44 ((D Þ (C Þ B)) Þ ((D Ù C) Þ B)) replace proposition variable P by D in 43
45 ((D Þ (C Þ (P Ú (Q Ù A)))) Þ ((D Ù C) Þ (P Ú (Q Ù A)))) replace proposition variable B by (P Ú (Q Ù A)) in 44
46 ((D Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((D Ù (P Ú A)) Þ (P Ú (Q Ù A)))) replace proposition variable C by (P Ú A) in 45
47 (((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A)))) replace proposition variable D by (P Ú Q) in 46
48 (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) modus ponens with 40, 47
qed

A form for the abbreviation rule form for disjunction (first direction):

3. Proposition
      ((P Ú Q) Þ Ø(ØP Ù ØQ))     (hilb38)

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 5 of hilb5 with hilb6
5 ((P Ú Q) Þ ØØ(ØØP Ú Q)) elementary equivalence in 4 at 8 of hilb5 with hilb6
6 ((P Ú Q) Þ ØØ(ØØP Ú ØØQ)) elementary equivalence in 5 at 11 of hilb5 with hilb6
7 ((P Ú Q) Þ Ø(ØP Ù ØQ)) reverse abbreviation and in 6 at occurence 1
qed

A form for the abbreviation rule form for disjunction (second direction):

4. Proposition
      (Ø(ØP Ù ØQ) Þ (P Ú Q))     (hilb39)

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 2 of hilb5 with hilb6
5 (ØØ(ØØP Ú Q) Þ (P Ú Q)) elementary equivalence in 4 at 5 of hilb5 with hilb6
6 (ØØ(ØØP Ú ØØQ) Þ (P Ú Q)) elementary equivalence in 5 at 8 of hilb5 with hilb6
7 (Ø(ØP Ù ØQ) Þ (P Ú Q)) reverse abbreviation and in 6 at occurence 1
qed

By duality we get the second distributive law (first direction):

5. Proposition
      ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú (P Ù A)))     (hilb40)

Proof:
1 (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) add proposition hilb37
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) Ù (P Ú A)) Þ (P Ú (Q Ù A))) Þ (Ø(P Ú (Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A)))) replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 5
7 (Ø(P Ú (Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A))) modus ponens with 1, 6
8 (Ø(P Ú ØØ(Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A))) elementary equivalence in 7 at 5 of hilb5 with hilb6
9 (Ø(P Ú ØØ(Q Ù A)) Þ Ø(ØØ(P Ú Q) Ù (P Ú A))) elementary equivalence in 8 at 12 of hilb5 with hilb6
10 (Ø(P Ú ØØ(Q Ù A)) Þ Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) elementary equivalence in 9 at 17 of hilb5 with hilb6
11 (Ø(P Ú ØØ(Q Ù B)) Þ Ø(ØØ(P Ú Q) Ù ØØ(P Ú B))) replace proposition variable A by B in 10
12 (Ø(P Ú ØØ(C Ù B)) Þ Ø(ØØ(P Ú C) Ù ØØ(P Ú B))) replace proposition variable Q by C in 11
13 (Ø(D Ú ØØ(C Ù B)) Þ Ø(ØØ(D Ú C) Ù ØØ(D Ú B))) replace proposition variable P by D in 12
14 (Ø(D Ú ØØ(C Ù ØA)) Þ Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA))) replace proposition variable B by ØA in 13
15 (Ø(D Ú ØØ(ØQ Ù ØA)) Þ Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA))) replace proposition variable C by ØQ in 14
16 (Ø(ØP Ú ØØ(ØQ Ù ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) replace proposition variable D by ØP in 15
17 ((P Ù Ø(ØQ Ù ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) reverse abbreviation and in 16 at occurence 1
18 ((P Ù (Q Ú A)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) elementary equivalence in 17 at 1 of hilb39 with hilb38
19 ((P Ù (Q Ú A)) Þ (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) elementary equivalence in 18 at 1 of hilb39 with hilb38
20 ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú Ø(ØP Ú ØA))) reverse abbreviation and in 19 at occurence 1
21 ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú (P Ù A))) reverse abbreviation and in 20 at occurence 1
qed

The second distributive law (second direction):

6. Proposition
      (((P Ù Q) Ú (P Ù A)) Þ (P Ù (Q Ú A)))     (hilb41)

Proof:
1 ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) add proposition hilb36
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) Ù (P Ú A))) Þ (Ø((P Ú Q) Ù (P Ú A)) Þ ØB)) replace proposition variable A by ((P Ú Q) Ù (P Ú A)) in 4
6 (((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) Þ (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú (Q Ù A)))) replace proposition variable B by (P Ú (Q Ù A)) in 5
7 (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú (Q Ù A))) modus ponens with 1, 6
8 (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) elementary equivalence in 7 at 13 of hilb5 with hilb6
9 (Ø(ØØ(P Ú Q) Ù (P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) elementary equivalence in 8 at 4 of hilb5 with hilb6
10 (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) elementary equivalence in 9 at 9 of hilb5 with hilb6
11 (Ø(ØØ(P Ú Q) Ù ØØ(P Ú B)) Þ Ø(P Ú ØØ(Q Ù B))) replace proposition variable A by B in 10
12 (Ø(ØØ(P Ú C) Ù ØØ(P Ú B)) Þ Ø(P Ú ØØ(C Ù B))) replace proposition variable Q by C in 11
13 (Ø(ØØ(D Ú C) Ù ØØ(D Ú B)) Þ Ø(D Ú ØØ(C Ù B))) replace proposition variable P by D in 12
14 (Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA)) Þ Ø(D Ú ØØ(C Ù ØA))) replace proposition variable B by ØA in 13
15 (Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA)) Þ Ø(D Ú ØØ(ØQ Ù ØA))) replace proposition variable C by ØQ in 14
16 (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) replace proposition variable D by ØP in 15
17 (Ø(Ø(P Ù Q) Ù ØØ(ØP Ú ØA)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) reverse abbreviation and in 16 at occurence 1
18 (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) reverse abbreviation and in 17 at occurence 1
19 (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) Þ (P Ù Ø(ØQ Ù ØA))) reverse abbreviation and in 18 at occurence 1
20 (((P Ù Q) Ú (P Ù A)) Þ (P Ù Ø(ØQ Ù ØA))) elementary equivalence in 19 at 1 of hilb39 with hilb38
21 (((P Ù Q) Ú (P Ù A)) Þ (P Ù (Q Ú A))) elementary equivalence in 20 at 1 of hilb39 with hilb38
qed

This module is used by the following modules: