THEOREM
*******
Suppose we have a set n (finte or otherwise), a function s: n --> n and n0 e n. Then induction holds on set n if and only if all elements of n are reachable by repeated succession starting at n0, i.e. the set m = {n0, s(n0), s(s(n0)), ... } will contain every element of n.
Note that m is the smallest subset of n such that n0 e m and for all x e m, we also have s(x) e m.
More formally:
Set(m)
& ALL(a):[a e m <=> a e n
& ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
Prove: ALL(n):ALL(n0):ALL(s):[Set(n)
& n0 e n
& ALL(a):[a e n => s(a) e n]
=> [ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
<=> EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]]]
This proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
PROOF
*****
Suppose...
1 Set(n)
& ALL(a):[a e n => s(a) e n]
& n0 e n
Premise
n set a set (finite or otherwise)
2 Set(n)
Split, 1
s is a function mapping n to itself
3 ALL(a):[a e n => s(a) e n]
Split, 1
4 n0 e n
Split, 1
'=>'
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
Suppose induction holds on n
5 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Premise
Construct set m
Apply Subset Axiom
6 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]]
Subset, 2
7 Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
E Spec, 6
Define: m
8 Set(m)
Split, 7
9 ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
Split, 7
Prove: m is a subset of n
Suppose...
10 x e m
Premise
Apply definition of m
11 x e m <=> x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
U Spec, 9
12 [x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 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]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e m]
Iff-And, 11
13 x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Split, 12
14 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e m
Split, 12
15 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Detach, 13, 10
16 x e n
Split, 15
As Required:
17 ALL(a):[a e m => a e n]
4 Conclusion, 10
Prove: n0 e m
Apply definition of m
18 n0 e m <=> n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
U Spec, 9
19 [n0 e m => n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]]
& [n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b] => n0 e m]
Iff-And, 18
20 n0 e m => n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
Split, 19
Sufficient: For n0 e m
21 n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b] => n0 e m
Split, 19
Prove: ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
Suppose...
22 Set(x)
& ALL(c):[c e x => c e n]
& n0 e x
& ALL(c):[c e x => s(c) e x]
Premise
23 Set(x)
Split, 22
24 ALL(c):[c e x => c e n]
Split, 22
25 n0 e x
Split, 22
As Required:
26 ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
4 Conclusion, 22
Joining results...
27 n0 e n
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
Join, 4, 26
As Required:
28 n0 e m
Detach, 21, 27
29 x e m
Premise
30 s(x) e m <=> s(x) e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]
U Spec, 9
31 [s(x) e m => s(x) e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]]
& [s(x) e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b] => s(x) e m]
Iff-And, 30
32 s(x) e m => s(x) e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]
Split, 31
33 s(x) e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b] => s(x) e m
Split, 31
34 x e n => s(x) e n
U Spec, 3
35 x e m => x e n
U Spec, 17
36 x e n
Detach, 35, 29
37 s(x) e n
Detach, 34, 36
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]
Suppose...
38 Set(y) & ALL(c):[c e y => c e n]
& n0 e y
& ALL(c):[c e y => s(c) e y]
Premise
39 Set(y)
Split, 38
40 ALL(c):[c e y => c e n]
Split, 38
41 n0 e y
Split, 38
42 ALL(c):[c e y => s(c) e y]
Split, 38
43 x e y => s(x) e y
U Spec, 42
Apply definition of m
44 x e m <=> x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
U Spec, 9
45 [x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 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]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e m]
Iff-And, 44
46 x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Split, 45
47 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e m
Split, 45
48 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Detach, 46, 29
49 x e n
Split, 48
50 ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Split, 48
51 Set(y) & ALL(c):[c e y => c e n]
& n0 e y
& ALL(c):[c e y => s(c) e y]
=> x e y
U Spec, 50
52 x e y
Detach, 51, 38
53 s(x) e y
Detach, 43, 52
As Required:
54 ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]
4 Conclusion, 38
55 s(x) e n
& ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> s(x) e b]
Join, 37, 54
56 s(x) e m
Detach, 33, 55
As Required:
57 ALL(a):[a e m => s(a) e m]
4 Conclusion, 29
Apply induction principle (not a proof by induction)
58 Set(m) & ALL(b):[b e m => b e n]
=> [n0 e m & ALL(b):[b e m => s(b) e m]
=> ALL(b):[b e n => b e m]]
U Spec, 5
59 Set(m) & ALL(a):[a e m => a e n]
Join, 8, 17
60 n0 e m & ALL(b):[b e m => s(b) e m]
=> ALL(b):[b e n => b e m]
Detach, 58, 59
61 n0 e m & ALL(a):[a e m => s(a) e m]
Join, 28, 57
62 ALL(b):[b e n => b e m]
Detach, 60, 61
63 Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]
Join, 7, 62
As Required:
64 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
4 Conclusion, 5
'<='
Prove: EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
=> ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
65 EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
Premise
66 Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]
E Spec, 65
Define: m
67 Set(m)
Split, 66
68 ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
Split, 66
69 ALL(b):[b e n => b e m]
Split, 66
Prove: ALL(b):[b e m => b e n]
Suppose...
70 x e m
Premise
Apply definition of m
71 x e m <=> x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
U Spec, 68
72 [x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 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]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e m]
Iff-And, 71
73 x e m => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Split, 72
74 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e m
Split, 72
75 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Detach, 73, 70
76 x e n
Split, 75
As Required:
77 ALL(b):[b e m => b e n]
4 Conclusion, 70
78 ALL(b):[[b e n => b e m] & [b e m => b e n]]
Join, 69, 77
79 ALL(b):[b e n <=> b e m]
Iff-And, 78
Prove: n=m
Apply Set Equality Axiom
80 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
81 ALL(b):[Set(n) & Set(b) => [n=b <=> ALL(c):[c e n <=> c e b]]]
U Spec, 80
82 Set(n) & Set(m) => [n=m <=> ALL(c):[c e n <=> c e m]]
U Spec, 81
83 Set(n) & Set(m)
Join, 2, 67
84 n=m <=> ALL(c):[c e n <=> c e m]
Detach, 82, 83
85 [n=m => ALL(c):[c e n <=> c e m]]
& [ALL(c):[c e n <=> c e m] => n=m]
Iff-And, 84
86 n=m => ALL(c):[c e n <=> c e m]
Split, 85
87 ALL(c):[c e n <=> c e m] => n=m
Split, 85
As Required:
88 n=m
Detach, 87, 79
89 Set(n) & ALL(a):[a e n <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e n]
Substitute, 88, 66
90 Set(n)
Split, 89
91 ALL(a):[a e n <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
Split, 89
92 ALL(b):[b e n => b e n]
Split, 89
Apply definition of m
93 n0 e m <=> n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
U Spec, 68
94 [n0 e m => n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]]
& [n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b] => n0 e m]
Iff-And, 93
95 n0 e m => n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
Split, 94
96 n0 e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b] => n0 e m
Split, 94
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
Suppose...
97 Set(x) & ALL(c):[c e x => c e n]
& n0 e x
& ALL(c):[c e x => s(c) e x]
Premise
98 Set(x)
Split, 97
99 ALL(c):[c e x => c e n]
Split, 97
100 n0 e x
Split, 97
As Required:
101 ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
4 Conclusion, 97
Joining results...
102 n0 e n
& ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> n0 e b]
Join, 4, 101
As Required:
103 n0 e m
Detach, 96, 102
Prove: ALL(a):[a e m => s(a) e m]
Suppose...
104 x e m
Premise
105 x e n => s(x) e n
U Spec, 3
106 x e m => x e n
U Spec, 77
107 x e n
Detach, 106, 104
108 s(x) e n
Detach, 105, 107
109 s(x) e n => s(x) e m
U Spec, 69
110 s(x) e m
Detach, 109, 108
As Required:
111 ALL(a):[a e m => s(a) e m]
4 Conclusion, 104
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
112 Set(p) & ALL(b):[b e p => b e n]
Premise
113 Set(p)
Split, 112
114 ALL(b):[b e p => b e n]
Split, 112
Prove: n0 e p & ALL(b):[b e p => s(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
115 n0 e p & ALL(b):[b e p => s(b) e p]
Premise
116 n0 e p
Split, 115
117 ALL(b):[b e p => s(b) e p]
Split, 115
Prove: ALL(b):[b e n => b e p]
Suppose...
118 x e n
Premise
Apply previous result
119 x e n <=> x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
U Spec, 91
120 [x e n => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 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]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e n]
Iff-And, 119
121 x e n => x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Split, 120
122 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b] => x e n
Split, 120
123 x e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Detach, 121, 118
124 x e n
Split, 123
125 ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> x e b]
Split, 123
126 Set(p) & ALL(c):[c e p => c e n]
& n0 e p
& ALL(c):[c e p => s(c) e p]
=> x e p
U Spec, 125
Joining results...
127 Set(p) & ALL(b):[b e p => b e n] & n0 e p
Join, 112, 116
128 Set(p) & ALL(b):[b e p => b e n] & n0 e p
& ALL(b):[b e p => s(b) e p]
Join, 127, 117
129 x e p
Detach, 126, 128
As Required:
130 ALL(b):[b e n => b e p]
4 Conclusion, 118
As Required:
131 n0 e p & ALL(b):[b e p => s(b) e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 115
As Required:
132 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 112
As Required:
133 EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
=> ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 65
Joining results...
134 [ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]]
& [EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
=> ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]]
Join, 64, 133
Apply Iff-And Rule
135 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
<=> EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]
Iff-And, 134
As Required:
136 ALL(n):ALL(s):ALL(n0):[Set(n)
& ALL(a):[a e n => s(a) e n]
& n0 e n
=> [ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
<=> EXIST(m):[Set(m) & ALL(a):[a e m <=> a e n & ALL(b):[Set(b) & ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => s(c) e b]
=> a e b]]
& ALL(b):[b e n => b e m]]]]
4 Conclusion, 1