for questions or link request: module admin

First theorems of Propositional Calculus

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

Uses the following modules:

Is used by the following modules:


1. Rule Declaration
      Apply Axiom     (rule9)


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

This module is used by the following modules: