for questions or link request: module admin

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: