for questions or link request: module admin

First theorems of Propositional Calculus

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

Description

This module includes first proofs of propositional calculus theorems.

Uses the following modules:

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