THEOREM
*******
For any set s with element s1 e s and f: s --> s there exists n such that:
- n is a subset of s
- s1 e n
- f is closed on n
- the induction principle is applicable on n with successor function f
Informally: n = {s1, f(s1), f(f(s1), ...}
OUTLINE OF PROOF
****************
Lines
-----
5-8 Construct n using Subset Axiom
9-19 Prove s1 e n
20-47 Prove ALL(a):[aen => f(a) e n]
48-55 Prove n is a subset of s
56-88 Prove induction principle holds on n using successor function f
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
Prove: ALL(s):ALL(s1):ALL(f):[Set(s)
& s1 e s
& ALL(a):[a e s => f(a) e s]
=> EXIST(n):[Set(n)
& ALL(a):[a e n => a e s]
& s1 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [s1 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]]]
Suppose...
1 Set(s)
& s1 e s
& ALL(a):[a e s => f(a) e s]
Premise
Splitting premise...
2 Set(s)
Split, 1
3 s1 e s
Split, 1
f is a function mapping s to itself
4 ALL(a):[a e s => f(a) e s]
Split, 1
Construct n
Apply Subset Axiom
5 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => a e b]]]]
Subset, 2
6 Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => a e b]]]
E Spec, 5
Define: n
7 Set(n)
Split, 6
8 ALL(a):[a e n <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => a e b]]]
Split, 6
Prove: s1 e n
Apply definition of n
9 s1 e n <=> s1 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]]
U Spec, 8
10 [s1 e n => s1 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]]]
& [s1 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]] => s1 e n]
Iff-And, 9
11 s1 e n => s1 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]]
Split, 10
12 s1 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]] => s1 e n
Split, 10
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]]
Suppose...
13 Set(q) & ALL(c):[c e q => c e s]
Premise
Prove: s1 e q & ALL(c):[c e q => f(c) e q] => s1 e q
Suppose...
14 s1 e q & ALL(c):[c e q => f(c) e q]
Premise
15 s1 e q
Split, 14
As Required:
16 s1 e q & ALL(c):[c e q => f(c) e q] => s1 e q
4 Conclusion, 14
As Required:
17 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]]
4 Conclusion, 13
Joining results...
18 s1 e s
& ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => s1 e b]]
Join, 3, 17
As Required:
19 s1 e n
Detach, 12, 18
Prove: ALL(a):[aen => f(a)en]
Suppose...
20 x e n
Premise
Apply definition of n
21 x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
U Spec, 8
22 [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]]
& [x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n]
Iff-And, 21
23 x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 22
24 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n
Split, 22
25 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Detach, 23, 20
26 x e s
Split, 25
27 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 25
Apply definiton of n
28 f(x) e n <=> f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
U Spec, 8
29 [f(x) e n => f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]]
& [f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]] => f(x) e n]
Iff-And, 28
30 f(x) e n => f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
Split, 29
Sufficient: For f(x) e n
31 f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]] => f(x) e n
Split, 29
Apply definition of f
32 x e s => f(x) e s
U Spec, 4
As Required:
33 f(x) e s
Detach, 32, 26
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]] => f(x) e n
Suppose...
34 Set(q) & ALL(c):[c e q => c e s]
Premise
Prove: s1 e q & ALL(c):[c e q => f(c) e q] => f(x) e q
Suppose...
35 s1 e q & ALL(c):[c e q => f(c) e q]
Premise
36 s1 e q
Split, 35
37 ALL(c):[c e q => f(c) e q]
Split, 35
Sufficient: f(x) e q
38 x e q => f(x) e q
U Spec, 37
Apply previous result
39 Set(q) & ALL(c):[c e q => c e s]
=> [s1 e q & ALL(c):[c e q => f(c) e q] => x e q]
U Spec, 27
40 s1 e q & ALL(c):[c e q => f(c) e q] => x e q
Detach, 39, 34
41 x e q
Detach, 40, 35
42 f(x) e q
Detach, 38, 41
As Required:
43 s1 e q & ALL(c):[c e q => f(c) e q] => f(x) e q
4 Conclusion, 35
As Required:
44 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
4 Conclusion, 34
Joining results...
45 f(x) e s
& ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => f(x) e b]]
Join, 33, 44
46 f(x) e n
Detach, 31, 45
As Required:
47 ALL(a):[a e n => f(a) e n]
4 Conclusion, 20
Prove: ALL(a):[a e n => a e s]
Suppose...
48 x e n
Premise
Apply definition of n
49 x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
U Spec, 8
50 [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]]
& [x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n]
Iff-And, 49
51 x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 50
52 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n
Split, 50
53 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Detach, 51, 48
54 x e s
Split, 53
As Required:
55 ALL(a):[a e n => a e s]
4 Conclusion, 48
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [s1 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
56 Set(p) & ALL(b):[b e p => b e n]
Premise
57 Set(p)
Split, 56
58 ALL(b):[b e p => b e n]
Split, 56
Prove: s1 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
59 s1 e p & ALL(b):[b e p => f(b) e p]
Premise
Prove: ALL(b):[b e n => b e p]
Suppose...
60 x e n
Premise
Apply definition of n
61 x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
U Spec, 8
62 [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]]
& [x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n]
Iff-And, 61
63 x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 62
64 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]] => x e n
Split, 62
65 x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Detach, 63, 60
66 x e s
Split, 65
67 ALL(b):[Set(b) & ALL(c):[c e b => c e s]
=> [s1 e b & ALL(c):[c e b => f(c) e b] => x e b]]
Split, 65
68 Set(p) & ALL(c):[c e p => c e s]
=> [s1 e p & ALL(c):[c e p => f(c) e p] => x e p]
U Spec, 67
Prove: ALL(c):[c e p => c e s]
Suppose...
69 y e p
Premise
70 y e p => y e n
U Spec, 58
71 y e n
Detach, 70, 69
72 y e n => y e s
U Spec, 55
73 y e s
Detach, 72, 71
As Required:
74 ALL(c):[c e p => c e s]
4 Conclusion, 69
Joining results...
75 Set(p) & ALL(c):[c e p => c e s]
Join, 57, 74
76 s1 e p & ALL(c):[c e p => f(c) e p] => x e p
Detach, 68, 75
77 x e p
Detach, 76, 59
As Required:
78 ALL(b):[b e n => b e p]
4 Conclusion, 60
As Required:
79 s1 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 59
Induction principle
As Required:
80 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [s1 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 56
Joining results...
81 Set(n) & ALL(a):[a e n => a e s]
Join, 7, 55
82 Set(n) & ALL(a):[a e n => a e s] & s1 e n
Join, 81, 19
83 Set(n) & ALL(a):[a e n => a e s] & s1 e n
& ALL(a):[a e n => f(a) e n]
Join, 82, 47
84 Set(n) & ALL(a):[a e n => a e s] & s1 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [s1 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Join, 83, 80
As Required:
85 ALL(s):ALL(s1):ALL(f):[Set(s)
& s1 e s
& ALL(a):[a e s => f(a) e s]
=> EXIST(n):[Set(n) & ALL(a):[a e n => a e s] & s1 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [s1 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]]]
4 Conclusion, 1