# First theorems of Propositional Calculus

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

Now we could declare the rule Apply Axiom.
parameters:
 p proof line number á link ñ axiom reference

If the proof line n has the form `p ' and an axiom ref matches the form `(p ® q) ' (p, q be formulas), then the string `q ' could be added as a new proof line.
For example: from proof line `(r Ú s) ' we derive `(r Ú s) ' by applying axiom 3.

1. Rule Declaration
Apply Axiom     (rule9)

Analogous to the preceding we declare the rule Apply Sentence.

2. Rule Declaration
Apply Sentence     (rule10)

First we prove a simple implication, that follows directly from the fourth axiom:

3. Proposition
((P
® Q) ® ((A ® P) ® (A ® Q)))     (hilb1)

Proof:
 1 ((P ® Q) ® ((A Ú P) ® (A Ú Q))) add axiom axiom4 2 ((P ® Q) ® ((ØA Ú P) ® (ØA Ú Q))) replace proposition variable A by ØA in 1 3 ((P ® Q) ® ((A ® P) ® (ØA Ú Q))) reverse abbreviation impl in 2 at occurence 1 4 ((P ® Q) ® ((A ® P) ® (A ® Q))) reverse abbreviation impl in 3 at occurence 1 qed

This proposition is the form for the Hypothetical Syllogism.

Now we could declare the rule Hypothetical Syllogism.
parameters:
 p proof line number m proof line number

If the proof line n has the form `(p ® q) '; and the proof line m has the form `(q ® r) ' (p, q and r must be formulas), then the string `(p ® s) ' could be added as a new proof line.

4. Rule Declaration
Hypothetical Syllogism     (rule11)

References, needed for declaration:
hilb1

The self implication could be derived:

5. Proposition
(P
® P)     (hilb2)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 (P ® (P Ú P)) replace proposition variable Q by P in 1 3 ((P Ú P) ® P) add axiom axiom1 4 (P ® P) hypothetical syllogism with 2 and 3 qed

One form of the classical tertium non datur

6. Proposition
(
ØP Ú P)     (hilb3)

Proof:
 1 (P ® P) add proposition hilb2 2 (ØP Ú P) use abbreviation impl in 1 at occurence 1 qed

The standard form of the excluded middle:

7. Proposition
(P
Ú ØP)     (hilb4)

Proof:
 1 (ØP Ú P) add proposition hilb3 2 (P Ú ØP) apply axiom axiom3 in 1 qed

Double negation is implicated:

8. Proposition
(P
® ØØP)     (hilb5)

Proof:
 1 (P Ú ØP) add proposition hilb4 2 (ØP Ú ØØP) replace proposition variable P by ØP in 1 3 (P ® ØØP) reverse abbreviation impl in 2 at occurence 1 qed

The reverse is also true:

9. Proposition
(
ØØP ® P)     (hilb6)

Proof:
 1 (P ® ØØP) add proposition hilb5 2 (ØP ® ØØØP) replace proposition variable P by ØP in 1 3 ((P Ú ØP) ® (P Ú ØØØP)) apply axiom axiom4 in 2 4 (P Ú ØP) add proposition hilb4 5 (P Ú ØØØP) modus ponens with 4, 3 6 (ØØØP Ú P) apply axiom axiom3 in 5 7 (ØØP ® P) reverse abbreviation impl in 6 at occurence 1 qed

The correct reverse of an implication:

10. Proposition
((P
® Q) ® (ØQ ® ØP))     (hilb7)

Proof:
 1 (P ® ØØP) add proposition hilb5 2 (Q ® ØØQ) replace proposition variable P by Q in 1 3 ((ØP Ú Q) ® (ØP Ú ØØQ)) apply axiom axiom4 in 2 4 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 5 ((ØP Ú ØØQ) ® (ØØQ Ú ØP)) substitute variables in 4 6 ((ØP Ú Q) ® (ØØQ Ú ØP)) hypothetical syllogism with 3 and 5 7 ((P ® Q) ® (ØØQ Ú ØP)) reverse abbreviation impl in 6 at occurence 1 8 ((P ® Q) ® (ØQ ® ØP)) reverse abbreviation impl in 7 at occurence 1 qed

11. Rule Declaration
Correct reverse of an implication     (rule12)

References, needed for declaration:
hilb7

12. Rule Declaration
Add a Conjunction on the Left     (rule13)

References, needed for declaration:
axiom4

13. Rule Declaration
Add a Conjunction on the Right     (rule14)

References, needed for declaration:
axiom3 , axiom4

Definition of an Implication 1. part:

14. Proposition
((P
® Q) ® (ØP Ú Q))     (defimpl1)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P ® Q) ® (P ® Q)) substitute variables in 1 3 ((P ® Q) ® (ØP Ú Q)) use abbreviation impl in 2 at occurence 3 qed

Definition of an Implication 2. part:

15. Proposition
((
ØP Ú Q) ® (P ® Q))     (defimpl2)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P ® Q) ® (P ® Q)) substitute variables in 1 3 ((ØP Ú Q) ® (P ® Q)) use abbreviation impl in 2 at occurence 2 qed

16. Rule Declaration
Addition of an Implication on the Right     (rule17)

References, needed for declaration:
defimpl1 , defimpl2

17. Rule Declaration
Addition of an Implication on the Left     (rule18)

References, needed for declaration:
defimpl1 , defimpl2

Definition of a Conjunction 1. part:

18. Proposition
((P
Ù Q) ® Ø(ØP Ú ØQ))     (defand1)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P Ù Q) ® (P Ù Q)) substitute variables in 1 3 ((P Ù Q) ® Ø(ØP Ú ØQ)) use abbreviation and in 2 at occurence 2 qed

Definition of a Conjunction 2. part:

19. Proposition
(
Ø(ØP Ú ØQ) ® (P Ù Q))     (defand2)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P Ù Q) ® (P Ù Q)) substitute variables in 1 3 (Ø(ØP Ú ØQ) ® (P Ù Q)) use abbreviation and in 2 at occurence 1 qed

20. Rule Declaration
Addition of a Conjunction on the Left     (rule19)

References, needed for declaration:
defand1 , defand2

21. Rule Declaration
Addition of a Conjunction on the Right     (rule20)

References, needed for declaration:
defand1 , defand2

Definition of an Equivalence 1. part:

22. Proposition
((P
« Q) ® ((P ® Q) Ù (Q ® P)))     (defequi1)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P « Q) ® (P « Q)) substitute variables in 1 3 ((P « Q) ® ((P ® Q) Ù (Q ® P))) use abbreviation equi in 2 at occurence 2 qed

Definition of an Equivalence 2. part:

23. Proposition
(((P
® Q) Ù (Q ® P)) ® (P « Q))     (defequi2)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P « Q) ® (P « Q)) substitute variables in 1 3 (((P ® Q) Ù (Q ® P)) ® (P « Q)) use abbreviation equi in 2 at occurence 1 qed

24. Rule Declaration
Addition of an Equivalence on the Left     (rule21)

References, needed for declaration:
defequi1 , defequi2

25. Rule Declaration
Addition of an Equivalence on the Right     (rule22)

References, needed for declaration:
defequi1 , defequi2

26. Rule Declaration
Elementary equivalence of two formulas     (rule30)

A simular formulation for the second axiom:

27. Proposition
(P
® (Q Ú P))     (hilb8)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 3 (P ® (Q Ú P)) hypothetical syllogism with 1 and 2 qed

A technical lemma (equal to the third axiom):

28. Proposition
((P
Ú Q) ® (Q Ú P))     (hilb9)

Proof:
 1 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 qed

And another technical lemma (simular to the third axiom):

29. Proposition
((Q
Ú P) ® (P Ú Q))     (hilb10)

Proof:
 1 ((P Ú Q) ® (Q Ú P)) add axiom axiom3 2 ((Q Ú P) ® (P Ú Q)) substitute variables in 1 qed

A technical lemma (equal to the first axiom):

30. Proposition
((P
Ú P) ® P)     (hilb11)

Proof:
 1 ((P Ú P) ® P) add axiom axiom1 qed

A simple propositon that follows directly from the second axiom:

31. Proposition
(P
® (P Ú P))     (hilb12)

Proof:
 1 (P ® (P Ú Q)) add axiom axiom2 2 (P ® (P Ú P)) replace proposition variable Q by P in 1 qed

This is a pre form for the associative law:

32. Proposition
((P
Ú (Q Ú A)) ® (Q Ú (P Ú A)))     (hilb13)

Proof:
 1 (P ® (Q Ú P)) add proposition hilb8 2 (A ® (P Ú A)) substitute variables in 1 3 ((Q Ú A) ® (Q Ú (P Ú A))) apply axiom axiom4 in 2 4 ((P Ú (Q Ú A)) ® (P Ú (Q Ú (P Ú A)))) apply axiom axiom4 in 3 5 ((P Ú (Q Ú A)) ® ((Q Ú (P Ú A)) Ú P)) elementary equivalence in 4 at 3 of hilb9 with hilb10 6 ((P Ú A) ® (Q Ú (P Ú A))) replace proposition variable P by (P Ú A) in 1 7 (P ® (P Ú Q)) add axiom axiom2 8 (P ® (P Ú A)) replace proposition variable Q by A in 7 9 (P ® (Q Ú (P Ú A))) hypothetical syllogism with 8 and 6 10 (((Q Ú (P Ú A)) Ú P) ® ((Q Ú (P Ú A)) Ú (Q Ú (P Ú A)))) apply axiom axiom4 in 9 11 (((Q Ú (P Ú A)) Ú P) ® (Q Ú (P Ú A))) elementary equivalence in 10 at 1 of hilb11 with hilb12 12 ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) hypothetical syllogism with 5 and 11 qed

The associative law for the disjunction (first direction):

33. Proposition
((P
Ú (Q Ú A)) ® ((P Ú Q) Ú A))     (hilb14)

Proof:
 1 (P ® P) add proposition hilb2 2 ((P Ú (Q Ú A)) ® (P Ú (Q Ú A))) substitute variables in 1 3 ((P Ú (Q Ú A)) ® (P Ú (A Ú Q))) elementary equivalence in 2 at 4 of hilb9 with hilb10 4 ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) add proposition hilb13 5 ((P Ú (A Ú Q)) ® (A Ú (P Ú Q))) substitute variables in 4 6 ((P Ú (Q Ú A)) ® (A Ú (P Ú Q))) hypothetical syllogism with 3 and 5 7 ((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) elementary equivalence in 6 at 3 of hilb9 with hilb10 qed

The associative law for the disjunction (second direction):

34. Proposition
(((P
Ú Q) Ú A) ® (P Ú (Q Ú A)))     (hilb15)

Proof:
 1 ((P Ú (Q Ú A)) ® ((P Ú Q) Ú A)) add proposition hilb14 2 ((A Ú (Q Ú P)) ® ((A Ú Q) Ú P)) substitute variables in 1 3 (((Q Ú P) Ú A) ® ((A Ú Q) Ú P)) elementary equivalence in 2 at 1 of hilb9 with hilb10 4 (((P Ú Q) Ú A) ® ((A Ú Q) Ú P)) elementary equivalence in 3 at 2 of hilb9 with hilb10 5 (((P Ú Q) Ú A) ® (P Ú (A Ú Q))) elementary equivalence in 4 at 3 of hilb9 with hilb10 6 (((P Ú Q) Ú A) ® (P Ú (Q Ú A))) elementary equivalence in 5 at 4 of hilb9 with hilb10 qed

Another consequence from hilb13 is the exchange of preconditions:

35. Proposition
((P
® (Q ® A)) ® (Q ® (P ® A)))     (hilb16)

Proof:
 1 ((P Ú (Q Ú A)) ® (Q Ú (P Ú A))) add proposition hilb13 2 ((ØP Ú (ØQ Ú A)) ® (ØQ Ú (ØP Ú A))) substitute variables in 1 3 ((P ® (ØQ Ú A)) ® (ØQ Ú (ØP Ú A))) reverse abbreviation impl in 2 at occurence 1 4 ((P ® (Q ® A)) ® (ØQ Ú (ØP Ú A))) reverse abbreviation impl in 3 at occurence 1 5 ((P ® (Q ® A)) ® (Q ® (ØP Ú A))) reverse abbreviation impl in 4 at occurence 1 6 ((P ® (Q ® A)) ® (Q ® (P ® A))) reverse abbreviation impl in 5 at occurence 1 qed

An analogus form for hyperref [hilb16]hilb16:

36. Proposition
((Q
® (P ® A)) ® (P ® (Q ® A)))     (hilb17)

Proof:
 1 ((P ® (Q ® A)) ® (Q ® (P ® A))) add proposition hilb16 2 ((Q ® (P ® A)) ® (P ® (Q ® A))) substitute variables in 1 qed

## Cross References

This document is used by the following documents: