# 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: