# Further Theorems of Propositional Calculus

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

## References

This document uses the results of the following documents:

## Content

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

## Cross References

This document is used by the following documents: