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: