THEOREM
*******
ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & (b,a) e next]]]
(This formal proof was prepared with the use of the author's DC Proof 2.0 software available free at http://www.dcproof.com )
AXIOMS
******
n is a set
1 Set(n)
Axiom
2 0 e n
Axiom
3 max e n
Axiom
next is a set of ordered pairs of elements of n
4 Set'(next)
Axiom
5 ALL(a):ALL(b):[(a,b) e next => a e n & b e n]
Axiom
0 has no predecessor
6 ALL(a):[a e n => ~(a,0) e next]
Axiom
max has no successor
7 ALL(a):[a e n => ~(max,a) e next]
Axiom
All numbers but max have a successor
8 ALL(a):[a e n => [~a=max => EXIST(b):[b e n & (a,b) e next]]]
Axiom
If a number has a successor, that successor is unique.
9 ALL(a):ALL(b):ALL(c):[(a,b) e next & (a,c) e next => b=c]
Axiom
If numbers x and y have the same successors, then x = y. (Cancelling +1)
10 ALL(a):ALL(b):ALL(c):ALL(d):[(a,b) e next & (c,d) e next => [b=d => a=c]]
Axiom
Induction
11 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => ALL(c):[(b,c) e next => c e a]]
=> ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Apply Subset Axiom for induction
12 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & [~a=0 => EXIST(b):[b e n & (b,a) e next]]]]
Subset, 1
13 Set(p) & ALL(a):[a e p <=> a e n & [~a=0 => EXIST(b):[b e n & (b,a) e next]]]
E Spec, 12
Define: p
14 Set(p)
Split, 13
15 ALL(a):[a e p <=> a e n & [~a=0 => EXIST(b):[b e n & (b,a) e next]]]
Split, 13
Apply induction axiom
16 Set(p) & ALL(b):[b e p => b e n]
=> [0 e p & ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
=> ALL(b):[b e n => b e p]]
U Spec, 11
Prove: ALL(b):[b e p => b e n]
Suppose...
17 x e p
Premise
Apply definition of p
18 x e p <=> x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
U Spec, 15
19 [x e p => x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]]
& [x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]] => x e p]
Iff-And, 18
20 x e p => x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
Split, 19
21 x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]] => x e p
Split, 19
22 x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
Detach, 20, 17
23 x e n
Split, 22
As Required:
24 ALL(b):[b e p => b e n]
4 Conclusion, 17
Joining results...
25 Set(p) & ALL(b):[b e p => b e n]
Join, 14, 24
Sufficient: ALL(b):[b e n => b e p]
26 0 e p & ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
=> ALL(b):[b e n => b e p]
Detach, 16, 25
Prove: 0 e p
Apply definition of p
27 0 e p <=> 0 e n & [~0=0 => EXIST(b):[b e n & (b,0) e next]]
U Spec, 15
28 [0 e p => 0 e n & [~0=0 => EXIST(b):[b e n & (b,0) e next]]]
& [0 e n & [~0=0 => EXIST(b):[b e n & (b,0) e next]] => 0 e p]
Iff-And, 27
29 0 e p => 0 e n & [~0=0 => EXIST(b):[b e n & (b,0) e next]]
Split, 28
30 0 e n & [~0=0 => EXIST(b):[b e n & (b,0) e next]] => 0 e p
Split, 28
31 0=0
Reflex
32 ~0=0 => EXIST(b):[b e n & (b,0) e next]
Arb Cons, 31
33 0 e n & [~0=0 => EXIST(b):[b e n & (b,0) e next]]
Join, 2, 32
As Required:
34 0 e p
Detach, 30, 33
Prove: ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
Suppose...
35 x e p
Premise
Apply definition of p
36 x e p <=> x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
U Spec, 15
37 [x e p => x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]]
& [x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]] => x e p]
Iff-And, 36
38 x e p => x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
Split, 37
39 x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]] => x e p
Split, 37
40 x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
Detach, 38, 35
41 x e n
Split, 40
42 ~x=0 => EXIST(b):[b e n & (b,x) e next]
Split, 40
Prove: ALL(c):[(x,c) e next => c e p]
Suppose...
43 (x,x') e next
Premise
Apply definition of p
44 x' e p <=> x' e n & [~x'=0 => EXIST(b):[b e n & (b,x') e next]]
U Spec, 15
45 [x' e p => x' e n & [~x'=0 => EXIST(b):[b e n & (b,x') e next]]]
& [x' e n & [~x'=0 => EXIST(b):[b e n & (b,x') e next]] => x' e p]
Iff-And, 44
46 x' e p => x' e n & [~x'=0 => EXIST(b):[b e n & (b,x') e next]]
Split, 45
47 x' e n & [~x'=0 => EXIST(b):[b e n & (b,x') e next]] => x' e p
Split, 45
Apply definition of next
48 ALL(b):[(x,b) e next => x e n & b e n]
U Spec, 5
49 (x,x') e next => x e n & x' e n
U Spec, 48
50 x e n & x' e n
Detach, 49, 43
51 x e n
Split, 50
52 x' e n
Split, 50
53 x' e n & [~~x'=0 | EXIST(b):[b e n & (b,x') e next]] => x' e p
Imply-Or, 47
Sufficient: x' e p
54 x' e n & [x'=0 | EXIST(b):[b e n & (b,x') e next]] => x' e p
Rem DNeg, 53
55 x e n & (x,x') e next
Join, 41, 43
56 EXIST(b):[b e n & (b,x') e next]
E Gen, 55
57 x'=0 | EXIST(b):[b e n & (b,x') e next]
Arb Or, 56
58 x' e n & [x'=0 | EXIST(b):[b e n & (b,x') e next]]
Join, 52, 57
59 x' e p
Detach, 54, 58
As Required:
60 ALL(c):[(x,c) e next => c e p]
4 Conclusion, 43
As Required:
61 ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
4 Conclusion, 35
62 0 e p
& ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
Join, 34, 61
63 ALL(b):[b e n => b e p]
Detach, 26, 62
Prove: ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & (b,a) e next]]]
Suppose...
64 x e n
Premise
Apply previous result
65 x e n => x e p
U Spec, 63
66 x e p
Detach, 65, 64
67 x e p <=> x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
U Spec, 15
68 [x e p => x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]]
& [x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]] => x e p]
Iff-And, 67
69 x e p => x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
Split, 68
70 x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]] => x e p
Split, 68
71 x e n & [~x=0 => EXIST(b):[b e n & (b,x) e next]]
Detach, 69, 66
72 x e n
Split, 71
73 ~x=0 => EXIST(b):[b e n & (b,x) e next]
Split, 71
As Required:
74 ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & (b,a) e next]]]
4 Conclusion, 64