# 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