for questions or link request: module admin

Further Theorems of Propositional Calculus

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

prophilbert1_1.00.00_1.02.00.html

Is used by the following modules:

prophilbert3_1.00.00_1.02.00.html

Negation of a conjunction:

1 Proposition
(Ø(P Ù Q) Þ (ØP Ú ØQ)) (hilb18)

Proof:

1 (ØØP Þ P) add proposition hilb6

2 (ØØ(ØP Ú ØQ) Þ (ØP Ú ØQ)) Subst Line1

3 (Ø(P Ù Q) Þ (ØP Ú ØQ)) reverse abbreviation and in 2 at occurence 1

qed

The reverse of a negation of a conjunction:

2 Proposition
((ØP Ú ØQ) Þ Ø(P Ù Q)) (hilb19)

Proof:

1 (P Þ ØØP) add proposition hilb5

2 ((ØP Ú ØQ) Þ ØØ(ØP Ú ØQ)) Subst Line1

3 ((ØP Ú ØQ) Þ Ø(P Ù Q)) reverse abbreviation and in 2 at occurence 1

qed

Negation of a disjunction:

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

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 8

4 (Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ)) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 11

5 (Ø(P Ú Q) Þ (ØP Ù ØQ)) reverse abbreviation and in 4 at occurence 1

qed

Reverse of a negation of a disjunction:

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

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 4

4 (Ø(ØØP Ú ØØQ) Þ Ø(P Ú Q)) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 7

5 ((ØP Ù ØQ) Þ Ø(P Ú Q)) reverse abbreviation and in 4 at occurence 1

qed

The Conjunction is commutative:

5 Proposition
((P Ù Q) Þ (Q Ù P)) (hilb22)

Proof:

1 (P Þ P) add proposition hilb2

2 ((P Ù Q) Þ (P Ù Q)) Subst Line1

3 ((P Ù Q) Þ Ø(ØP Ú ØQ)) use abbreviation and in 2 at occurence 2

4 ((P Ù Q) Þ Ø(ØQ Ú ØP)) ElementaryEquivalence in 3 with Reference "hilb9" and Reference "hilb10" at 1

5 ((P Ù Q) Þ (Q Ù P)) reverse abbreviation and in 4 at occurence 1

qed

A technical lemma that is simular to the previous one:

6 Proposition
((Q Ù P) Þ (P Ù Q)) (hilb23)

Proof:

1 ((P Ù Q) Þ (Q Ù P)) add proposition hilb22

2 ((Q Ù P) Þ (P Ù Q)) Subst Line1

qed

Reduction of a conjunction:

7 Proposition
((P Ù Q) Þ P) (hilb24)

Proof:

1 (P Þ (P Ú Q)) add axiom axiom2

2 (ØP Þ (ØP Ú ØQ)) Subst Line1

3 (Ø(ØP Ú ØQ) Þ ØØP) Apply Sentence Reference "hilb7" to line 2

4 ((P Ù Q) Þ ØØP) reverse abbreviation and in 3 at occurence 1

5 ((P Ù Q) Þ P) ElementaryEquivalence in 4 with Reference "hilb6" and Reference "hilb5" at 1

qed

Another form of a reduction of a conjunction:

8 Proposition
((P Ù Q) Þ Q) (hilb25)

Proof:

1 ((P Ù Q) Þ P) add proposition hilb24

2 ((Q Ù P) Þ Q) Subst Line1

3 ((P Ù Q) Þ Q) ElementaryEquivalence in 2 with Reference "hilb22" and Reference "hilb23" at 1

qed

The conjunction is associative too (first implication):

9 Proposition
((P Ù (Q Ù A)) Þ ((P Ù Q) Ù A)) (hilb26)

Proof:

1 (((P Ú Q) Ú A) Þ (P Ú (Q Ú A))) add proposition hilb15

2 (Ø(P Ú (Q Ú A)) Þ Ø((P Ú Q) Ú A)) Apply Sentence Reference "hilb7" to line 1

3 (Ø(P Ú ØØ(Q Ú A)) Þ Ø((P Ú Q) Ú A)) ElementaryEquivalence in 2 with Reference "hilb5" and Reference "hilb6" at 5

4 (Ø(P Ú ØØ(Q Ú A)) Þ Ø(ØØ(P Ú Q) Ú A)) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 12

5 (Ø(ØP Ú ØØ(ØQ Ú ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ú ØA)) Subst Line4

6 ((P Ù Ø(ØQ Ú ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ú ØA)) reverse abbreviation and in 5 at occurence 1

7 ((P Ù (Q Ù A)) Þ Ø(ØØ(ØP Ú ØQ) Ú ØA)) reverse abbreviation and in 6 at occurence 1

8 ((P Ù (Q Ù A)) Þ (Ø(ØP Ú ØQ) Ù A)) reverse abbreviation and in 7 at occurence 1

9 ((P Ù (Q Ù A)) Þ ((P Ù Q) Ù A)) reverse abbreviation and in 8 at occurence 1

qed

The conjunction is associative (second implication):

10 Proposition
(((P Ù Q) Ù A) Þ (P Ù (Q Ù A))) (hilb27)

Proof:

1 ((P Ú (Q Ú A)) Þ ((P Ú Q) Ú A)) add proposition hilb14

2 (Ø((P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) Apply Sentence Reference "hilb7" to line 1

3 (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú (Q Ú A))) ElementaryEquivalence in 2 with Reference "hilb5" and Reference "hilb6" at 4

4 (Ø(ØØ(P Ú Q) Ú A) Þ Ø(P Ú ØØ(Q Ú A))) ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 13

5 (Ø(ØØ(ØP Ú ØQ) Ú ØA) Þ Ø(ØP Ú ØØ(ØQ Ú ØA))) Subst Line4

6 ((Ø(ØP Ú ØQ) Ù A) Þ Ø(ØP Ú ØØ(ØQ Ú ØA))) reverse abbreviation and in 5 at occurence 1

7 (((P Ù Q) Ù A) Þ Ø(ØP Ú ØØ(ØQ Ú ØA))) reverse abbreviation and in 6 at occurence 1

8 (((P Ù Q) Ù A) Þ (P Ù Ø(ØQ Ú ØA))) reverse abbreviation and in 7 at occurence 1

9 (((P Ù Q) Ù A) Þ (P Ù (Q Ù A))) reverse abbreviation and in 8 at occurence 1

qed

Form for the conjunction rule:

11 Proposition
(P Þ (Q Þ (P Ù Q))) (hilb28)

Proof:

1 (P Ú ØP) add proposition hilb4

2 ((ØP Ú ØQ) Ú Ø(ØP Ú ØQ)) replace proposition variable P by (ØP Ú ØQ) in 1

3 (ØP Ú (ØQ Ú Ø(ØP Ú ØQ))) Apply Sentence Reference "hilb15" to line 2

4 (P Þ (ØQ Ú Ø(ØP Ú ØQ))) reverse abbreviation impl in 3 at occurence 1

5 (P Þ (Q Þ Ø(ØP Ú ØQ))) reverse abbreviation impl in 4 at occurence 1

6 (P Þ (Q Þ (P Ù Q))) reverse abbreviation and in 5 at occurence 1

qed

Preconditions could be put together in a conjunction (first direction):

12 Proposition
((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) (hilb29)

Proof:

1 (P Þ P) add proposition hilb2

2 ((P Þ (Q Þ A)) Þ (P Þ (Q Þ A))) Subst Line1

3 ((P Þ (Q Þ A)) Þ (ØP Ú (Q Þ A))) use abbreviation impl in 2 at occurence 4

4 ((P Þ (Q Þ A)) Þ (ØP Ú (ØQ Ú A))) use abbreviation impl in 3 at occurence 4

5 ((P Þ (Q Þ A)) Þ ((ØP Ú ØQ) Ú A)) ElementaryEquivalence in 4 with Reference "hilb14" and Reference "hilb15" at 1

6 ((P Þ (Q Þ A)) Þ (ØØ(ØP Ú ØQ) Ú A)) ElementaryEquivalence in 5 with Reference "hilb5" and Reference "hilb6" at 8

7 ((P Þ (Q Þ A)) Þ (Ø(ØP Ú ØQ) Þ A)) reverse abbreviation impl in 6 at occurence 1

8 ((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) reverse abbreviation and in 7 at occurence 1

qed

Preconditions could be put together in a conjunction (second direction):

13 Proposition
(((P Ù Q) Þ A) Þ (P Þ (Q Þ A))) (hilb30)

Proof:

1 (P Þ P) add proposition hilb2

2 ((P Þ (Q Þ A)) Þ (P Þ (Q Þ A))) Subst Line1

3 ((ØP Ú (Q Þ A)) Þ (P Þ (Q Þ A))) use abbreviation impl in 2 at occurence 2

4 ((ØP Ú (ØQ Ú A)) Þ (P Þ (Q Þ A))) use abbreviation impl in 3 at occurence 2

5 (((ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) ElementaryEquivalence in 4 with Reference "hilb14" and Reference "hilb15" at 1

6 ((ØØ(ØP Ú ØQ) Ú A) Þ (P Þ (Q Þ A))) ElementaryEquivalence in 5 with Reference "hilb5" and Reference "hilb6" at 3

7 ((Ø(ØP Ú ØQ) Þ A) Þ (P Þ (Q Þ A))) reverse abbreviation impl in 6 at occurence 1

8 (((P Ù Q) Þ A) Þ (P Þ (Q Þ A))) reverse abbreviation and in 7 at occurence 1

qed

Absorbtion of a conjunction (first direction):

14 Proposition
((P Ù P) Þ P) (hilb31)

Proof:

1 ((P Ù Q) Þ P) add proposition hilb24

2 ((P Ù P) Þ P) replace proposition variable Q by P in 1

qed

Absorbtion of a conjunction (second direction):

15 Proposition
(P Þ (P Ù P)) (hilb32)

Proof:

1 ((P Ú P) Þ P) add proposition hilb11

2 (ØP Þ Ø(P Ú P)) Apply Sentence Reference "hilb7" to line 1

3 (ØØP Þ Ø(ØP Ú ØP)) Subst Line2

4 (P Þ Ø(ØP Ú ØP)) ElementaryEquivalence in 3 with Reference "hilb6" and Reference "hilb5" at 1

5 (P Þ (P Ù P)) reverse abbreviation and in 4 at occurence 1

qed

Absorbtion of identical preconditions (first direction):

16 Proposition
((P Þ (P Þ Q)) Þ (P Þ Q)) (hilb33)

Proof:

1 ((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) add proposition hilb29

2 ((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q)) Subst Line1

3 ((P Þ (P Þ Q)) Þ (P Þ Q)) ElementaryEquivalence in 2 with Reference "hilb31" and Reference "hilb32" at 1

qed

Absorbtion of identical preconditions (second direction):

17 Proposition
((P Þ Q) Þ (P Þ (P Þ Q))) (hilb34)

Proof:

1 (((P Ù Q) Þ A) Þ (P Þ (Q Þ A))) add proposition hilb30

2 (((P Ù P) Þ Q) Þ (P Þ (P Þ Q))) Subst Line1

3 ((P Þ Q) Þ (P Þ (P Þ Q))) ElementaryEquivalence in 2 with Reference "hilb31" and Reference "hilb32" at 1

qed

1	(ØØP Þ P)	add proposition hilb6
2	(ØØ(ØP Ú ØQ) Þ (ØP Ú ØQ))	Subst Line1
3	(Ø(P Ù Q) Þ (ØP Ú ØQ))	reverse abbreviation and in 2 at occurence 1
	qed

1	(P Þ ØØP)	add proposition hilb5
2	((ØP Ú ØQ) Þ ØØ(ØP Ú ØQ))	Subst Line1
3	((ØP Ú ØQ) Þ Ø(P Ù Q))	reverse abbreviation and in 2 at occurence 1
	qed

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 8
4	(Ø(P Ú Q) Þ Ø(ØØP Ú ØØQ))	ElementaryEquivalence in 3 with Reference "hilb5" and Reference "hilb6" at 11
5	(Ø(P Ú Q) Þ (ØP Ù ØQ))	reverse abbreviation and in 4 at occurence 1
	qed

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

1	((P Ù Q) Þ (Q Ù P))	add proposition hilb22
2	((Q Ù P) Þ (P Ù Q))	Subst Line1
	qed

1	(P Þ (P Ú Q))	add axiom axiom2
2	(ØP Þ (ØP Ú ØQ))	Subst Line1
3	(Ø(ØP Ú ØQ) Þ ØØP)	Apply Sentence Reference "hilb7" to line 2
4	((P Ù Q) Þ ØØP)	reverse abbreviation and in 3 at occurence 1
5	((P Ù Q) Þ P)	ElementaryEquivalence in 4 with Reference "hilb6" and Reference "hilb5" at 1
	qed

1	((P Ù Q) Þ P)	add proposition hilb24
2	((Q Ù P) Þ Q)	Subst Line1
3	((P Ù Q) Þ Q)	ElementaryEquivalence in 2 with Reference "hilb22" and Reference "hilb23" at 1
	qed

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

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

1	(P Ú ØP)	add proposition hilb4
2	((ØP Ú ØQ) Ú Ø(ØP Ú ØQ))	replace proposition variable P by (ØP Ú ØQ) in 1
3	(ØP Ú (ØQ Ú Ø(ØP Ú ØQ)))	Apply Sentence Reference "hilb15" to line 2
4	(P Þ (ØQ Ú Ø(ØP Ú ØQ)))	reverse abbreviation impl in 3 at occurence 1
5	(P Þ (Q Þ Ø(ØP Ú ØQ)))	reverse abbreviation impl in 4 at occurence 1
6	(P Þ (Q Þ (P Ù Q)))	reverse abbreviation and in 5 at occurence 1
	qed

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

1	((P Ù Q) Þ P)	add proposition hilb24
2	((P Ù P) Þ P)	replace proposition variable Q by P in 1
	qed

1	((P Ú P) Þ P)	add proposition hilb11
2	(ØP Þ Ø(P Ú P))	Apply Sentence Reference "hilb7" to line 1
3	(ØØP Þ Ø(ØP Ú ØP))	Subst Line2
4	(P Þ Ø(ØP Ú ØP))	ElementaryEquivalence in 3 with Reference "hilb6" and Reference "hilb5" at 1
5	(P Þ (P Ù P))	reverse abbreviation and in 4 at occurence 1
	qed

1	((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A))	add proposition hilb29
2	((P Þ (P Þ Q)) Þ ((P Ù P) Þ Q))	Subst Line1
3	((P Þ (P Þ Q)) Þ (P Þ Q))	ElementaryEquivalence in 2 with Reference "hilb31" and Reference "hilb32" at 1
	qed

1	(((P Ù Q) Þ A) Þ (P Þ (Q Þ A)))	add proposition hilb30
2	(((P Ù P) Þ Q) Þ (P Þ (P Þ Q)))	Subst Line1
3	((P Þ Q) Þ (P Þ (P Þ Q)))	ElementaryEquivalence in 2 with Reference "hilb31" and Reference "hilb32" at 1
	qed