The Axioms of the Whitehead Russell Calculus

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

Description

This module notates the original axioms of the Whitehead-Russell calculus, the so called `primitive propositions'. These five primitive propositions could be deduced by our four axioms.

References

This document uses the results of the following documents:

Content

At first we show a little proposition to demonstrate the basic proof methods of propositional calculus:

1. Proposition
P → (Q ∨ P)     (lem1)

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

This is the first primitive proposition, its equal to our first axiom:

2. Proposition
(P ∨ P) → P     (prin1)

Proof:
 1 (P ∨ P) → P add axiom axiom1 qed

Now comes the second primitive proposition. It looks simular to our second axiom, but we have to use our first proposition to prove it:

3. Proposition
Q → (P ∨ Q)     (prin2)

Proof:
 1 P → (Q ∨ P) add proposition lem1 2 P → (A ∨ P) replace proposition variable Q by A in 1 3 Q → (A ∨ Q) replace proposition variable P by Q in 2 4 Q → (P ∨ Q) replace proposition variable A by P in 3 qed

The third primitive proposition:

4. Proposition
(P ∨ Q) → (Q ∨ P)     (prin3)

Proof:
 1 (P ∨ Q) → (Q ∨ P) add axiom axiom3 qed

The fourth primitive proposition was proved with the other primitve propositions by P. Bernays. Here comes the sledgehammer:

5. Proposition
(P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A))     (prin4)

Proof:
 1 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4 2 (P7 → Q) → ((A ∨ P7) → (A ∨ Q)) replace proposition variable P by P7 in 1 3 (P7 → P8) → ((A ∨ P7) → (A ∨ P8)) replace proposition variable Q by P8 in 2 4 (P7 → P8) → ((P9 ∨ P7) → (P9 ∨ P8)) replace proposition variable A by P9 in 3 5 P → (Q ∨ P) add proposition lem1 6 (P → (Q ∨ P)) → ((A ∨ P) → (A ∨ (Q ∨ P))) replace proposition variable Q by Q ∨ P in 1 7 (A ∨ P) → (A ∨ (Q ∨ P)) modus ponens with 5, 6 8 ((A ∨ P) → P8) → ((P9 ∨ (A ∨ P)) → (P9 ∨ P8)) replace proposition variable P7 by A ∨ P in 4 9 ((A ∨ P) → (A ∨ (Q ∨ P))) → ((P9 ∨ (A ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P)))) replace proposition variable P8 by A ∨ (Q ∨ P) in 8 10 (P9 ∨ (A ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P))) modus ponens with 7, 9 11 (Q ∨ (A ∨ P)) → (Q ∨ (A ∨ (Q ∨ P))) replace proposition variable P9 by Q in 10 12 (P ∨ Q) → (Q ∨ P) add axiom axiom3 13 (D ∨ Q) → (Q ∨ D) replace proposition variable P by D in 12 14 (D ∨ (A ∨ (Q ∨ P))) → ((A ∨ (Q ∨ P)) ∨ D) replace proposition variable Q by A ∨ (Q ∨ P) in 13 15 (Q ∨ (A ∨ (Q ∨ P))) → ((A ∨ (Q ∨ P)) ∨ Q) replace proposition variable D by Q in 14 16 ((Q ∨ (A ∨ (Q ∨ P))) → P8) → ((P9 ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ P8)) replace proposition variable P7 by Q ∨ (A ∨ (Q ∨ P)) in 4 17 ((Q ∨ (A ∨ (Q ∨ P))) → ((A ∨ (Q ∨ P)) ∨ Q)) → ((P9 ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q))) replace proposition variable P8 by (A ∨ (Q ∨ P)) ∨ Q in 16 18 (P9 ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) modus ponens with 15, 17 19 (¬(Q ∨ (A ∨ P)) ∨ (Q ∨ (A ∨ (Q ∨ P)))) → (¬(Q ∨ (A ∨ P)) ∨ ((A ∨ (Q ∨ P)) ∨ Q)) replace proposition variable P9 by ¬(Q ∨ (A ∨ P)) in 18 20 ((Q ∨ (A ∨ P)) → (Q ∨ (A ∨ (Q ∨ P)))) → (¬(Q ∨ (A ∨ P)) ∨ ((A ∨ (Q ∨ P)) ∨ Q)) reverse abbreviation impl in 19 at occurence 1 21 ((Q ∨ (A ∨ P)) → (Q ∨ (A ∨ (Q ∨ P)))) → ((Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q)) reverse abbreviation impl in 20 at occurence 1 22 (Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q) modus ponens with 11, 21 23 P → (P ∨ Q) add axiom axiom2 24 A → (A ∨ Q) replace proposition variable P by A in 23 25 A → (A ∨ P) replace proposition variable Q by P in 24 26 Q → (Q ∨ P) replace proposition variable A by Q in 25 27 P → (A ∨ P) replace proposition variable Q by A in 5 28 (Q ∨ P) → (A ∨ (Q ∨ P)) replace proposition variable P by Q ∨ P in 27 29 ((Q ∨ P) → P8) → ((P9 ∨ (Q ∨ P)) → (P9 ∨ P8)) replace proposition variable P7 by Q ∨ P in 4 30 ((Q ∨ P) → (A ∨ (Q ∨ P))) → ((P9 ∨ (Q ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P)))) replace proposition variable P8 by A ∨ (Q ∨ P) in 29 31 (P9 ∨ (Q ∨ P)) → (P9 ∨ (A ∨ (Q ∨ P))) modus ponens with 28, 30 32 (¬Q ∨ (Q ∨ P)) → (¬Q ∨ (A ∨ (Q ∨ P))) replace proposition variable P9 by ¬Q in 31 33 (Q → (Q ∨ P)) → (¬Q ∨ (A ∨ (Q ∨ P))) reverse abbreviation impl in 32 at occurence 1 34 (Q → (Q ∨ P)) → (Q → (A ∨ (Q ∨ P))) reverse abbreviation impl in 33 at occurence 1 35 Q → (A ∨ (Q ∨ P)) modus ponens with 26, 34 36 (Q → P8) → ((P9 ∨ Q) → (P9 ∨ P8)) replace proposition variable P7 by Q in 4 37 (Q → (A ∨ (Q ∨ P))) → ((P9 ∨ Q) → (P9 ∨ (A ∨ (Q ∨ P)))) replace proposition variable P8 by A ∨ (Q ∨ P) in 36 38 (P9 ∨ Q) → (P9 ∨ (A ∨ (Q ∨ P))) modus ponens with 35, 37 39 ((A ∨ (Q ∨ P)) ∨ Q) → ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) replace proposition variable P9 by A ∨ (Q ∨ P) in 38 40 (P ∨ P) → P add axiom axiom1 41 ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) → (A ∨ (Q ∨ P)) replace proposition variable P by A ∨ (Q ∨ P) in 40 42 (((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) → P8) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ P8)) replace proposition variable P7 by (A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)) in 4 43 (((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P))) → (A ∨ (Q ∨ P))) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ (A ∨ (Q ∨ P)))) replace proposition variable P8 by A ∨ (Q ∨ P) in 42 44 (P9 ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (P9 ∨ (A ∨ (Q ∨ P))) modus ponens with 41, 43 45 (¬((A ∨ (Q ∨ P)) ∨ Q) ∨ ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (¬((A ∨ (Q ∨ P)) ∨ Q) ∨ (A ∨ (Q ∨ P))) replace proposition variable P9 by ¬((A ∨ (Q ∨ P)) ∨ Q) in 44 46 (((A ∨ (Q ∨ P)) ∨ Q) → ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (¬((A ∨ (Q ∨ P)) ∨ Q) ∨ (A ∨ (Q ∨ P))) reverse abbreviation impl in 45 at occurence 1 47 (((A ∨ (Q ∨ P)) ∨ Q) → ((A ∨ (Q ∨ P)) ∨ (A ∨ (Q ∨ P)))) → (((A ∨ (Q ∨ P)) ∨ Q) → (A ∨ (Q ∨ P))) reverse abbreviation impl in 46 at occurence 1 48 ((A ∨ (Q ∨ P)) ∨ Q) → (A ∨ (Q ∨ P)) modus ponens with 39, 47 49 (((A ∨ (Q ∨ P)) ∨ Q) → P8) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (P9 ∨ P8)) replace proposition variable P7 by (A ∨ (Q ∨ P)) ∨ Q in 4 50 (((A ∨ (Q ∨ P)) ∨ Q) → (A ∨ (Q ∨ P))) → ((P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (P9 ∨ (A ∨ (Q ∨ P)))) replace proposition variable P8 by A ∨ (Q ∨ P) in 49 51 (P9 ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (P9 ∨ (A ∨ (Q ∨ P))) modus ponens with 48, 50 52 (¬(Q ∨ (A ∨ P)) ∨ ((A ∨ (Q ∨ P)) ∨ Q)) → (¬(Q ∨ (A ∨ P)) ∨ (A ∨ (Q ∨ P))) replace proposition variable P9 by ¬(Q ∨ (A ∨ P)) in 51 53 ((Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q)) → (¬(Q ∨ (A ∨ P)) ∨ (A ∨ (Q ∨ P))) reverse abbreviation impl in 52 at occurence 1 54 ((Q ∨ (A ∨ P)) → ((A ∨ (Q ∨ P)) ∨ Q)) → ((Q ∨ (A ∨ P)) → (A ∨ (Q ∨ P))) reverse abbreviation impl in 53 at occurence 1 55 (Q ∨ (A ∨ P)) → (A ∨ (Q ∨ P)) modus ponens with 22, 54 56 (P7 ∨ (A ∨ P)) → (A ∨ (P7 ∨ P)) replace proposition variable Q by P7 in 55 57 (P7 ∨ (Q ∨ P)) → (Q ∨ (P7 ∨ P)) replace proposition variable A by Q in 56 58 (P7 ∨ (Q ∨ A)) → (Q ∨ (P7 ∨ A)) replace proposition variable P by A in 57 59 (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) replace proposition variable P7 by P in 58 qed

The fifth primitive proposition is our fourth axiom:

6. Proposition
(P → Q) → ((A ∨ P) → (A ∨ Q))     (prin5)

Proof:
 1 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4 qed