THEOREM
-------
The natural numbers (or natural-number-like structures) are embedded in every infinite set.
This proof makes use of set-theoretic axioms only to construct subsets and Cartesian products. It makes no use of axioms of infinity.
This proof was written with the aid of the author's DC Proof 2.0 software availabe free at
PREVIOUS RESULTS
----------------
If f maps x to y, and f is both injective (1-1) and surjective (onto) then
f has an inverse f'.
1 ALL(x):ALL(y):ALL(f):[Set(x)
& Set(y)
& ALL(a):[a e x => f(a) e y]
& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
& ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e x]
& ALL(a):ALL(b):[a e y & b e x => [f'(a)=b <=> f(b)=a]]
& ALL(a):ALL(b):[a e y & b e y => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e y & f'(b)=a]]]]
Axiom
If f is an injective function defined on set s, then, for every element s1 of s with no pre-image under f, there exists a unique subset n of s on which the Peano axioms hold.
2 ALL(s):ALL(f):[Set(s)
& ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
=> ALL(s1):[s1 e s & ALL(b):[b e s => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]]
Axiom
PROOF
-----
Suppose set s is Dedekind-infinite
3 Set(s)
& EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e s]
& EXIST(a):[a e s & ~a e s']
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]]
Premise
Splitting up this premise...
s is a set
4 Set(s)
Split, 3
There exits a proper subset s' of s and a bejection f from s' to s
5 EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e s]
& EXIST(a):[a e s & ~a e s']
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]]
Split, 3
6 EXIST(f):[Set(s')
& ALL(a):[a e s' => a e s]
& EXIST(a):[a e s & ~a e s']
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]]
E Spec, 5
Define: s' and f
7 Set(s')
& ALL(a):[a e s' => a e s]
& EXIST(a):[a e s & ~a e s']
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]
E Spec, 6
Splitting this premise...
s' is a set
8 Set(s')
Split, 7
s' is a subset of s
9 ALL(a):[a e s' => a e s]
Split, 7
At least one elment of s is not in s'
10 EXIST(a):[a e s & ~a e s']
Split, 7
f is a function mapping s' to s
11 ALL(a):[a e s' => f(a) e s]
Split, 7
f is injective (1 to 1)
12 ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
Split, 7
f is surjective (onto)
13 ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]
Split, 7
Let s1 be an element of s not in s'
14 s1 e s & ~s1 e s'
E Spec, 10
15 s1 e s
Split, 14
16 ~s1 e s'
Split, 14
Joining previous results...
17 Set(s') & Set(s)
Join, 8, 4
18 Set(s') & Set(s) & ALL(a):[a e s' => f(a) e s]
Join, 17, 11
19 Set(s') & Set(s) & ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
Join, 18, 12
20 Set(s') & Set(s) & ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]
Join, 19, 13
Apply previous result for inverse functions
21 ALL(y):ALL(f):[Set(s')
& Set(y)
& ALL(a):[a e s' => f(a) e y]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e y => EXIST(b):[b e s' & f(b)=a]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e s']
& ALL(a):ALL(b):[a e y & b e s' => [f'(a)=b <=> f(b)=a]]
& ALL(a):ALL(b):[a e y & b e y => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e s' => EXIST(b):[b e y & f'(b)=a]]]]
U Spec, 1
22 ALL(f):[Set(s')
& Set(s)
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]
=> EXIST(f'):[ALL(a):[a e s => f'(a) e s']
& ALL(a):ALL(b):[a e s & b e s' => [f'(a)=b <=> f(b)=a]]
& ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e s' => EXIST(b):[b e s & f'(b)=a]]]]
U Spec, 21
23 Set(s')
& Set(s)
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]
=> EXIST(f'):[ALL(a):[a e s => f'(a) e s']
& ALL(a):ALL(b):[a e s & b e s' => [f'(a)=b <=> f(b)=a]]
& ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e s' => EXIST(b):[b e s & f'(b)=a]]]
U Spec, 22
24 Set(s') & Set(s)
Join, 8, 4
25 Set(s') & Set(s) & ALL(a):[a e s' => f(a) e s]
Join, 24, 11
26 Set(s') & Set(s) & ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
Join, 25, 12
27 Set(s') & Set(s) & ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]
Join, 26, 13
28 EXIST(f'):[ALL(a):[a e s => f'(a) e s']
& ALL(a):ALL(b):[a e s & b e s' => [f'(a)=b <=> f(b)=a]]
& ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e s' => EXIST(b):[b e s & f'(b)=a]]]
Detach, 23, 27
29 ALL(a):[a e s => f'(a) e s']
& ALL(a):ALL(b):[a e s & b e s' => [f'(a)=b <=> f(b)=a]]
& ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e s' => EXIST(b):[b e s & f'(b)=a]]
E Spec, 28
Define: f', the inverse of f
30 ALL(a):[a e s => f'(a) e s']
Split, 29
31 ALL(a):ALL(b):[a e s & b e s' => [f'(a)=b <=> f(b)=a]]
Split, 29
32 ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
Split, 29
33 ALL(a):[a e s' => EXIST(b):[b e s & f'(b)=a]]
Split, 29
Apply previous result for natural-number-like structures embedded in other sets
34 ALL(f):[Set(s)
& ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
=> ALL(s1):[s1 e s & ALL(b):[b e s => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]]
U Spec, 2
35 Set(s)
& ALL(b):[b e s => f'(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f'(b)=f'(c) => b=c]]
=> ALL(s1):[s1 e s & ALL(b):[b e s => ~f'(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f'(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n' => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]
U Spec, 34
Prove: ALL(a):[a e s => f'(a) e s]
Suppose...
36 x e s
Premise
37 x e s => f'(x) e s'
U Spec, 30
38 f'(x) e s'
Detach, 37, 36
39 f'(x) e s' => f'(x) e s
U Spec, 9
40 f'(x) e s
Detach, 39, 38
As Required:
41 ALL(a):[a e s => f'(a) e s]
4 Conclusion, 36
Prove: ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
Suppose...
42 x e s & y e s
Premise
43 x e s
Split, 42
44 y e s
Split, 42
Prove: f'(x)=f'(y) => x=y
Suppose...
45 f'(x)=f'(y)
Premise
46 ALL(b):[x e s & b e s => [f'(x)=f'(b) => x=b]]
U Spec, 32
47 x e s & y e s => [f'(x)=f'(y) => x=y]
U Spec, 46
48 f'(x)=f'(y) => x=y
Detach, 47, 42
49 x=y
Detach, 48, 45
50 f'(x)=f'(y) => x=y
4 Conclusion, 45
As Required:
51 ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
4 Conclusion, 42
52 Set(s) & ALL(a):[a e s => f'(a) e s]
Join, 4, 41
53 Set(s) & ALL(a):[a e s => f'(a) e s]
& ALL(a):ALL(b):[a e s & b e s => [f'(a)=f'(b) => a=b]]
Join, 52, 51
54 ALL(s1):[s1 e s & ALL(b):[b e s => ~f'(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f'(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n' => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]
Detach, 35, 53
Sufficient: For existense of a natural-number-like structure
55 s1 e s & ALL(b):[b e s => ~f'(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f'(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n' => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]
U Spec, 54
Prove: ALL(b):[b e s => ~f'(b)=s1]
56 x e s
Premise
Prove: ~f'(x)=s1
Suppose to the contrary...
57 f'(x)=s1
Premise
58 x e s => f'(x) e s'
U Spec, 30
59 f'(x) e s'
Detach, 58, 56
60 s1 e s'
Substitute, 57, 59
61 s1 e s' & ~s1 e s'
Join, 60, 16
62 ~f'(x)=s1
4 Conclusion, 57
As Required:
63 ALL(b):[b e s => ~f'(b)=s1]
4 Conclusion, 56
64 s1 e s & ALL(b):[b e s => ~f'(b)=s1]
Join, 15, 63
65 EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f'(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n' => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]
Detach, 55, 64
Define: n, a natural-number-like structure in s
66 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f'(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n' => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]
E Spec, 65
67 Set(n)
Split, 66
68 ALL(b):[b e n => b e s]
Split, 66
69 s1 e n
Split, 66
70 ALL(b):[b e n => f'(b) e n]
Split, 66
71 ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
Split, 66
72 ALL(b):[b e n => ~f'(b)=s1]
Split, 66
73 ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
Split, 66
74 Set(n) & ALL(b):[b e n => b e s]
Join, 67, 68
75 Set(n) & ALL(b):[b e n => b e s] & s1 e n
Join, 74, 69
76 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
Join, 75, 70
77 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
Join, 76, 71
78 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
Join, 77, 72
79 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f'(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f'(b)=f'(c) => b=c]]
& ALL(b):[b e n => ~f'(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f'(c) e b]
=> ALL(c):[c e n => c e b]]
Join, 78, 73
As Required:
80 ALL(s):[Set(s)
& EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e s]
& EXIST(a):[a e s & ~a e s']
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]]
=> EXIST(n):EXIST(s1):EXIST(f):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]]]
4 Conclusion, 3