for questions or link request: module admin

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