INTRODUCTION
************
Suppose we have a set n,
function s: n --> n, and 0 e n.
Then we can construct, i.e.
prove the existence of subset m of n such that:
m = {0, S(0),
S(S(0)) ... }
Now, if we assume n = m, the Principle
of Mathematical Induction follows immediately.
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 software available
at http://www.dcproof.com
PROOF
******
Define: n, s and 0
1 Set(n)
Axiom
2 0 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
Construct the set m
Apply the Subset Axiom
4 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
a e b]]]
Subset, 1
Define: m {0, s(0), s(s(0)) ... }
5 Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
a e b]]
E Spec, 4
6 Set(m)
Split, 5
7 ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
a e b]]
Split, 5
Prove: m=n
=> ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
8 m=n
Premise
9 ALL(a):ALL(b):[Set(a) & Set(b) =>
[a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
10 ALL(b):[Set(m) & Set(b)
=> [m=b <=> ALL(c):[c e m <=> c e b]]]
U Spec, 9
11 Set(m) & Set(n) => [m=n <=> ALL(c):[c e m <=> c e n]]
U Spec, 10
12 Set(m) & Set(n)
Join, 6, 1
13 m=n <=> ALL(c):[c e m <=> c e n]
Detach, 11, 12
14 [m=n => ALL(c):[c e m <=> c e n]]
&
[ALL(c):[c e m <=> c e n] => m=n]
Iff-And, 13
15 m=n => ALL(c):[c e m <=> c e n]
Split, 14
16 ALL(c):[c e m <=> c e n] => m=n
Split, 14
17 ALL(c):[c e m <=> c e n]
Detach, 15, 8
Prove: ALL(a):[Set(a) &
ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
18 Set(p) & ALL(b):[b e p => b e n]
Premise
19 Set(p)
Split, 18
20 ALL(b):[b e p => b e n]
Split, 18
Prove: 0 e p & ALL(b):[b e p => s(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
21 0 e p & ALL(b):[b e p => s(b) e p]
Premise
22 0 e p
Split, 21
23 ALL(b):[b e p => s(b) e p]
Split, 21
Prove: ALL(b):[b e n => b e p]
Suppose...
24 x e n
Premise
25 x e m <=> x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
& ALL(c):[c e b => s(c) e b]
=>
x e b]
U Spec, 7
26 [x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]]
&
[x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e m]
Iff-And, 25
27 x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 26
28 x e n & ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b] => x e m
Split, 26
29 x e m
Substitute, 8, 24
30 x e n & ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Detach, 27, 29
31 x e n
Split, 30
32 ALL(b):[Set(b) & ALL(c):[c e b => c e n]
&
0 e b
&
ALL(c):[c e b => s(c) e b]
=>
x e b]
Split, 30
Sufficient: For x e p
33 Set(p) & ALL(c):[c e p => c e n]
&
0 e p
&
ALL(c):[c e p => s(c) e p]
=>
x e p
U Spec, 32
34 Set(p) & ALL(b):[b e p => b e n] & 0 e p
Join, 18, 22
35 Set(p) & ALL(b):[b e p => b e n] & 0 e p
&
ALL(b):[b e p => s(b) e p]
Join, 34, 23
36 x e p
Detach, 33, 35
As Required:
37 ALL(b):[b e n => b e p]
4 Conclusion, 24
As Required:
38 0 e p & ALL(b):[b e p => s(b) e p]
=>
ALL(b):[b e n => b e p]
4 Conclusion, 21
As Required:
39 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=>
[0 e a & ALL(b):[b e a => s(b) e a]
=>
ALL(b):[b e n => b e a]]]
4 Conclusion, 18
As Required:
40 m=n
=>
ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=>
[0 e a & ALL(b):[b e a => s(b) e a]
=>
ALL(b):[b e n => b e a]]]
4 Conclusion, 8