THEOREM
*******
If there is no non-empty subset
of N that excludes 0 and that is not "accessible" from the rest of
the natural numbers by means of the successor function, then we can derive the
Principle of Mathematical Induction.
More formally:
~EXIST(p):EXIST(p'):[Set(p)
& Set(p') & ALL(b):[b e p => b e n]
& 0 e p
& ALL(a):[a e p' <=> a e n & ~a e p]
& ~Accessible(p,p')]
=> Induction
where 'Accessible' and
'Induction' are as defined below (lines 4-5).
The 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
*****
1 Set(n)
Axiom
From Peano's
Axioms (other axioms not used):
2 0 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
Define: Induction
'Induction' means that
induction holds on (n,s,0)
4 Induction <=> 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]]]
Axiom
Define: Accessible
'Accessible(x,y)' means subset y of n is accessible from subset x
of n by means of s
5 ALL(a):ALL(b):[ALL(c):[c e a => c e n] & EXIST(c):c e a & ALL(c):[c e b => c e n]
=>
[Accessible(a,b) <=>
EXIST(c):EXIST(d):[c e a & d e b & s(c)=d]]]
Axiom
Proof by contrapositive
Prove: ~Induction
=> EXIST(p):EXIST(p'):[Set(p) & Set(p') & ALL(b):[b e p => b e n]
& 0 e p
& ALL(a):[a e p' <=> a e n & ~a e p]
& ~Accessible(p,p')]
Suppose induction does NOT hold on (n,s,0)
6 ~Induction
Premise
Apply
definition of Induction
7 [Induction => 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]]]]
&
[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]]] => Induction]
Iff-And, 4
8 Induction => 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]]]
Split, 7
9 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]]] => Induction
Split, 7
10 ~Induction => ~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]]]
Contra, 9
11 ~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]]]
Detach, 10, 6
12 ~~EXIST(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]]]
Quant, 11
13 EXIST(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]]]
Rem DNeg, 12
14 EXIST(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]]]
Imply-And, 13
15 EXIST(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]]]
Rem DNeg, 14
16 EXIST(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]]]
Imply-And, 15
17 EXIST(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]]]
Rem DNeg, 16
18 EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a &
ALL(b):[b e a => s(b) e a] & ~~EXIST(b):~[b e n => b e a]]]
Quant, 17
19 EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a &
ALL(b):[b e a => s(b) e a] & EXIST(b):~[b e n => b e a]]]
Rem DNeg, 18
20 EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a &
ALL(b):[b e a => s(b) e a] & EXIST(b):~~[b e n & ~b e a]]]
Imply-And, 19
21 EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a &
ALL(b):[b e a => s(b) e a] & EXIST(b):[b e n & ~b e a]]]
Rem DNeg, 20
22 Set(p) & ALL(b):[b e p => b e n] & [0 e p & ALL(b):[b e p => s(b) e p] & EXIST(b):[b e n & ~b e p]]
E Spec, 21
Define: p
23 Set(p)
Split, 22
24 ALL(b):[b e p => b e n]
Split, 22
25 0 e p & ALL(b):[b e p => s(b) e p] & EXIST(b):[b e n & ~b e p]
Split, 22
26 0 e p
Split, 25
27 ALL(b):[b e p => s(b) e p]
Split, 25
28 EXIST(b):[b e n & ~b e p]
Split, 25
29 x0 e n & ~x0 e p
E Spec, 28
30 x0 e n
Split, 29
31 ~x0 e p
Split, 29
32 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ~a e p]]
Subset, 1
33 Set(p') & ALL(a):[a e p' <=> a e n & ~a e p]
E Spec, 32
Define: p'
34 Set(p')
Split, 33
35 ALL(a):[a e p' <=> a e n & ~a e p]
Split, 33
36 x0 e p' <=> x0 e n & ~x0 e p
U Spec, 35
37 [x0 e p' => x0 e n & ~x0 e p]
&
[x0 e n & ~x0 e p => x0 e p']
Iff-And, 36
38 x0 e p' => x0 e n & ~x0 e p
Split, 37
39 x0 e n & ~x0 e p => x0 e p'
Split, 37
40 x0 e p'
Detach, 39, 29
Apply defintion of Accessible(p,p')
41 ALL(b):[ALL(c):[c e p => c e n] & EXIST(c):c e p & ALL(c):[c e b => c e n]
=>
[Accessible(p,b) <=> EXIST(c):EXIST(d):[c e p & d e b & s(c)=d]]]
U Spec, 5
42 ALL(c):[c e p => c e n] & EXIST(c):c e p & ALL(c):[c e p' => c e n]
=>
[Accessible(p,p') <=>
EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]]
U Spec, 41
43 EXIST(c):c e p
E Gen, 26
Prove: ALL(c):[c e p' => c e n]
Suppose...
44 x e p'
Premise
45 x e p' <=> x e n & ~x e p
U Spec, 35
46 [x e p' => x e n & ~x e p] & [x e n & ~x e p => x e p']
Iff-And, 45
47 x e p' => x e n & ~x e p
Split, 46
48 x e n & ~x e p => x e p'
Split, 46
49 x e n & ~x e p
Detach, 47, 44
50 x e n
Split, 49
As Required:
51 ALL(c):[c e p' => c e n]
4 Conclusion, 44
52 ALL(b):[b e p => b e n] & EXIST(c):c e p
Join, 24, 43
53 ALL(b):[b e p => b e n] & EXIST(c):c e p
&
ALL(c):[c e p' => c e n]
Join, 52, 51
54 Accessible(p,p') <=>
EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]
Detach, 42, 53
55 [Accessible(p,p') =>
EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]]
&
[EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d] => Accessible(p,p')]
Iff-And, 54
56 Accessible(p,p') =>
EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]
Split, 55
57 EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d] => Accessible(p,p')
Split, 55
58 ~EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d] => ~Accessible(p,p')
Contra, 56
59 ~~ALL(c):~EXIST(d):[c e p & d e p' & s(c)=d] => ~Accessible(p,p')
Quant, 58
60 ALL(c):~EXIST(d):[c e p & d e p' & s(c)=d] => ~Accessible(p,p')
Rem DNeg, 59
61 ALL(c):~~ALL(d):~[c e p & d e p' & s(c)=d] => ~Accessible(p,p')
Quant, 60
62 ALL(c):ALL(d):~[c e p & d e p' & s(c)=d] => ~Accessible(p,p')
Rem DNeg, 61
63 ALL(c):ALL(d):~~[c e p & d e p' => ~s(c)=d] => ~Accessible(p,p')
Imply-And, 62
Sufficient: For ~Accessible(p,p')
64 ALL(c):ALL(d):[c e p & d e p' => ~s(c)=d] => ~Accessible(p,p')
Rem DNeg, 63
Prove: ALL(c):ALL(d):[c e p & d e p' =>
~s(c)=d]
Suppose...
65 y e p & y' e p'
Premise
66 y e p
Split, 65
67 y' e p'
Split, 65
Prove: ~s(y)=y'
Suppose to the contrary...
68 s(y)=y'
Premise
69 y e p => s(y) e p
U Spec, 27
70 s(y) e p
Detach, 69, 66
71 y' e p
Substitute, 68,
70
72 y' e p' <=> y' e n & ~y' e p
U Spec, 35
73 [y' e p' => y' e n & ~y' e p]
&
[y' e n & ~y' e p => y' e p']
Iff-And, 72
74 y' e p' => y' e n & ~y' e p
Split, 73
75 y' e n & ~y' e p => y' e p'
Split, 73
76 y' e n & ~y' e p
Detach, 74, 67
77 y' e n
Split, 76
78 ~y' e p
Split, 76
Obtain the contradiction...
79 y' e p & ~y' e p
Join, 71, 78
As Required:
80 ~s(y)=y'
4 Conclusion, 68
As Required:
81 ALL(c):ALL(d):[c e p & d e p' => ~s(c)=d]
4 Conclusion, 65
82 ~Accessible(p,p')
Detach, 64, 81
83 Set(p) & Set(p')
Join, 23, 34
84 Set(p) & Set(p') & ALL(b):[b e p => b e n]
Join, 83, 24
85 Set(p) & Set(p') & ALL(b):[b e p => b e n]
&
0 e p
Join, 84, 26
86 Set(p) & Set(p') & ALL(b):[b e p => b e n]
&
0 e p
&
ALL(a):[a e p' <=> a e n & ~a e p]
Join, 85, 35
87 Set(p) & Set(p') & ALL(b):[b e p => b e n]
&
0 e p
&
ALL(a):[a e p' <=> a e n & ~a e p]
&
~Accessible(p,p')
Join, 86, 82
As Required:
88 ~Induction
=>
EXIST(p):EXIST(p'):[Set(p) & Set(p') &
ALL(b):[b e p => b e n]
&
0 e p
&
ALL(a):[a e p' <=> a e n & ~a e p]
&
~Accessible(p,p')]
4 Conclusion, 6
Apply Contrapositive Rule
89 ~EXIST(p):EXIST(p'):[Set(p) & Set(p') & ALL(b):[b e p => b e n]
&
0 e p
&
ALL(a):[a e p' <=> a e n & ~a e p]
&
~Accessible(p,p')] =>
~~Induction
Contra, 88
As Required:
90 ~EXIST(p):EXIST(p'):[Set(p) & Set(p')
& ALL(b):[b e p => b e n]
&
0 e p
&
ALL(a):[a e p' <=> a e n & ~a e p]
&
~Accessible(p,p')] =>
Induction
Rem DNeg, 89