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.

References

This document uses the results of the following documents:

Content

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