INTRODUCTION
************
Definition of the set of natural numbers proposed by WM (version 2.0):
ALL(a):[a e n <=> ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]]
Unfortunately, this definition is satisfied by the conditions, 0+1=0 and n = {0}.
Notice that 1 has not been defined to be a natural number. Addition on has also not been defined at all. So, WM's use of the '+1' notation is a bit misleading. It is really a successor function using a unary, post-fix notation.
(This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )
AXIOMS
******
1 0+1=0
Axiom
Informally, n = {0}
2 ALL(a):[a e n <=> a=0]
Axiom
PROOF
*****
'=>'
Prove: ALL(a):[a e n
=> ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]]
Suppose...
3 x e n
Premise
Apply definition of n
4 x e n <=> x=0
U Spec, 2
5 [x e n => x=0] & [x=0 => x e n]
Iff-And, 4
6 x e n => x=0
Split, 5
7 x=0 => x e n
Split, 5
8 x=0
Detach, 6, 3
Prove: ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => x e b]
Suppose...
9 0 e p & ALL(c):[c e p => c+1 e p]
Premise
10 0 e p
Split, 9
11 ALL(c):[c e p => c+1 e p]
Split, 9
12 x e p
Substitute, 8, 10
As Required:
13 ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => x e b]
4 Conclusion, 9
As Required:
14 ALL(a):[a e n
=> ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]]
4 Conclusion, 3
'<='
Prove: ALL(a):[ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]
=> a e n]
Suppose...
15 ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => x e b]
Premise
Sufficient: x e n
16 0 e n & ALL(c):[c e n => c+1 e n] => x e n
U Spec, 15
Apply definition of n
17 0 e n <=> 0=0
U Spec, 2
18 [0 e n => 0=0] & [0=0 => 0 e n]
Iff-And, 17
19 0 e n => 0=0
Split, 18
20 0=0 => 0 e n
Split, 18
21 0=0
Reflex
22 0 e n
Detach, 20, 21
Prove: ALL(c):[c e n => c+1 e n]
Suppose...
23 y e n
Premise
Apply definition of n
24 y e n <=> y=0
U Spec, 2
25 [y e n => y=0] & [y=0 => y e n]
Iff-And, 24
26 y e n => y=0
Split, 25
27 y=0 => y e n
Split, 25
28 y=0
Detach, 26, 23
29 y+1=y
Substitute, 28, 1
30 y+1 e n
Substitute, 29, 23
As Required:
31 ALL(c):[c e n => c+1 e n]
4 Conclusion, 23
Joining results...
32 0 e n & ALL(c):[c e n => c+1 e n]
Join, 22, 31
33 x e n
Detach, 16, 32
As Required:
34 ALL(a):[ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]
=> a e n]
4 Conclusion, 15
Joining results...
35 ALL(a):[[a e n
=> ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]] & [ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]
=> a e n]]
Join, 14, 34
As Required:
36 ALL(a):[a e n
<=> ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => a e b]]
Iff-And, 35