THEOREM
*******
From any Dedekind infinite set X can be selected a subset N on which the Peano Axioms hold.
We let f be a function on x that is injective and not surjective, i.e. x is Dedekind infinite. Since f is not surjective, we can let x0 be an element of x having no pre-image under f. Here we prove that each of the following axioms will hold with f being the successor function on a subset n, and x0 being the first element in n.
PA1: x0 e n (lines 20-27)
PA2: ALL(a):[a e n => f(a) e n] (lines 28-52)
PA3: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (lines 53-64)
PA4: ALL(a):[a e n => ~f(a)=x0] (lines 65-70)
PA5: ALL(a):[Set(a) & ALL(b):[b e a => b e n] (lines 71-97)
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
This proof cites only one axiom of set theory, namely the Subset Axiom on line 9.
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com
Dan Christensen
2021/11/17
PROOF
*****
Suppose f is a function on set x that is injective and not surjective
1 Set(x)
& ALL(a):[a e x => f(a) e x]
& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
& EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
Premise
2 Set(x)
Split, 1
f is a function on x
3 ALL(a):[a e x => f(a) e x]
Split, 1
f is injective
4 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
Split, 1
f is NOT surjective
5 EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
Split, 1
Define: x0
6 x0 e x & ALL(b):[b e x => ~f(b)=x0]
E Spec, 5
7 x0 e x
Split, 6
8 ALL(b):[b e x => ~f(b)=x0]
Split, 6
Construct n
Apply the Subset Axiom
9 EXIST(a):[Set(a) & ALL(b):[b e a <=> b e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> b e c]]]
Subset, 2
10 Set(n) & ALL(b):[b e n <=> b e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> b e c]]
E Spec, 9
Define: n
11 Set(n)
Split, 10
12 ALL(b):[b e n <=> b e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> b e c]]
Split, 10
Prove: ALL(a):[a e n => a e x]
Suppose...
13 y e n
Premise
Apply the definition of n
14 y e n <=> y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
U Spec, 12
15 [y e n => y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]]
& [y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c] => y e n]
Iff-And, 14
16 y e n => y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Split, 15
17 y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Detach, 16, 13
18 y e x
Split, 17
As Required:
n is a subset of x
19 ALL(a):[a e n => a e x]
4 Conclusion, 13
Properties of n (The Peano Axioms)
***************
Prove: x0 e n
Apply definition of n
20 x0 e n <=> x0 e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c]
U Spec, 12
21 [x0 e n => x0 e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c]]
& [x0 e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c] => x0 e n]
Iff-And, 20
Sufficient: For x0 e n
22 x0 e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c] => x0 e n
Split, 21
Prove: ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c]
Suppose...
23 Set(y)
& ALL(d):[d e y => d e x]
& x0 e y
& ALL(d):[d e y => f(d) e y]
Premise
24 x0 e y
Split, 23
As Required:
25 ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c]
4 Conclusion, 23
26 x0 e x
& ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> x0 e c]
Join, 7, 25
PA1
27 x0 e n
Detach, 22, 26
Prove: ALL(a):[aen => f(a)en]
Suppose...
28 y e n
Premise
Apply definition of n
29 y e n <=> y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
U Spec, 12
30 [y e n => y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]]
& [y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c] => y e n]
Iff-And, 29
31 y e n => y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Split, 30
32 y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Detach, 31, 28
33 y e x
Split, 32
34 ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Split, 32
35 y e x => f(y) e x
U Spec, 3
36 f(y) e x
Detach, 35, 33
Apply definition of n
37 f(y) e n <=> f(y) e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> f(y) e c]
U Spec, 12, 36
38 [f(y) e n => f(y) e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> f(y) e c]]
& [f(y) e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> f(y) e c] => f(y) e n]
Iff-And, 37
Sufficient: For f(y) e n
39 f(y) e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> f(y) e c] => f(y) e n
Split, 38
Suppose...
40 Set(z)
& ALL(d):[d e z => d e x]
& x0 e z
& ALL(d):[d e z => f(d) e z]
Premise
41 Set(z)
Split, 40
42 ALL(d):[d e z => d e x]
Split, 40
43 x0 e z
Split, 40
44 ALL(d):[d e z => f(d) e z]
Split, 40
45 y e z => f(y) e z
U Spec, 44
Apply previous result
46 Set(z)
& ALL(d):[d e z => d e x]
& x0 e z
& ALL(d):[d e z => f(d) e z]
=> y e z
U Spec, 34
47 y e z
Detach, 46, 40
48 f(y) e z
Detach, 45, 47
As Required:
49 ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> f(y) e c]
4 Conclusion, 40
50 f(y) e x
& ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> f(y) e c]
Join, 36, 49
51 f(y) e n
Detach, 39, 50
PA2
52 ALL(a):[a e n => f(a) e n]
4 Conclusion, 28
Prove: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Suppose...
53 y e n & z e n
Premise
54 y e n
Split, 53
55 z e n
Split, 53
56 ALL(b):[y e x & b e x => [f(y)=f(b) => y=b]]
U Spec, 4
57 y e x & z e x => [f(y)=f(z) => y=z]
U Spec, 56
58 y e n => y e x
U Spec, 19
59 y e x
Detach, 58, 54
60 z e n => z e x
U Spec, 19
61 z e x
Detach, 60, 55
62 y e x & z e x
Join, 59, 61
63 f(y)=f(z) => y=z
Detach, 57, 62
PA3
64 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 53
Prove: ALL(a):[aen => ~a=x0]
Suppose...
65 y e n
Premise
66 y e x => ~f(y)=x0
U Spec, 8
67 y e n => y e x
U Spec, 19
68 y e x
Detach, 67, 65
69 ~f(y)=x0
Detach, 66, 68
PA4
70 ALL(a):[a e n => ~f(a)=x0]
4 Conclusion, 65
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 p is a subset of n
71 Set(p)
& ALL(b):[b e p => b e n]
Premise
72 Set(p)
Split, 71
73 ALL(b):[b e p => b e n]
Split, 71
Prove: x0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
74 x0 e p & ALL(b):[b e p => f(b) e p]
Premise
75 x0 e p
Split, 74
76 ALL(b):[b e p => f(b) e p]
Split, 74
Prove: ALL(b):[b e n => b e p]
Suppose...
77 y e n
Premise
Apply definition of n
78 y e n <=> y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
U Spec, 12
79 [y e n => y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]]
& [y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c] => y e n]
Iff-And, 78
80 y e n => y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Split, 79
81 y e x & ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Detach, 80, 77
82 y e x
Split, 81
83 ALL(c):[Set(c)
& ALL(d):[d e c => d e x]
& x0 e c
& ALL(d):[d e c => f(d) e c]
=> y e c]
Split, 81
Sufficient: For y e p
84 Set(p)
& ALL(d):[d e p => d e x]
& x0 e p
& ALL(d):[d e p => f(d) e p]
=> y e p
U Spec, 83
Prove: ALL(d):[d e p => d e x]
Suppose...
85 z e p
Premise
86 z e p => z e n
U Spec, 73
87 z e n
Detach, 86, 85
88 z e n => z e x
U Spec, 19
89 z e x
Detach, 88, 87
As Required:
90 ALL(d):[d e p => d e x]
4 Conclusion, 85
91 Set(p) & ALL(d):[d e p => d e x]
Join, 72, 90
92 Set(p) & ALL(d):[d e p => d e x] & x0 e p
Join, 91, 75
93 Set(p) & ALL(d):[d e p => d e x] & x0 e p
& ALL(b):[b e p => f(b) e p]
Join, 92, 76
94 y e p
Detach, 84, 93
As Required:
95 ALL(b):[b e n => b e p]
4 Conclusion, 77
As Required:
96 x0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 74
PA5 (Induction)
97 ALL(a):[Set(a)
& ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 71
Joining results...
98 Set(n) & ALL(a):[a e n => a e x]
Join, 11, 19
99 Set(n) & ALL(a):[a e n => a e x] & x0 e n
Join, 98, 27
100 Set(n) & ALL(a):[a e n => a e x] & x0 e n
& ALL(a):[a e n => f(a) e n]
Join, 99, 52
101 Set(n) & ALL(a):[a e n => a e x] & x0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Join, 100, 64
102 Set(n) & ALL(a):[a e n => a e x] & x0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=x0]
Join, 101, 70
103 Set(n) & ALL(a):[a e n => a e x] & x0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Join, 102, 97
As Required:
104 ALL(x):ALL(f):[Set(x)
& ALL(a):[a e x => f(a) e x]
& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
& EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
=> EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=x0]
& ALL(a):[Set(a)
& ALL(b):[b e a => b e n]
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]]]
4 Conclusion, 1