# Further Theorems of Propositional Calculus

name: prophilbert2, module version: 1.00.00, rule version: 1.02.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 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

## Cross References

This document is used by the following documents: