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