Constructing the Natural Numbers from the Reals
From the field, order and completeness axioms for the real numbers, we show here that there
exists a unique subset n such that:
1 
n
ALL(a):[a n => a+1 n]
ALL(a):[a n => ~a+1=1]
ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
ALL(a):[Set(a) & 1 a & ALL(b):[b n & b a => b+1 a]
=> ALL(b):[b n => b a]
These properties correspond to Peano's Axioms for the natural numbers.
The Archimedean Axiom for the reals is then defined in terms of this set n.
Field Axioms
************
1 Set(real)
& ALL(a):ALL(b):[a real & b real => a+b real]
& ALL(a):ALL(b):ALL(c):[a real & b real & c real => a+b+c=a+(b+c)]
& ALL(a):ALL(b):[a real & b real => a+b=b+a]
& 0 real
& ALL(a):[a real => a+0=a]
& ALL(a):[a real => _a real]
& ALL(a):[a real => a+_a=0]
& ALL(a):ALL(b):[a real & b real => a*b real]
& ALL(a):ALL(b):ALL(c):[a real & b real & c real => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a real & b real => a*b=b*a]
& ALL(a):ALL(b):ALL(c):[a real & b real & c real => a*(b+c)=a*b+a*c]
& 1 real
& ~0=1
& ALL(a):[a real => a*1=a]
& ALL(a):[a real & ~a=0 => 1/a real]
& ALL(a):[a real => a*(1/a)=1]
Premise
Splitting into individual axioms...
Define: real, the set of real numbers
2 Set(real)
Split, 1
Define: + operator
3 ALL(a):ALL(b):[a real & b real => a+b real]
Split, 1
+ is associative
4 ALL(a):ALL(b):ALL(c):[a real & b real & c real => a+b+c=a+(b+c)]
Split, 1
+ is commutative
5 ALL(a):ALL(b):[a real & b real => a+b=b+a]
Split, 1
Define: 0
6 0 real
Split, 1
7 ALL(a):[a real => a+0=a]
Split, 1
Define: _x (additive invervse)
8 ALL(a):[a real => _a real]
Split, 1
9 ALL(a):[a real => a+_a=0]
Split, 1
Define: * operator
10 ALL(a):ALL(b):[a real & b real => a*b real]
Split, 1
* is associative
11 ALL(a):ALL(b):ALL(c):[a real & b real & c real => a*b*c=a*(b*c)]
Split, 1
* is commutative
12 ALL(a):ALL(b):[a real & b real => a*b=b*a]
Split, 1
* is distributive over +
13 ALL(a):ALL(b):ALL(c):[a real & b real & c real => a*(b+c)=a*b+a*c]
Split, 1
Define: 1
14 1 real
Split, 1
15 ~0=1
Split, 1
16 ALL(a):[a real => a*1=a]
Split, 1
Define: 1/x (multiplicative inverse)
17 ALL(a):[a real & ~a=0 => 1/a real]
Split, 1
18 ALL(a):[a real => a*(1/a)=1]
Split, 1
Order Axioms
************
19 Set(pos)
& ALL(a):[a pos => a real]
& ALL(a):[a real
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
& ALL(a):ALL(b):[a real & b real & a pos & b pos => a+b pos]
& ALL(a):ALL(b):[a real & b real & a pos & b pos => a*b pos]
& ALL(a):ALL(b):[a real & b real => [a<b <=> b+_a pos]]
& ALL(a):ALL(b):[a real & b real => [a<=b <=> a<b | a=b]]
Premise
Splitting into individual axioms...
Define: pos, the set of postive elements of the set real
20 Set(pos)
Split, 19
pos is a subset of real
21 ALL(a):[a pos => a real]
Split, 19
The Trichotomy Rule
22 ALL(a):[a real
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
Split, 19
Adding postive elements
23 ALL(a):ALL(b):[a real & b real & a pos & b pos => a+b pos]
Split, 19
Mulitplying postive elements
24 ALL(a):ALL(b):[a real & b real & a pos & b pos => a*b pos]
Split, 19
Define: < relation
25 ALL(a):ALL(b):[a real & b real => [a<b <=> b+_a pos]]
Split, 19
Define: <= relation
26 ALL(a):ALL(b):[a real & b real => [a<=b <=> a<b | a=b]]
Split, 19
Completeness Axiom
******************
27 ALL(a):[Set(a)
& ALL(b):[b a => b real]
& EXIST(b):b a
& EXIST(b):[b real & ALL(c):[c a => c<=b]]
=> EXIST(b):[b a & ALL(c):[c a => c<=b]]]
Premise
Constructing n
**************
Applying the subset axiom...
28 EXIST(n):[Set(n) & ALL(a):[a n <=> a real & [0<a & [a=1 | EXIST(b):[b n & b+1=a]]]]]
Subset, 2
Previously established results
******************************
Lemma 1
29 0<1
Premise
Lemma 2 Additivity of >
30 ALL(a):ALL(b):ALL(c):[a real & b real & c real & a<b => a+c<b+c]
Premise
Lemma 3 Transitivity of <
31 ALL(a):ALL(b):ALL(c):[a real & b real & c real & a<b & b<c => a<c]
Premise
Lemma 4 Right cancellation, and adding same to both sides
32 ALL(a):ALL(b):ALL(c):[a real & b real & c real => [a=b <=> a+c=b+c]]
Premise
Lemma 5
33 _1 real
Premise
Lemma 6
34 _0=0
Premise
Lemma 7 Greatest Lower Bound
35 ALL(a):[Set(a)
& ALL(b):[b a => b real]
& EXIST(b):b a
& EXIST(b):[b real & ALL(c):[c a => b<=c]]
=> EXIST(b):[b a & ALL(c):[c a => b<=c]]]
Premise
Lemma 8 x+1=y => x<y
36 ALL(a):ALL(b):[a real & b real & a+1=b => a<b]
Premise
Lemma 9 x<=y <=> ~y<x
37 ALL(a):ALL(b):[a real & b real => [a<=b <=> ~b<a]]
Premise
Define: n, a subset of real
38 Set(n) & ALL(a):[a n <=> a real & [0<a & [a=1 | EXIST(b):[b n & b+1=a]]]]
E Spec, 28
39 Set(n)
Split, 38
40 ALL(a):[a n <=> a real & [0<a & [a=1 | EXIST(b):[b n & b+1=a]]]]
Split, 38
Prove: 1n
Applying the defintion of n...
41 1 n <=> 1 real & [0<1 & [1=1 | EXIST(b):[b n & b+1=1]]]
U Spec, 40
42 [1 n => 1 real & [0<1 & [1=1 | EXIST(b):[b n & b+1=1]]]]
& [1 real & [0<1 & [1=1 | EXIST(b):[b n & b+1=1]]] => 1 n]
Iff-And, 41
43 1 n => 1 real & [0<1 & [1=1 | EXIST(b):[b n & b+1=1]]]
Split, 42
Sufficient: For 1n
44 1 real & [0<1 & [1=1 | EXIST(b):[b n & b+1=1]]] => 1 n
Split, 42
45 1=1
Reflex
46 1=1 | EXIST(b):[b n & b+1=1]
Arb Or, 45
47 0<1 & [1=1 | EXIST(b):[b n & b+1=1]]
Join, 29, 46
48 1 real & [0<1 & [1=1 | EXIST(b):[b n & b+1=1]]]
Join, 14, 47
As Required:
49 1 n
Detach, 44, 48
Prove: xn => x+1n
Suppose...
50 x n
Premise
Applying defintion of n...
51 x n <=> x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
U Spec, 40
52 [x n => x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]]
& [x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]] => x n]
Iff-And, 51
53 x n => x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
Split, 52
54 x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]] => x n
Split, 52
55 x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
Detach, 53, 50
56 x real
Split, 55
57 0<x & [x=1 | EXIST(b):[b n & b+1=x]]
Split, 55
58 0<x
Split, 57
59 x=1 | EXIST(b):[b n & b+1=x]
Split, 57
Applying defintion of n...
60 x+1 n <=> x+1 real & [0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]]
U Spec, 40
61 [x+1 n => x+1 real & [0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]]]
& [x+1 real & [0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]] => x+1 n]
Iff-And, 60
62 x+1 n => x+1 real & [0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]]
Split, 61
Sufficient: For x+1n
63 x+1 real & [0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]] => x+1 n
Split, 61
Prove: x+1real
Applying defintion of n...
64 ALL(b):[x real & b real => x+b real]
U Spec, 3
65 x real & 1 real => x+1 real
U Spec, 64
66 x real & 1 real
Join, 56, 14
67 x+1 real
Detach, 65, 66
Prove: 0<x+1
Applying Lemma 2...
68 ALL(b):ALL(c):[0 real & b real & c real & 0<b => 0+c<b+c]
U Spec, 30
69 ALL(c):[0 real & 1 real & c real & 0<1 => 0+c<1+c]
U Spec, 68
70 0 real & 1 real & x real & 0<1 => 0+x<1+x
U Spec, 69
71 0 real & 1 real
Join, 6, 14
72 0 real & 1 real & x real
Join, 71, 56
73 0 real & 1 real & x real & 0<1
Join, 72, 29
74 0+x<1+x
Detach, 70, 73
Applying commutativity of +...
75 ALL(b):[0 real & b real => 0+b=b+0]
U Spec, 5
76 0 real & x real => 0+x=x+0
U Spec, 75
77 0 real & x real
Join, 6, 56
78 0+x=x+0
Detach, 76, 77
79 x+0<1+x
Substitute, 78, 74
80 x real => x+0=x
U Spec, 7
81 x+0=x
Detach, 80, 56
82 x<1+x
Substitute, 81, 79
Applying commutativity of +...
83 ALL(b):[1 real & b real => 1+b=b+1]
U Spec, 5
84 1 real & x real => 1+x=x+1
U Spec, 83
85 1 real & x real
Join, 14, 56
86 1+x=x+1
Detach, 84, 85
87 x<x+1
Substitute, 86, 82
Prove: 0<x+1
Applying transitivity of <...
88 ALL(b):ALL(c):[0 real & b real & c real & 0<b & b<c => 0<c]
U Spec, 31
89 ALL(c):[0 real & x real & c real & 0<x & x<c => 0<c]
U Spec, 88
Sufficient: For 0<x+1
90 0 real & x real & x+1 real & 0<x & x<x+1 => 0<x+1
U Spec, 89
Prove: x+1 real
Applying the definition of +...
91 ALL(b):[x real & b real => x+b real]
U Spec, 3
92 x real & 1 real => x+1 real
U Spec, 91
93 x real & 1 real
Join, 56, 14
94 x+1 real
Detach, 92, 93
95 0 real & x real
Join, 6, 56
96 0 real & x real & x+1 real
Join, 95, 94
97 0 real & x real & x+1 real & 0<x
Join, 96, 58
98 0 real & x real & x+1 real & 0<x & x<x+1
Join, 97, 87
99 0<x+1
Detach, 90, 98
100 x+1=x+1
Reflex
101 x n & x+1=x+1
Join, 50, 100
102 EXIST(b):[b n & b+1=x+1]
E Gen, 101
103 x+1=1 | EXIST(b):[b n & b+1=x+1]
Arb Or, 102
104 0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]
Join, 99, 103
105 x+1 real
& [0<x+1 & [x+1=1 | EXIST(b):[b n & b+1=x+1]]]
Join, 67, 104
106 x+1 n
Detach, 63, 105
As Required:
107 x n => x+1 n
Conclusion, 50
As Required:
108 ALL(a):[a n => a+1 n]
U Gen, 107
Prove: xn => ~x+1=1
Suppose...
109 x n
Premise
Applying the definition of n...
110 x n <=> x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
U Spec, 40
111 [x n => x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]]
& [x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]] => x n]
Iff-And, 110
112 x n => x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
Split, 111
113 x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]] => x n
Split, 111
114 x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
Detach, 112, 109
115 x real
Split, 114
116 0<x & [x=1 | EXIST(b):[b n & b+1=x]]
Split, 114
117 0<x
Split, 116
118 x=1 | EXIST(b):[b n & b+1=x]
Split, 116
Suppose to the contrary...
119 x+1=1
Premise
Prove: x=0
Adding _1 to both sides...
120 ALL(b):ALL(c):[x+1 real & b real & c real => [x+1=b <=> x+1+c=b+c]]
U Spec, 32
121 ALL(c):[x+1 real & 1 real & c real => [x+1=1 <=> x+1+c=1+c]]
U Spec, 120
122 x+1 real & 1 real & _1 real => [x+1=1 <=> x+1+_1=1+_1]
U Spec, 121
Prove: x+1 real
Applying the defintion of +...
123 ALL(b):[x real & b real => x+b real]
U Spec, 3
124 x real & 1 real => x+1 real
U Spec, 123
125 x real & 1 real
Join, 115, 14
126 x+1 real
Detach, 124, 125
127 x+1 real & 1 real
Join, 126, 14
128 x+1 real & 1 real & _1 real
Join, 127, 33
129 x+1=1 <=> x+1+_1=1+_1
Detach, 122, 128
130 [x+1=1 => x+1+_1=1+_1] & [x+1+_1=1+_1 => x+1=1]
Iff-And, 129
131 x+1=1 => x+1+_1=1+_1
Split, 130
132 x+1+_1=1+_1 => x+1=1
Split, 130
133 x+1+_1=1+_1
Detach, 131, 119
Applying associativity of +...
134 ALL(b):ALL(c):[x real & b real & c real => x+b+c=x+(b+c)]
U Spec, 4
135 ALL(c):[x real & 1 real & c real => x+1+c=x+(1+c)]
U Spec, 134
136 x real & 1 real & _1 real => x+1+_1=x+(1+_1)
U Spec, 135
137 x real & 1 real
Join, 115, 14
138 x real & 1 real & _1 real
Join, 137, 33
139 x+1+_1=x+(1+_1)
Detach, 136, 138
140 x+(1+_1)=1+_1
Substitute, 139, 133
Applying definition of _ operator...
141 1 real => 1+_1=0
U Spec, 9
142 1+_1=0
Detach, 141, 14
143 x+0=0
Substitute, 142, 140
Applying defintion of 0...
144 x real => x+0=x
U Spec, 7
145 x+0=x
Detach, 144, 115
146 x=0
Substitute, 145, 143
147 0<0
Substitute, 146, 117
Applying definition of <...
148 ALL(b):[0 real & b real => [0<b <=> b+_0 pos]]
U Spec, 25
149 0 real & 0 real => [0<0 <=> 0+_0 pos]
U Spec, 148
150 0 real & 0 real
Join, 6, 6
151 0<0 <=> 0+_0 pos
Detach, 149, 150
152 [0<0 => 0+_0 pos] & [0+_0 pos => 0<0]
Iff-And, 151
153 0<0 => 0+_0 pos
Split, 152
154 0+_0 pos => 0<0
Split, 152
155 0+_0 pos
Detach, 153, 147
156 0+0 pos
Substitute, 34, 155
Applying defintion of 0...
157 0 real => 0+0=0
U Spec, 7
158 0+0=0
Detach, 157, 6
159 0 pos
Substitute, 158, 156
Applying Trichotomy Rule...
160 0 real
=> [0=0 | 0 pos | _0 pos]
& ~[0=0 & 0 pos]
& ~[0=0 & _0 pos]
& ~[0 pos & _0 pos]
U Spec, 22
161 [0=0 | 0 pos | _0 pos]
& ~[0=0 & 0 pos]
& ~[0=0 & _0 pos]
& ~[0 pos & _0 pos]
Detach, 160, 6
162 0=0 | 0 pos | _0 pos
Split, 161
163 ~[0=0 & 0 pos]
Split, 161
164 ~[0=0 & _0 pos]
Split, 161
165 ~[0 pos & _0 pos]
Split, 161
166 0=0
Reflex
167 0=0 & 0 pos
Join, 166, 159
168 0=0 & 0 pos & ~[0=0 & 0 pos]
Join, 167, 163
As Required:
By contradiction...
169 ~x+1=1
Conclusion, 119
As Required:
170 x n => ~x+1=1
Conclusion, 109
As Required:
171 ALL(a):[a n => ~a+1=1]
U Gen, 170
Prove: x n & y n & x+1=y+1 => x=y
Suppose...
172 x n & y n & x+1=y+1
Premise
173 x n
Split, 172
174 y n
Split, 172
175 x+1=y+1
Split, 172
176 x n <=> x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
U Spec, 40
177 [x n => x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]]
& [x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]] => x n]
Iff-And, 176
178 x n => x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
Split, 177
179 x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]] => x n
Split, 177
180 x real & [0<x & [x=1 | EXIST(b):[b n & b+1=x]]]
Detach, 178, 173
181 x real
Split, 180
182 0<x & [x=1 | EXIST(b):[b n & b+1=x]]
Split, 180
183 y n <=> y real & [0<y & [y=1 | EXIST(b):[b n & b+1=y]]]
U Spec, 40
184 [y n => y real & [0<y & [y=1 | EXIST(b):[b n & b+1=y]]]]
& [y real & [0<y & [y=1 | EXIST(b):[b n & b+1=y]]] => y n]
Iff-And, 183
185 y n => y real & [0<y & [y=1 | EXIST(b):[b n & b+1=y]]]
Split, 184
186 y real & [0<y & [y=1 | EXIST(b):[b n & b+1=y]]] => y n
Split, 184
187 y real & [0<y & [y=1 | EXIST(b):[b n & b+1=y]]]
Detach, 185, 174
188 y real
Split, 187
189 0<y & [y=1 | EXIST(b):[b n & b+1=y]]
Split, 187
Applying right cancellation...
190 ALL(b):ALL(c):[x real & b real & c real => [x=b <=> x+c=b+c]]
U Spec, 32
191 ALL(c):[x real & y real & c real => [x=y <=> x+c=y+c]]
U Spec, 190
192 x real & y real & 1 real => [x=y <=> x+1=y+1]
U Spec, 191
193 x real & y real
Join, 181, 188
194 x real & y real & 1 real
Join, 193, 14
195 x=y <=> x+1=y+1
Detach, 192, 194
196 [x=y => x+1=y+1] & [x+1=y+1 => x=y]
Iff-And, 195
197 x=y => x+1=y+1
Split, 196
198 x+1=y+1 => x=y
Split, 196
199 x=y
Detach, 198, 175
As Required:
200 x n & y n & x+1=y+1 => x=y
Conclusion, 172
201 ALL(b):[x n & b n & x+1=b+1 => x=b]
U Gen, 200
As Required:
202 ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
U Gen, 201
Prove: Set(s) & 1 s & ALL(b):[b n & b s => b+1 s]
=> ALL(b):[b n => b s]
Suppose...
203 Set(s) & 1 s & ALL(b):[b n & b s => b+1 s]
Premise
204 Set(s)
Split, 203
205 1 s
Split, 203
206 ALL(b):[b n & b s => b+1 s]
Split, 203
Suppose to the contrary...
207 ~ALL(b):[b n => b s]
Premise
208 ~~EXIST(b):~[b n => b s]
Quant, 207
209 EXIST(b):~[b n => b s]
Rem DNeg, 208
210 EXIST(b):~~[b n & ~b s]
Imply-And, 209
211 EXIST(b):[b n & ~b s]
Rem DNeg, 210
Define: p, an element of n that is not in s
212 p n & ~p s
E Spec, 211
213 p n
Split, 212
214 ~p s
Split, 212
Applying the defintion of n...
215 p n <=> p real & [0<p & [p=1 | EXIST(b):[b n & b+1=p]]]
U Spec, 40
216 [p n => p real & [0<p & [p=1 | EXIST(b):[b n & b+1=p]]]]
& [p real & [0<p & [p=1 | EXIST(b):[b n & b+1=p]]] => p n]
Iff-And, 215
217 p n => p real & [0<p & [p=1 | EXIST(b):[b n & b+1=p]]]
Split, 216
218 p real & [0<p & [p=1 | EXIST(b):[b n & b+1=p]]] => p n
Split, 216
219 p real & [0<p & [p=1 | EXIST(b):[b n & b+1=p]]]
Detach, 217, 213
220 p real
Split, 219
221 0<p & [p=1 | EXIST(b):[b n & b+1=p]]
Split, 219
222 0<p
Split, 221
223 p=1 | EXIST(b):[b n & b+1=p]
Split, 221
Construct t
Applying the subset axiom...
224 EXIST(t):[Set(t) & ALL(a):[a t <=> a n & ~a s]]
Subset, 39
Define: t, the subset of n not in s
225 Set(t) & ALL(a):[a t <=> a n & ~a s]
E Spec, 224
226 Set(t)
Split, 225
227 ALL(a):[a t <=> a n & ~a s]
Split, 225
Applying the Greatest Lower Bound lemma...
228 Set(t)
& ALL(b):[b t => b real]
& EXIST(b):b t
& EXIST(b):[b real & ALL(c):[c t => b<=c]]
=> EXIST(b):[b t & ALL(c):[c t => b<=c]]
U Spec, 35
Prove: u t => u real
Suppose...
229 u t
Premise
230 u t <=> u n & ~u s
U Spec, 227
231 [u t => u n & ~u s] & [u n & ~u s => u t]
Iff-And, 230
232 u t => u n & ~u s
Split, 231
233 u n & ~u s => u t
Split, 231
234 u n & ~u s
Detach, 232, 229
235 u n
Split, 234
236 ~u s
Split, 234
Applying the definition of n...
237 u n <=> u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]
U Spec, 40
238 [u n => u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]]
& [u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]] => u n]
Iff-And, 237
239 u n => u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]
Split, 238
240 u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]] => u n
Split, 238
241 u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]
Detach, 239, 235
242 u real
Split, 241
As Required:
243 u t => u real
Conclusion, 229
As Required:
244 ALL(b):[b t => b real]
U Gen, 243
Prove: EXIST(b):bt
Applying the defintion of t...
245 p t <=> p n & ~p s
U Spec, 227
246 [p t => p n & ~p s] & [p n & ~p s => p t]
Iff-And, 245
247 p t => p n & ~p s
Split, 246
248 p n & ~p s => p t
Split, 246
249 p t
Detach, 248, 212
As Required:
250 EXIST(b):b t
E Gen, 249
Prove: ut => 0<=u
Suppose...
251 u t
Premise
Applying the definition of t...
252 u t <=> u n & ~u s
U Spec, 227
253 [u t => u n & ~u s] & [u n & ~u s => u t]
Iff-And, 252
254 u t => u n & ~u s
Split, 253
255 u n & ~u s => u t
Split, 253
256 u n & ~u s
Detach, 254, 251
257 u n
Split, 256
258 ~u s
Split, 256
Applying the definition of u...
259 u n <=> u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]
U Spec, 40
260 [u n => u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]]
& [u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]] => u n]
Iff-And, 259
261 u n => u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]
Split, 260
262 u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]] => u n
Split, 260
263 u real & [0<u & [u=1 | EXIST(b):[b n & b+1=u]]]
Detach, 261, 257
264 u real
Split, 263
265 0<u & [u=1 | EXIST(b):[b n & b+1=u]]
Split, 263
266 0<u
Split, 265
267 u=1 | EXIST(b):[b n & b+1=u]
Split, 265
Prove: 0<=u
Applying the definition of <=...
268 ALL(b):[0 real & b real => [0<=b <=> 0<b | 0=b]]
U Spec, 26
269 0 real & u real => [0<=u <=> 0<u | 0=u]
U Spec, 268
270 0 real & u real
Join, 6, 264
271 0<=u <=> 0<u | 0=u
Detach, 269, 270
272 [0<=u => 0<u | 0=u] & [0<u | 0=u => 0<=u]
Iff-And, 271
273 0<=u => 0<u | 0=u
Split, 272
274 0<u | 0=u => 0<=u
Split, 272
275 0<u | 0=u
Arb Or, 266
As Required:
276 0<=u
Detach, 274, 275
As Required:
277 u t => 0<=u
Conclusion, 251
278 ALL(c):[c t => 0<=c]
U Gen, 277
279 0 real & ALL(c):[c t => 0<=c]
Join, 6, 278
As Required:
280 EXIST(b):[b real & ALL(c):[c t => b<=c]]
E Gen, 279
281 Set(t) & ALL(b):[b t => b real]
Join, 226, 244
282 Set(t) & ALL(b):[b t => b real]
& EXIST(b):b t
Join, 281, 250
283 Set(t) & ALL(b):[b t => b real]
& EXIST(b):b t
& EXIST(b):[b real & ALL(c):[c t => b<=c]]
Join, 282, 280
284 EXIST(b):[b t & ALL(c):[c t => b<=c]]
Detach, 228, 283
Define: glbt, the greatest lower bound of t
285 glbt t & ALL(c):[c t => glbt<=c]
E Spec, 284
286 glbt t
Split, 285
287 ALL(c):[c t => glbt<=c]
Split, 285
Applying the defintion of t...
288 glbt t <=> glbt n & ~glbt s
U Spec, 227
289 [glbt t => glbt n & ~glbt s]
& [glbt n & ~glbt s => glbt t]
Iff-And, 288
290 glbt t => glbt n & ~glbt s
Split, 289
291 glbt n & ~glbt s => glbt t
Split, 289
292 glbt n & ~glbt s
Detach, 290, 286
293 glbt n
Split, 292
294 ~glbt s
Split, 292
Applying the definition of n...
295 glbt n <=> glbt real & [0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]]
U Spec, 40
296 [glbt n => glbt real & [0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]]]
& [glbt real & [0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]] => glbt n]
Iff-And, 295
297 glbt n => glbt real & [0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]]
Split, 296
298 glbt real & [0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]] => glbt n
Split, 296
299 glbt real & [0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]]
Detach, 297, 293
300 glbt real
Split, 299
301 0<glbt & [glbt=1 | EXIST(b):[b n & b+1=glbt]]
Split, 299
302 0<glbt
Split, 301
303 glbt=1 | EXIST(b):[b n & b+1=glbt]
Split, 301
Prove: ~glbt=1
Suppose to the contrary...
304 glbt=1
Premise
305 ~1 s
Substitute, 304, 294
306 1 s & ~1 s
Join, 205, 305
As Required:
By contradiction...
307 ~glbt=1
Conclusion, 304
308 ~glbt=1 => EXIST(b):[b n & b+1=glbt]
Imply-Or, 303
309 EXIST(b):[b n & b+1=glbt]
Detach, 308, 307
Define: preglbt, the predecessor of glbt
310 preglbt n & preglbt+1=glbt
E Spec, 309
311 preglbt n
Split, 310
312 preglbt+1=glbt
Split, 310
Applying the definition of n...
313 preglbt n <=> preglbt real & [0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]]
U Spec, 40
314 [preglbt n => preglbt real & [0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]]]
& [preglbt real & [0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]] => preglbt n]
Iff-And, 313
315 preglbt n => preglbt real & [0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]]
Split, 314
316 preglbt real & [0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]] => preglbt n
Split, 314
317 preglbt real & [0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]]
Detach, 315, 311
318 preglbt real
Split, 317
319 0<preglbt & [preglbt=1 | EXIST(b):[b n & b+1=preglbt]]
Split, 317
320 0<preglbt
Split, 319
321 preglbt=1 | EXIST(b):[b n & b+1=preglbt]
Split, 319
Applying defintion of s...
322 preglbt n & preglbt s => preglbt+1 s
U Spec, 206
Substituting...
323 preglbt n & preglbt s => glbt s
Substitute, 312, 322
Applying the defintion of <...
324 ALL(b):[preglbt real & b real => [preglbt<b <=> b+_preglbt pos]]
U Spec, 25
before lemma in Reals3
325 preglbt real & glbt real => [preglbt<glbt <=> glbt+_preglbt pos]
U Spec, 324
326 preglbt real & glbt real
Join, 318, 300
327 preglbt<glbt <=> glbt+_preglbt pos
Detach, 325, 326
328 [preglbt<glbt => glbt+_preglbt pos]
& [glbt+_preglbt pos => preglbt<glbt]
Iff-And, 327
329 preglbt<glbt => glbt+_preglbt pos
Split, 328
330 glbt+_preglbt pos => preglbt<glbt
Split, 328
Applying Lemma 8...
331 ALL(b):[preglbt real & b real & preglbt+1=b => preglbt<b]
U Spec, 36
332 preglbt real & glbt real & preglbt+1=glbt => preglbt<glbt
U Spec, 331
333 preglbt real & glbt real & preglbt+1=glbt
Join, 326, 312
334 preglbt<glbt
Detach, 332, 333
Applying the defintion of glbt...
335 preglbt t => glbt<=preglbt
U Spec, 287
336 ~glbt<=preglbt => ~preglbt t
Contra, 335
337 ALL(b):[glbt real & b real => [glbt<=b <=> ~b<glbt]]
U Spec, 37
338 glbt real & preglbt real => [glbt<=preglbt <=> ~preglbt<glbt]
U Spec, 337
339 glbt real & preglbt real
Join, 300, 318
340 glbt<=preglbt <=> ~preglbt<glbt
Detach, 338, 339
341 [glbt<=preglbt => ~preglbt<glbt]
& [~preglbt<glbt => glbt<=preglbt]
Iff-And, 340
342 glbt<=preglbt => ~preglbt<glbt
Split, 341
343 ~preglbt<glbt => glbt<=preglbt
Split, 341
344 ~~preglbt<glbt => ~glbt<=preglbt
Contra, 342
345 preglbt<glbt => ~glbt<=preglbt
Rem DNeg, 344
346 ~glbt<=preglbt
Detach, 345, 334
347 ~preglbt t
Detach, 336, 346
Applying the definition of t...
348 preglbt t <=> preglbt n & ~preglbt s
U Spec, 227
349 [preglbt t => preglbt n & ~preglbt s]
& [preglbt n & ~preglbt s => preglbt t]
Iff-And, 348
350 preglbt t => preglbt n & ~preglbt s
Split, 349
351 preglbt n & ~preglbt s => preglbt t
Split, 349
352 ~preglbt t => ~[preglbt n & ~preglbt s]
Contra, 351
353 ~[preglbt n & ~preglbt s]
Detach, 352, 347
354 ~~[preglbt n => ~~preglbt s]
Imply-And, 353
355 preglbt n => ~~preglbt s
Rem DNeg, 354
356 preglbt n => preglbt s
Rem DNeg, 355
357 preglbt s
Detach, 356, 311
358 preglbt n & preglbt s
Join, 311, 357
359 glbt s
Detach, 323, 358
360 glbt s & ~glbt s
Join, 359, 294
As Required:
361 ~~ALL(b):[b n => b s]
Conclusion, 207
362 ALL(b):[b n => b s]
Rem DNeg, 361
363 Set(s) & 1 s & ALL(b):[b n & b s => b+1 s]
=> ALL(b):[b n => b s]
Conclusion, 203
As Required:
The principle of mathmatical induction...
364 ALL(a):[Set(a) & 1 a & ALL(b):[b n & b a => b+1 a]
=> ALL(b):[b n => b a]]
U Gen, 363
365 Set(n) & 1 n
Join, 39, 49
366 Set(n) & 1 n & ALL(a):[a n => a+1 n]
Join, 365, 108
367 Set(n) & 1 n & ALL(a):[a n => a+1 n]
& ALL(a):[a n => ~a+1=1]
Join, 366, 171
368 Set(n) & 1 n & ALL(a):[a n => a+1 n]
& ALL(a):[a n => ~a+1=1]
& ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
Join, 367, 202
As Required:
We have the following properties corresponding to Peano's Axioms...
369 Set(n) & 1 n & ALL(a):[a n => a+1 n]
& ALL(a):[a n => ~a+1=1]
& ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
& ALL(a):[Set(a) & 1 a & ALL(b):[b n & b a => b+1 a]
=> ALL(b):[b n => b a]]
Join, 368, 364
Prove: n is unique.
Suppose we also have n' such that...
370 Set(n')
& 1 n' & ALL(a):[a n' => a+1 n']
& ALL(a):[a n' => ~a+1=1]
& ALL(a):ALL(b):[a n' & b n' & a+1=b+1 => a=b]
& ALL(a):[Set(a) & 1 a & ALL(b):[b n' & b a => b+1 a]
=> ALL(b):[b n' => b a]]
Premise
371 Set(n')
Split, 370
372 1 n'
Split, 370
373 ALL(a):[a n' => a+1 n']
Split, 370
374 ALL(a):[a n' => ~a+1=1]
Split, 370
375 ALL(a):ALL(b):[a n' & b n' & a+1=b+1 => a=b]
Split, 370
376 ALL(a):[Set(a) & 1 a & ALL(b):[b n' & b a => b+1 a]
=> ALL(b):[b n' => b a]]
Split, 370
Applying Set Equality Axiom...
377 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c a <=> c b]]]
Set Equality
378 ALL(b):[Set(n) & Set(b) => [n=b <=> ALL(c):[c n <=> c b]]]
U Spec, 377
379 Set(n) & Set(n') => [n=n' <=> ALL(c):[c n <=> c n']]
U Spec, 378
380 Set(n) & Set(n')
Join, 39, 371
381 n=n' <=> ALL(c):[c n <=> c n']
Detach, 379, 380
382 [n=n' => ALL(c):[c n <=> c n']]
& [ALL(c):[c n <=> c n'] => n=n']
Iff-And, 381
383 n=n' => ALL(c):[c n <=> c n']
Split, 382
Sufficient: For n=n'
384 ALL(c):[c n <=> c n'] => n=n'
Split, 382
Applying the principle of mathematical induction in n...
385 Set(n') & 1 n' & ALL(b):[b n & b n' => b+1 n']
=> ALL(b):[b n => b n']
U Spec, 364
386 x n & x n'
Premise
387 x n
Split, 386
388 x n'
Split, 386
389 x n' => x+1 n'
U Spec, 373
390 x+1 n'
Detach, 389, 388
391 x n & x n' => x+1 n'
Conclusion, 386
392 ALL(b):[b n & b n' => b+1 n']
U Gen, 391
393 Set(n') & 1 n'
Join, 371, 372
394 Set(n') & 1 n'
& ALL(b):[b n & b n' => b+1 n']
Join, 393, 392
395 ALL(b):[b n => b n']
Detach, 385, 394
Applying the principle of mathematical induction in n'...
396 Set(n) & 1 n & ALL(b):[b n' & b n => b+1 n]
=> ALL(b):[b n' => b n]
U Spec, 376
397 x n' & x n
Premise
398 x n'
Split, 397
399 x n
Split, 397
400 x n => x+1 n
U Spec, 108
401 x+1 n
Detach, 400, 399
402 x n' & x n => x+1 n
Conclusion, 397
403 ALL(b):[b n' & b n => b+1 n]
U Gen, 402
404 Set(n) & 1 n
Join, 39, 49
405 Set(n) & 1 n
& ALL(b):[b n' & b n => b+1 n]
Join, 404, 403
406 ALL(b):[b n' => b n]
Detach, 396, 405
407 x n
Premise
408 x n => x n'
U Spec, 395
409 x n'
Detach, 408, 407
410 x n => x n'
Conclusion, 407
411 x n'
Premise
412 x n' => x n
U Spec, 406
413 x n
Detach, 412, 411
414 x n' => x n
Conclusion, 411
415 [x n => x n'] & [x n' => x n]
Join, 410, 414
416 x n <=> x n'
Iff-And, 415
417 ALL(c):[c n <=> c n']
U Gen, 416
As Required:
n is unique
418 n=n'
Detach, 384, 417
Completing the axioms for the real numbers, we have the Archimedean Axiom in terms of n:
419 ALL(a):ALL(b):[a real & b real & 0<b => EXIST(c):[c n & a<b*c]]
Premise