Here we apply WM's proposed definition of the natural numbers to obtain:
1 e n
1+1 e n
1+1+1 e n
ALL(a):[aen => EXIST(b):[ben & b=a+1]]
2=1+1
3=2+1
4=3+1
(This proof was written with aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )
Define: n (proposed by WM)
*********
1 ALL(a):[a e n
<=> ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => a e b]]
Axiom
Prove: 1en
Apply definition of 1
2 1 e n
<=> ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b]
U Spec, 1
3 [1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b]]
& [ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b] => 1 e n]
Iff-And, 2
4 1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b]
Split, 3
5 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b] => 1 e n
Split, 3
Prove: ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b]
Suppose...
6 1 e p & ALL(c):[c e p => c+1 e p]
Premise
7 1 e p
Split, 6
As Required:
8 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1 e b]
4 Conclusion, 6
As Required:
9 1 e n
Detach, 5, 8
Prove: 1+1 e n
Apply definiton of n
10 1+1 e n
<=> ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1 e b]
U Spec, 1
11 [1+1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1 e b]]
& [ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1 e b] => 1+1 e n]
Iff-And, 10
12 1+1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1 e b]
Split, 11
13 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1 e b] => 1+1 e n
Split, 11
Prove: ALL(bp):[1 e bp & ALL(c):[c e bp => c+1 e bp] => 1+1 e bp]
Suppose...
14 1 e p & ALL(c):[c e p => c+1 e p]
Premise
15 1 e p
Split, 14
16 ALL(c):[c e p => c+1 e p]
Split, 14
17 1 e p => 1+1 e p
U Spec, 16
18 1+1 e p
Detach, 17, 15
As Required:
19 ALL(bp):[1 e bp & ALL(c):[c e bp => c+1 e bp] => 1+1 e bp]
4 Conclusion, 14
As Required:
20 1+1 e n
Detach, 13, 19
Prove: 1+1+1 e n
Apply definition of n
21 1+1+1 e n
<=> ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b]
U Spec, 1
22 [1+1+1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b]]
& [ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b] => 1+1+1 e n]
Iff-And, 21
23 1+1+1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b]
Split, 22
24 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b] => 1+1+1 e n
Split, 22
Prove: ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b]
Suppose...
25 1 e p & ALL(c):[c e p => c+1 e p]
Premise
26 1 e p
Split, 25
27 ALL(c):[c e p => c+1 e p]
Split, 25
28 1+1 e p => 1+1+1 e p
U Spec, 27
29 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1 e b]
Detach, 12, 20
30 1 e p & ALL(c):[c e p => c+1 e p] => 1+1 e p
U Spec, 29
31 1+1 e p
Detach, 30, 25
32 1+1+1 e p
Detach, 28, 31
As Required:
33 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => 1+1+1 e b]
4 Conclusion, 25
As Required:
34 1+1+1 e n
Detach, 24, 33
Prove: ALL(a):[a e n => EXIST(b):[b e n & b=a+1]]
Suppose...
35 x e n
Premise
Apply definition n
36 x e n
<=> ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x e b]
U Spec, 1
37 [x e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x e b]]
& [ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x e b] => x e n]
Iff-And, 36
38 x e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x e b]
Split, 37
39 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x e b] => x e n
Split, 37
40 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x e b]
Detach, 38, 35
Apply definition of n
41 x+1 e n
<=> ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b]
U Spec, 1
42 [x+1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b]]
& [ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b] => x+1 e n]
Iff-And, 41
43 x+1 e n => ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b]
Split, 42
Sufficient:
44 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b] => x+1 e n
Split, 42
Prove: ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b]
Suppose...
45 1 e p & ALL(c):[c e p => c+1 e p]
Premise
46 1 e p
Split, 45
47 ALL(c):[c e p => c+1 e p]
Split, 45
Sufficient: x+1 e p
48 x e p => x+1 e p
U Spec, 47
49 1 e p & ALL(c):[c e p => c+1 e p] => x e p
U Spec, 40
50 x e p
Detach, 49, 45
51 x+1 e p
Detach, 48, 50
As Required:
52 ALL(b):[1 e b & ALL(c):[c e b => c+1 e b] => x+1 e b]
4 Conclusion, 45
53 x+1 e n
Detach, 44, 52
54 x+1=x+1
Reflex
55 x+1 e n & x+1=x+1
Join, 53, 54
Generalizing...
56 EXIST(b):[b e n & b=x+1]
E Gen, 55
As Required:
57 ALL(a):[a e n => EXIST(b):[b e n & b=a+1]]
4 Conclusion, 35
Prove: 2=1+1
Apply previous result
58 1 e n => EXIST(b):[b e n & b=1+1]
U Spec, 57
59 EXIST(b):[b e n & b=1+1]
Detach, 58, 9
60 2 e n & 2=1+1
E Spec, 59
61 2 e n
Split, 60
As Required:
62 2=1+1
Split, 60
Prove: 3=2+1
Apply previous result
63 2 e n => EXIST(b):[b e n & b=2+1]
U Spec, 57
64 EXIST(b):[b e n & b=2+1]
Detach, 63, 61
65 3 e n & 3=2+1
E Spec, 64
66 3 e n
Split, 65
As Required:
67 3=2+1
Split, 65
Prove: 4=3+1
Apply previous result
68 3 e n => EXIST(b):[b e n & b=3+1]
U Spec, 57
69 EXIST(b):[b e n & b=3+1]
Detach, 68, 66
70 4 e n & 4=3+1
E Spec, 69
71 4 e n
Split, 70
As Required:
72 4=3+1
Split, 70