for questions or link request: module admin

Further Theorems of Propositional Calculus

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


First distributive law (first direction):

1 Proposition
      ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))     (hilb36)

Proof:

1 ((P Ù Q) Þ P) add proposition hilb24
2 ((Q Ù A) Þ Q) Subst Line1
3 ((P Ú (Q Ù A)) Þ (P Ú Q)) Apply Axiom Reference "axiom4" to line 2
4 ((P Ù Q) Þ Q) add proposition hilb25
5 ((Q Ù A) Þ A) Subst Line4
6 ((P Ú (Q Ù A)) Þ (P Ú A)) Apply Axiom Reference "axiom4" to line 5
7 (P Þ (Q Þ (P Ù Q))) add proposition hilb28
8 ((P Ú Q) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Subst Line7
9 ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Hypothetical Syllogism 3 8
10 ((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Apply Sentence Reference "hilb16" to line 9
11 ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Hypothetical Syllogism 6 10
12 ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) Apply Sentence Reference "hilb33" to line 11
qed


First distributive law (second direction):

2 Proposition
      (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A)))     (hilb37)

Proof:

1 (P Þ (Q Þ (P Ù Q))) add proposition hilb28
2 (Q Þ (A Þ (Q Ù A))) Subst Line1
3 ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) add axiom axiom4
4 ((A Þ (Q Ù A)) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Subst Line3
5 (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Hypothetical Syllogism 2 4
6 ((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) Apply Sentence Reference "hilb16" to line 5
7 ((Q Þ (P Ú (Q Ù A))) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) Subst Line3
8 ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) Hypothetical Syllogism 6 7
9 ((P Ú A) Þ ((P Ú Q) Þ ((P Ú P) Ú (Q Ù A)))) ElementaryEquivalence in 8 with Reference "hilb14" and Reference "hilb15" at 1
10 ((P Ú A) Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) ElementaryEquivalence in 9 with Reference "hilb11" and Reference "hilb12" at 1
11 ((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Apply Sentence Reference "hilb16" to line 10
12 (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) Apply Sentence Reference "hilb29" to line 11
qed


A form for the abbreviation rule form for disjunction (first direction):

3 Proposition
      ((P Ú Q) Þ Ø(ØP Ù ØQ))     (hilb38)

Proof:

1 (P Þ P) add proposition hilb2
2 ((P Ú Q) Þ (P Ú Q)) Subst Line1
3 ((P Ú Q) Þ ØØ(P Ú Q)) ElementaryEquivalence in 2 with Reference "hilb5" and Reference "hilb6" at 5
4 ((P Ú Q) Þ ØØ(ØØP Ú Q)) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 8
5 ((P Ú Q) Þ ØØ(ØØP Ú ØØQ)) ElementaryEquivalence in 4 with Reference "hilb5" and Reference "hilb6" at 11
6 ((P Ú Q) Þ Ø(ØP Ù ØQ)) reverse abbreviation and in 5 at occurence 1
qed


A form for the abbreviation rule form for disjunction (second direction):

4 Proposition
      (Ø(ØP Ù ØQ) Þ (P Ú Q))     (hilb39)

Proof:

1 (P Þ P) add proposition hilb2
2 ((P Ú Q) Þ (P Ú Q)) Subst Line1
3 (ØØ(P Ú Q) Þ (P Ú Q)) ElementaryEquivalence in 2 with Reference "hilb5" and Reference "hilb6" at 2
4 (ØØ(ØØP Ú Q) Þ (P Ú Q)) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 5
5 (ØØ(ØØP Ú ØØQ) Þ (P Ú Q)) ElementaryEquivalence in 4 with Reference "hilb5" and Reference "hilb6" at 8
6 (Ø(ØP Ù ØQ) Þ (P Ú Q)) reverse abbreviation and in 5 at occurence 1
qed


By duality we get the second distributive law (first direction):

5 Proposition
      ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú (P Ù A)))     (hilb40)

Proof:

1 (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) add proposition hilb37
2 (Ø(P Ú (Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A))) Apply Sentence Reference "hilb7" to line 1
3 (Ø(P Ú ØØ(Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A))) ElementaryEquivalence in 2 with Reference "hilb5" and Reference "hilb6" at 5
4 (Ø(P Ú ØØ(Q Ù A)) Þ Ø(ØØ(P Ú Q) Ù (P Ú A))) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 12
5 (Ø(P Ú ØØ(Q Ù A)) Þ Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) ElementaryEquivalence in 4 with Reference "hilb5" and Reference "hilb6" at 17
6 (Ø(ØP Ú ØØ(ØQ Ù ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) Subst Line5
7 ((P Ù Ø(ØQ Ù ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) reverse abbreviation and in 6 at occurence 1
8 ((P Ù (Q Ú A)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) ElementaryEquivalence in 7 with Reference "hilb39" and Reference "hilb38" at 1
9 ((P Ù (Q Ú A)) Þ (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) ElementaryEquivalence in 8 with Reference "hilb39" and Reference "hilb38" at 1
10 ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú Ø(ØP Ú ØA))) reverse abbreviation and in 9 at occurence 1
11 ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú (P Ù A))) reverse abbreviation and in 10 at occurence 1
qed


The second distributive law (second direction):

6 Proposition
      (((P Ù Q) Ú (P Ù A)) Þ (P Ù (Q Ú A)))     (hilb41)

Proof:

1 ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) add proposition hilb36
2 (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú (Q Ù A))) Apply Sentence Reference "hilb7" to line 1
3 (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) ElementaryEquivalence in 2 with Reference "hilb5" and Reference "hilb6" at 13
4 (Ø(ØØ(P Ú Q) Ù (P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 4
5 (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) ElementaryEquivalence in 4 with Reference "hilb5" and Reference "hilb6" at 9
6 (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) Subst Line5
7 (Ø(Ø(P Ù Q) Ù ØØ(ØP Ú ØA)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) reverse abbreviation and in 6 at occurence 1
8 (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) reverse abbreviation and in 7 at occurence 1
9 (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) Þ (P Ù Ø(ØQ Ù ØA))) reverse abbreviation and in 8 at occurence 1
10 (((P Ù Q) Ú (P Ù A)) Þ (P Ù Ø(ØQ Ù ØA))) ElementaryEquivalence in 9 with Reference "hilb39" and Reference "hilb38" at 1
11 (((P Ù Q) Ú (P Ù A)) Þ (P Ù (Q Ú A))) ElementaryEquivalence in 10 with Reference "hilb39" and Reference "hilb38" at 1
qed