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:


First we prove a simple implication:

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


The self implication could be derived:

2 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 2 3
qed


One form of the classical "tertium non datur"

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

4 Proposition
      (P Ú ØP)     (hilb4)

Proof:

1 (ØP Ú P) add proposition hilb3
2 (P Ú ØP) Apply Axiom Reference "axiom3" to line 1
qed


Double negation is implicated:

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

6 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 Reference "axiom4" to line 2
4 (P Ú ØP) add proposition hilb4
5 (P Ú ØØØP) modus ponens with 4, 3
6 (ØØØP Ú P) Apply Axiom Reference "axiom3" to line 5
7 (ØØP Þ P) reverse abbreviation impl in 6 at occurence 1
qed


The correct reverse of an implication:

7 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 Reference "axiom4" to line 2
4 ((P Ú Q) Þ (Q Ú P)) add axiom axiom3
5 ((ØP Ú ØØQ) Þ (ØØQ Ú ØP)) Subst Line4
6 ((ØP Ú Q) Þ (ØØQ Ú ØP)) Hypothetical Syllogism 3 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


A simular formulation for the second axiom:

8 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 1 2
qed


A technical lemma (equal to the third axiom):

9 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):

10 Proposition
      ((Q Ú P) Þ (P Ú Q))     (hilb10)

Proof:

1 ((P Ú Q) Þ (Q Ú P)) add axiom axiom3
2 ((Q Ú P) Þ (P Ú Q)) Subst Line1
qed


A technical lemma (equal to the first axiom):

11 Proposition
      ((P Ú P) Þ P)     (hilb11)

Proof:

1 ((P Ú P) Þ P) add axiom axiom1
qed


A simple propositon that follows directly from the second axiom:

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

13 Proposition
      ((P Ú (Q Ú A)) Þ (Q Ú (P Ú A)))     (hilb13)

Proof:

1 (P Þ (Q Ú P)) add proposition hilb8
2 (A Þ (P Ú A)) Subst Line1
3 ((Q Ú A) Þ (Q Ú (P Ú A))) Apply Axiom Reference "axiom4" to line 2
4 ((P Ú (Q Ú A)) Þ (P Ú (Q Ú (P Ú A)))) Apply Axiom Reference "axiom4" to line 3
5 ((P Ú (Q Ú A)) Þ ((Q Ú (P Ú A)) Ú P)) ElementaryEquivalence in 4 with Reference "hilb9" and Reference "hilb10" at 3
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 8 6
10 (((Q Ú (P Ú A)) Ú P) Þ ((Q Ú (P Ú A)) Ú (Q Ú (P Ú A)))) Apply Axiom Reference "axiom4" to line 9
11 (((Q Ú (P Ú A)) Ú P) Þ (Q Ú (P Ú A))) ElementaryEquivalence in 10 with Reference "hilb11" and Reference "hilb12" at 1
12 ((P Ú (Q Ú A)) Þ (Q Ú (P Ú A))) Hypothetical Syllogism 5 11
qed


The associative law for the disjunction (first direction):

14 Proposition
      ((P Ú (Q Ú A)) Þ ((P Ú Q) Ú A))     (hilb14)

Proof:

1 (P Þ P) add proposition hilb2
2 ((P Ú (Q Ú A)) Þ (P Ú (Q Ú A))) Subst Line1
3 ((P Ú (Q Ú A)) Þ (P Ú (A Ú Q))) ElementaryEquivalence in 2 with Reference "hilb9" and Reference "hilb10" at 4
4 ((P Ú (Q Ú A)) Þ (Q Ú (P Ú A))) add proposition hilb13
5 ((P Ú (A Ú Q)) Þ (A Ú (P Ú Q))) Subst Line4
6 ((P Ú (Q Ú A)) Þ (A Ú (P Ú Q))) Hypothetical Syllogism 3 5
7 ((P Ú (Q Ú A)) Þ ((P Ú Q) Ú A)) ElementaryEquivalence in 6 with Reference "hilb9" and Reference "hilb10" at 3
qed


The associative law for the disjunction (second direction):

15 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)) Subst Line1
3 (((Q Ú P) Ú A) Þ ((A Ú Q) Ú P)) ElementaryEquivalence in 2 with Reference "hilb9" and Reference "hilb10" at 1
4 (((P Ú Q) Ú A) Þ ((A Ú Q) Ú P)) ElementaryEquivalence in 3 with Reference "hilb9" and Reference "hilb10" at 2
5 (((P Ú Q) Ú A) Þ (P Ú (A Ú Q))) ElementaryEquivalence in 4 with Reference "hilb9" and Reference "hilb10" at 3
6 (((P Ú Q) Ú A) Þ (P Ú (Q Ú A))) ElementaryEquivalence in 5 with Reference "hilb9" and Reference "hilb10" at 4
qed


Another consequence from hilb13 is the exchange of preconditions:

16 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))) Subst Line1
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:

17 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))) Subst Line1
qed