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 first proofs of propositional 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:
n 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.

This could easily be derived by using the following: 

        n.  (p => q)
        m.  (q => r)
        1'. ((x => y) => ((z => x) => (z => y)))   (AddAxiom/AddSentence)
        2'. ((p => q) => ((r => p) => (r => q)))   (SubstLine 1')
        3'. ((q => r) => ((p => q) => (p => r)))   (SubstLine 1')
        4'. ((p => q) => (p => r))                 (ModusPonens n, 2')
        5'. (p => r)                               (ModusPonens m, 3')

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