THEOREM
*******
Let x be an infinite set. There exists a subset n of x, function f: n --> n and x0 in n such that (n,f,x0) satisfies Peano's axioms (PA1-5).
Lines
-----
13-39 Define f: x --> x
40-42 Define x0
43-46 Construct subset n of x
47-57 PA1: x0 e n
59-84 PA2: f is closed on n
93-107 PA3: f is injective on n
108-113 PA4: There is no pre-image of x0 in n under f
114-141 PA5: Induction holds on n using f as the successor function and x0 as the "first" element
142-151 Generalizing
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
DEFINITIONS
***********
Define: Infinite
1
ALL(a):[Infinite(a)
<=> EXIST(f):[ALL(b):[b e
a => f(b)
e a] & [Injective(f,a,a)
& ~Surjective(f,a,a)]]]
Axiom
Define: Injective
2
ALL(f):ALL(a):ALL(b):[Injective(f,a,b) <=> ALL(c):ALL(d):[c
e a & d
e a => [f(c)=f(d)
=> c=d]]]
Axiom
Define: Surjective
3 ALL(f):ALL(a):ALL(b):[Surjective(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
Axiom
PROOF
*****
Suppose x is an infinite set
4 Set(x) & Infinite(x)
Premise
5 Set(x)
Split, 4
6 Infinite(x)
Split, 4
Apply definition of Infinite
7
Infinite(x)
<=> EXIST(f):[ALL(b):[b e
x
=> f(b) e
x]
& [Injective(f,x,x)
& ~Surjective(f,x,x)]]
U Spec, 1
8
[Infinite(x)
=> EXIST(f):[ALL(b):[b e
x
=> f(b) e
x]
& [Injective(f,x,x)
& ~Surjective(f,x,x)]]]
& [EXIST(f):[ALL(b):[b
e x
=> f(b) e
x]
& [Injective(f,x,x)
& ~Surjective(f,x,x)]]
=> Infinite(x)]
Iff-And, 7
9
Infinite(x)
=> EXIST(f):[ALL(b):[b e
x
=> f(b) e
x]
& [Injective(f,x,x)
& ~Surjective(f,x,x)]]
Split, 8
10 EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]]
=> Infinite(x)
Split, 8
11 EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]]
Detach, 9, 6
12 ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]
E Spec, 11
13 ALL(b):[b e x => f(b) e x]
Split, 12
14 Injective(f,x,x) & ~Surjective(f,x,x)
Split, 12
15 Injective(f,x,x)
Split, 14
16 ~Surjective(f,x,x)
Split, 14
Apply definition of Injective
17 ALL(a):ALL(b):[Injective(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 2
18 ALL(b):[Injective(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
U Spec, 17
19 Injective(f,x,x) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
U Spec, 18
20 [Injective(f,x,x) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injective(f,x,x)]
Iff-And, 19
21 Injective(f,x,x) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 20
22 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injective(f,x,x)
Split, 20
f is injective
23 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Detach, 21, 15
Apply definition of Surjective
24 ALL(a):ALL(b):[Surjective(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
U Spec, 3
25 ALL(b):[Surjective(f,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & f(d)=c]]]
U Spec, 24
26 Surjective(f,x,x) <=> ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]
U Spec, 25
27 [Surjective(f,x,x) => ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]]
& [ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]] => Surjective(f,x,x)]
Iff-And, 26
28 Surjective(f,x,x) => ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]
Split, 27
29 ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]] => Surjective(f,x,x)
Split, 27
Necessary for ~Surjective
30 ~Surjective(f,x,x) => ~ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]
Contra, 29
31 ~ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]
Detach, 30, 16
32 ~~EXIST(c):~[c e x => EXIST(d):[d e x & f(d)=c]]
Quant, 31
33 EXIST(c):~[c e x => EXIST(d):[d e x & f(d)=c]]
Rem DNeg, 32
34 EXIST(c):~~[c e x & ~EXIST(d):[d e x & f(d)=c]]
Imply-And, 33
35 EXIST(c):[c e x & ~EXIST(d):[d e x & f(d)=c]]
Rem DNeg, 34
36 EXIST(c):[c e x & ~~ALL(d):~[d e x & f(d)=c]]
Quant, 35
37 EXIST(c):[c e x & ALL(d):~[d e x & f(d)=c]]
Rem DNeg, 36
38 EXIST(c):[c e x & ALL(d):~~[d e x => ~f(d)=c]]
Imply-And, 37
39 EXIST(c):[c e x & ALL(d):[d e x => ~f(d)=c]]
Rem DNeg, 38
40 x0 e x & ALL(d):[d e x => ~f(d)=x0]
E Spec, 39
Define: x0
41 x0 e x
Split, 40
42 ALL(d):[d e x => ~f(d)=x0]
Split, 40
Construct subset n of x
Apply Subset Axiom
43 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> a e b]]]
Subset, 5
44 Set(n) & ALL(a):[a e n <=> a e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> a e b]]
E Spec, 43
Define: n
45 Set(n)
Split, 44
46 ALL(a):[a e n <=> a e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> a e b]]
Split, 44
Prove: x0 e n (PA1)
Apply definition of n
47 x0 e n <=> x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b]
U Spec, 46
48 [x0 e n => x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b]]
& [x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b] => x0 e n]
Iff-And, 47
49 x0 e n => x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b]
Split, 48
Sufficient: For x0 in n
50 x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b] => x0 e n
Split, 48
51 Set(q)
& ALL(c):[c e q => c e x]
& x0 e q
& ALL(c):[c e q => f(c) e q]
Premise
52 Set(q)
Split, 51
53 ALL(c):[c e q => c e x]
Split, 51
54 x0 e q
Split, 51
55 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b]
4 Conclusion, 51
56 x0 e x
& ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> x0 e b]
Join, 41, 55
PA1
***
57 x0 e n
Detach, 50, 56
Prove: ALL(a):[a e n => f(a) e n] (PA2)
Suppose...
58 t e n
Premise
Apply definition of n
59 t e n <=> t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
U Spec, 46
60 [t e n => t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]]
& [t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b] => t e n]
Iff-And, 59
61 t e n => t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Split, 60
62 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b] => t e n
Split, 60
63 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Detach, 61, 58
64 t e x
Split, 63
65 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Split, 63
Apply definition n
66 f(t) e n <=> f(t) e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b]
U Spec, 46
67 [f(t) e n => f(t) e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b]]
& [f(t) e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b] => f(t) e n]
Iff-And, 66
68 f(t) e n => f(t) e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b]
Split, 67
Sufficient: For f(t) e n
69 f(t) e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b] => f(t) e n
Split, 67
Apply previous result
70 t e x => f(t) e x
U Spec, 13
71 f(t) e x
Detach, 70, 64
Prove: ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b]
Suppose...
72 Set(q)
& ALL(c):[c e q => c e x]
& x0 e q
& ALL(c):[c e q => f(c) e q]
Premise
73 Set(q)
Split, 72
74 ALL(c):[c e q => c e x]
Split, 72
75 x0 e q
Split, 72
76 ALL(c):[c e q => f(c) e q]
Split, 72
77 t e q => f(t) e q
U Spec, 76
Apply previous result
78 Set(q)
& ALL(c):[c e q => c e x]
& x0 e q
& ALL(c):[c e q => f(c) e q]
=> t e q
U Spec, 65
79 t e q
Detach, 78, 72
80 f(t) e q
Detach, 77, 79
As Required:
81 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b]
4 Conclusion, 72
82 f(t) e x
& ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> f(t) e b]
Join, 71, 81
83 f(t) e n
Detach, 69, 82
PA2 f is closed on n
***
84 ALL(a):[a e n => f(a) e n]
4 Conclusion, 58
Prove: n is a subset of x
Suppose...
85 t e n
Premise
86 t e n <=> t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
U Spec, 46
87 [t e n => t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]]
& [t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b] => t e n]
Iff-And, 86
88 t e n => t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Split, 87
89 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b] => t e n
Split, 87
90 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Detach, 88, 85
91 t e x
Split, 90
As Required:
n is a subset of x
92 ALL(a):[a e n => a e x]
4 Conclusion, 85
Prove: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (PA3)
Suppose...
93 t e n & u e n
Premise
94 t e n
Split, 93
95 u e n
Split, 93
Prove: f(t)=f(u) => t=u
Suppose...
96 f(t)=f(u)
Premise
Apply previous result
97 ALL(d):[t e x & d e x => [f(t)=f(d) => t=d]]
U Spec, 23
98 t e x & u e x => [f(t)=f(u) => t=u]
U Spec, 97
99 t e n => t e x
U Spec, 92
100 t e x
Detach, 99, 94
101 u e n => u e x
U Spec, 92
102 u e x
Detach, 101, 95
103 t e x & u e x
Join, 100, 102
104 f(t)=f(u) => t=u
Detach, 98, 103
105 t=u
Detach, 104, 96
As Required:
106 f(t)=f(u) => t=u
4 Conclusion, 96
PA3 f is injective on n
***
107 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 93
Prove: ALL(a):[a e n => ~f(a)=x0] (PA4)
Suppose...
108 t e n
Premise
109 t e x => ~f(t)=x0
U Spec, 42
110 t e n => t e x
U Spec, 92
111 t e x
Detach, 110, 108
112 ~f(t)=x0
Detach, 109, 111
PA4 x0 has no pre-image in n under f
***
113 ALL(a):[a e n => ~f(a)=x0]
4 Conclusion, 108
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n] (PA5)
=> [x0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
114 Set(p) & ALL(b):[b e p => b e n]
Premise
115 Set(p)
Split, 114
116 ALL(b):[b e p => b e n]
Split, 114
Prove: x0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
117 x0 e p & ALL(b):[b e p => f(b) e p]
Premise
118 x0 e p
Split, 117
119 ALL(b):[b e p => f(b) e p]
Split, 117
Prove: ALL(b):[b e n => b e p]
Suppose...
120 t e n
Premise
Apply definition of n
121 t e n <=> t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
U Spec, 46
122 [t e n => t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]]
& [t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b] => t e n]
Iff-And, 121
123 t e n => t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Split, 122
124 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b] => t e n
Split, 122
125 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Detach, 123, 120
126 t e x
Split, 125
127 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& x0 e b
& ALL(c):[c e b => f(c) e b]
=> t e b]
Split, 125
Sufficient: For t e p
128 Set(p)
& ALL(c):[c e p => c e x]
& x0 e p
& ALL(c):[c e p => f(c) e p]
=> t e p
U Spec, 127
Prove: ALL(c):[c e p => c e x]
Suppose...
129 u e p
Premise
130 u e p => u e n
U Spec, 116
131 u e n
Detach, 130, 129
132 u e n => u e x
U Spec, 92
133 u e x
Detach, 132, 131
As Required:
134 ALL(c):[c e p => c e x]
4 Conclusion, 129
135 Set(p) & ALL(c):[c e p => c e x]
Join, 115, 134
136 Set(p) & ALL(c):[c e p => c e x] & x0 e p
Join, 135, 118
137 Set(p) & ALL(c):[c e p => c e x] & x0 e p
& ALL(b):[b e p => f(b) e p]
Join, 136, 119
138 t e p
Detach, 128, 137
As Required:
139 ALL(b):[b e n => b e p]
4 Conclusion, 120
As Required:
140 x0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 117
PA5 Induction holds on n with successor function f and "first" element x0
***
141 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, 114
Joining previous results...
142 Set(n) & ALL(a):[a e n => a e x]
Join, 45, 92
143 Set(n) & ALL(a):[a e n => a e x] & x0 e n
Join, 142, 57
144 Set(n) & ALL(a):[a e n => a e x] & x0 e n
& ALL(a):[a e n => f(a) e n]
Join, 143, 84
145 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, 144, 107
146 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, 145, 113
147 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, 146, 141
148 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]]]]
E Gen, 147
149 EXIST(f):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]]]]
E Gen, 148
150 EXIST(n):EXIST(f):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]]]]
E Gen, 149
As Required:
151 ALL(x):[Set(x) & Infinite(x)
=> EXIST(n):EXIST(f):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, 4