for questions or link request: module admin

First theorems of Propositional Calculus

name: proptheo1, module version: 1.00.00, rule version: 1.00.00, original: proptheo1, author of this module: Michael Meyling

Description

This module includes first proofs of propositional calculus theorems.

This document uses the results of the following documents:

First we prove a well known tautology:

1. Proposition
¬P ∨ P (theo1)

Proof:

1	(P → Q) → ((A ∨ P) → (A ∨ Q))	add axiom axiom4
2	((P ∨ P) → Q) → ((A ∨ (P ∨ P)) → (A ∨ Q))	replace proposition variable P by P ∨ P in 1
3	((P ∨ P) → P) → ((A ∨ (P ∨ P)) → (A ∨ P))	replace proposition variable Q by P in 2
4	((P ∨ P) → P) → ((¬P ∨ (P ∨ P)) → (¬P ∨ P))	replace proposition variable A by ¬P in 3
5	(P ∨ P) → P	add axiom axiom1
6	(¬P ∨ (P ∨ P)) → (¬P ∨ P)	modus ponens with 5, 4
7	(P → (P ∨ P)) → (¬P ∨ P)	reverse abbreviation impl in 6 at occurence 1
8	P → (P ∨ Q)	add axiom axiom2
9	P → (P ∨ P)	replace proposition variable Q by P in 8
10	¬P ∨ P	modus ponens with 9, 7
	qed

We just use our first sentence to get the second theorem:

2. Proposition
P → P (theo2)

Proof:

1	¬P ∨ P	add proposition theo1
2	P → P	reverse abbreviation impl in 1 at occurence 1
	qed

And another use of the first theorem, to get the law of the excluded middle (tertium non datur):

3. Proposition
P ∨ ¬P (theo3)

Proof:

1	¬P ∨ P	add proposition theo1
2	(P ∨ Q) → (Q ∨ P)	add axiom axiom3
3	(¬P ∨ Q) → (Q ∨ ¬P)	replace proposition variable P by ¬P in 2
4	(¬P ∨ P) → (P ∨ ¬P)	replace proposition variable Q by P in 3
5	P ∨ ¬P	modus ponens with 1, 4
	qed

Also trivial is:

4. Proposition
P → ¬¬P (theo4)

Proof:

1	P ∨ ¬P	add proposition theo3
2	¬P ∨ ¬¬P	replace proposition variable P by ¬P in 1
3	P → ¬¬P	reverse abbreviation impl in 2 at occurence 1
	qed

Three negations:

5. Proposition
P ∨ ¬¬¬P (theo5)

Proof:

1	P → ¬¬P	add proposition theo4
2	(P → Q) → ((A ∨ P) → (A ∨ Q))	add axiom axiom4
3	(P → ¬¬P) → ((A ∨ P) → (A ∨ ¬¬P))	replace proposition variable Q by ¬¬P in 2
4	(A ∨ P) → (A ∨ ¬¬P)	modus ponens with 1, 3
5	(A ∨ ¬P) → (A ∨ ¬¬¬P)	replace proposition variable P by ¬P in 4
6	(P ∨ ¬P) → (P ∨ ¬¬¬P)	replace proposition variable A by P in 5
7	P ∨ ¬P	add proposition theo3
8	P ∨ ¬¬¬P	modus ponens with 7, 6
	qed

Now we could prove the reverse of Proposition 4:

6. Proposition
¬¬P → P (theo6)

Proof:

1	P ∨ ¬¬¬P	add proposition theo5
2	(P ∨ Q) → (Q ∨ P)	add axiom axiom3
3	(P ∨ ¬¬¬P) → (¬¬¬P ∨ P)	replace proposition variable Q by ¬¬¬P in 2
4	¬¬¬P ∨ P	modus ponens with 1, 3
5	¬¬P → P	reverse abbreviation impl in 4 at occurence 1
	qed