for questions or link request: module admin

First theorems of Propositional Calculus

name: luktheo1, module version: 1.00.00, rule version: 1.00.00, original: luktheo1, authors of this module: Franz Fritsche, 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 theorem known as identity:

1. Proposition
      (P ® P)     (theorem1)

Proof:
1 (P ® (Q ® P)) add axiom axiom1
2 (P ® ((P ® P) ® P)) replace proposition variable Q by (P ® P) in 1
3 ((P ® (Q ® A)) ® ((P ® Q) ® (P ® A))) add axiom axiom2
4 ((P ® ((P ® P) ® A)) ® ((P ® (P ® P)) ® (P ® A))) replace proposition variable Q by (P ® P) in 3
5 ((P ® ((P ® P) ® P)) ® ((P ® (P ® P)) ® (P ® P))) replace proposition variable A by P in 4
6 ((P ® (P ® P)) ® (P ® P)) modus ponens with 2, 5
7 (P ® (P ® P)) replace proposition variable Q by P in 1
8 (P ® P) modus ponens with 7, 6
qed

Now we prove a theorem known as (one form of) hypothetical syllogism:

2. Proposition
      ((Q ® A) ® ((P ® Q) ® (P ® A)))     (theorem2)

Proof:
1 (P ® (Q ® P)) add axiom axiom1
2 (P ® ((Q ® A) ® P)) replace proposition variable Q by (Q ® A) in 1
3 (((P ® (Q ® A)) ® ((P ® Q) ® (P ® A))) ® ((Q ® A) ® ((P ® (Q ® A)) ® ((P ® Q) ® (P ® A))))) replace proposition variable P by ((P ® (Q ® A)) ® ((P ® Q) ® (P ® A))) in 2
4 ((P ® (Q ® A)) ® ((P ® Q) ® (P ® A))) add axiom axiom2
5 ((Q ® A) ® ((P ® (Q ® A)) ® ((P ® Q) ® (P ® A)))) modus ponens with 4, 3
6 ((B ® (Q ® A)) ® ((B ® Q) ® (B ® A))) replace proposition variable P by B in 4
7 ((B ® (C ® A)) ® ((B ® C) ® (B ® A))) replace proposition variable Q by C in 6
8 ((B ® (C ® D)) ® ((B ® C) ® (B ® D))) replace proposition variable A by D in 7
9 (((Q ® A) ® (C ® D)) ® (((Q ® A) ® C) ® ((Q ® A) ® D))) replace proposition variable B by (Q ® A) in 8
10 (((Q ® A) ® ((P ® (Q ® A)) ® D)) ® (((Q ® A) ® (P ® (Q ® A))) ® ((Q ® A) ® D))) replace proposition variable C by (P ® (Q ® A)) in 9
11 (((Q ® A) ® ((P ® (Q ® A)) ® ((P ® Q) ® (P ® A)))) ® (((Q ® A) ® (P ® (Q ® A))) ® ((Q ® A) ® ((P ® Q) ® (P ® A))))) replace proposition variable D by ((P ® Q) ® (P ® A)) in 10
12 (((Q ® A) ® (P ® (Q ® A))) ® ((Q ® A) ® ((P ® Q) ® (P ® A)))) modus ponens with 5, 11
13 (P ® (B ® P)) replace proposition variable Q by B in 1
14 ((Q ® A) ® (B ® (Q ® A))) replace proposition variable P by (Q ® A) in 13
15 ((Q ® A) ® (P ® (Q ® A))) replace proposition variable B by P in 14
16 ((Q ® A) ® ((P ® Q) ® (P ® A))) modus ponens with 15, 12
qed