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