Arithmetization — Source and provenance

Accepted projected chapter

41456 bytes; SHA-256 667517b3a4671b9c63932d98f92705a3f32005e151f0ab549756fb632e755046.

1. \olchapter{sfr}{arith}{Arithmetization}
3. \begin{editorial}
4. The material in this chapter presents the construction of the number
5. systems in na\"ive set theory. It is taken from Tim Button's Open Set
6. Theory text.
7. \end{editorial}
11. \olfileid{sfr}{arith}{int}
12. \olsection{From $\Nat$ to $\Int$}
14. Here are two basic realisations:
15. \begin{enumerate}
16. \item Every integer can be written in the form $n - m$, with $n, m \in\Nat$.
17. \item The information encoded in an expression $n - m$ can equally be encoded by an ordered pair $\tuple{n, m}$.
18. \end{enumerate}
19. We already know that the ordered pairs of natural numbers are the !!{element}s of $\Nat^2$. And we are assuming that we understand $\Nat$. So here is a na\"{i}ve suggestion, based on the two realisations we have had: \emph{let's treat integers as ordered pairs of natural numbers}.
21. In fact, this suggestion is too na\"{i}ve. Obviously we want it to be the case that $0- 2 = 4 - 6$. But evidently $\tuple{0, 2 }\neq \tuple{4, 6}$. So we cannot simply say that $\Nat^2$ is the set of integers.
23. Generalising from the preceding problem, what we want is the following:
24. $$a - b = c - d \text{ iff }a + d = c + b$$
25. (It should be obvious that this is how integers are \emph{meant} to behave: just add $b$ and $d$ to both sides.) And the easy way to guarantee this behaviour is just to define an equivalence relation between ordered pairs, $\Intequiv$, as follows:
26. $$\tuple{ a, b } \Intequiv \tuple{c, d}\text{ iff }a + d = c + b$$
27. We now have to show that this is an equivalence relation.
28. \begin{prop} $\Intequiv$ is an equivalence relation.
29. \end{prop}
30. \begin{proof}
31. We must show that $\Intequiv$ is reflexive, symmetric, and transitive.
33. \emph{Reflexivity:} Evidently $\tuple{a, b} \Intequiv \tuple{a, b}$, since $a + b = b + a$.
35. \emph{Symmetry:} Suppose $\tuple{a, b} \Intequiv \tuple{c, d}$, so $a + d = c + b$. Then $c + b = a + d$, so that $\tuple{c, d} \Intequiv \tuple{a, b}$.
37. \emph{Transitivity:} Suppose $\tuple{a, b} \Intequiv \tuple{c, d}\Intequiv \tuple{m, n}$. So $a + d = c + b$ and $c + n = m + d$. So $a + d + c + n = c + b + m + d$, and so $a + n = m + b$. Hence $\tuple{a, b } \Intequiv \tuple{m, n}$.
38. \end{proof}
40. Now we can use this equivalence relation to take equivalence classes:
42. \begin{defn}
43. The integers are the equivalence classes, under $\Intequiv$, of ordered pairs of natural numbers; that is, $\Int = \equivclass{\Nat^2}{\Intequiv}$.
44. \end{defn}
46. Now, one might have plenty of different \emph{philosophical} reactions to this stipulative definition. Before we consider those reactions, though, it is worth continuing with some of the technicalities.
48. Having said what the integers are, we shall need to define basic functions and relations on them. Let's write $\equivrep{m, n}{\Intequiv}$ for the equivalence class under $\Intequiv$ with $\tuple{m, n}$ as !!a{element}.\footnote{Note: using the notation introduced in \olref[sfr][rel][eqv]{def:equivalenceclass}, we would have written $\equivrep{\tuple{m,n}}{\Intequiv}$ for the same thing. But that's just a bit harder to read.} That is:
49. $$\equivrep{m, n}{\Intequiv} = \Setabs{\tuple{a, b} \in \Nat^2}{\tuple{a, b}\Intequiv \tuple{m, n}}$$
50. So now we offer some definitions:
51. \begin{align*}
52. \equivrep{a, b}{\Intequiv} + \equivrep{c, d}{\Intequiv} &= \equivrep{a + c, b + d}{\Intequiv}\\
53. \equivrep{a, b}{\Intequiv} \times \equivrep{c, d}{\Intequiv} &= \equivrep{a c + b d, a d + b c}{\Intequiv}\\
54. \equivrep{a, b}{\Intequiv} \leq \equivrep{c, d}{\Intequiv} &\text{ iff }a + d \leq b + c
55. \end{align*}
56. (As is common, I'm using `$ab$' stand for `$(a \times b)$', just to make the axioms easier to read.) Now, we need to make sure that these definitions behave as they \emph{ought} to. Spelling out what this means, and checking it through, is rather laborious; we relegate the details to \olref[check]{sec}. But the short point is: everything works!
58. One final thing remains. We have constructed the integers using
59. natural numbers. But this will mean that the natural numbers \emph{are
60. not themselves integers}. We will return to the philosophical
61. significance of this in \olref[ref]{sec}. On a purely technical front,
62. though, we will need some way to be able to treat natural numbers
63. \emph{as} integers. The idea is quite easy: for each $n \in \Nat$, we
64. just stipulate that $n_\Int = \equivrep{n, 0}{\Intequiv}$. We need to
65. confirm that this definition is well-behaved, i.e., that for any $m, n
66. \in \Nat$
67. \begin{align*}
68. (m + n)_\Int &= m_\Int + n_\Int\\
69. (m \times n)_\Int &= m_\Int \times n_\Int\\
70. m \leq n &\liff m_\Int \leq n_\Int
71. \end{align*}
72. But this is all pretty straightforward. For example, to show that the
73. second of these obtains, we can simply help ourselves to the behaviour
74. of the natural numbers and reason as follows:
77. \begin{align*}
79. (m \times n)_\Int &= \equivrep{m \times n, 0}{\Intequiv} \\
80. &= \equivrep{m \times n + 0 \times 0, m \times 0 + 0 \times n}{\Intequiv} \\
81. &= \equivrep{m, 0}{\Intequiv} \times \equivrep{n, 0}{\Intequiv} \\
82. &= m_\Int \times n_\Int
83. \end{align*}
85. We leave it as an exercise to confirm that the other two conditions hold.
86. \begin{prob}
87. Show that $(m + n)_\Int = m_\Int + n_\Int$ and $m \leq n \liff m_\Int \leq n_\Int$, for any $m, n \in \Nat$.
88. \end{prob}
92. \olfileid{sfr}{arith}{rat}
93. \olsection{From $\Int$ to $\Rat$}
95. We just saw how to construct the integers from the natural numbers,
96. using some na\"{i}ve set theory. We shall now see how to construct the
97. rationals from the integers in a very similar way. Our initial
98. realisations are:
99. \begin{enumerate}
100. \item Every rational can be written in the form $\nicefrac{i}{j}$,
101. where both $i$ and $j$ are integers but $j$ is non-zero.
102. \item The information encoded in an expression $\nicefrac{i}{j}$
103. can equally be encoded in an ordered pair $\tuple{ i, j}$.
104. \end{enumerate}
105. The obvious approach would be to think of the rationals \emph{as}
106. ordered pairs drawn from $\Int \times (\Int \setminus \{0_\Int\})$. As
107. before, though, that would be a bit too na\"ive, since we want
108. $\nicefrac{3}{2} = \nicefrac{6}{4}$, but $\tuple{ 3, 2}\neq \tuple{ 6,
109. 4}$. More generally, we will want the following:
110. \[
111. \nicefrac{a}{b} = \nicefrac{c}{d} \text{ iff } a \times d = b \times c
112. \]
113. To get this, we define an {equivalence relation} on $\Int \times
114. (\Int \setminus \{0_\Int\})$ thus:
115. \[
116. \tuple{ a, b }\Ratequiv \tuple{ c, d} \text{ iff }a \times d = b \times c
117. \]
118. We must check that this is an equivalence relation. This is very much
119. like the case of $\Intequiv$, and we will leave it as an exercise.
120. \begin{prob}
121. Show that $\Ratequiv$ is an equivalence relation.
122. \end{prob}
123. But it allows us to say:
124. \begin{defn}
125. The rationals are the equivalence classes, under $\Ratequiv$, of pairs
126. of integers (whose second element is non-zero). That is, $\Rat =
127. \equivclass{(\Int \times (\Int\setminus \{0_\Int\}))}{\Ratequiv}$.
128. \end{defn}
130. As with the integers, we also want to define some basic operations.
131. Where $\equivrep{i,j}{\Ratequiv}$ is the equivalence class under
132. $\Ratequiv$ with $\tuple{i, j}$ as !!a{element}, we say:
133. \begin{align*}
134. \equivrep{a, b}{\Ratequiv} + \equivrep{c, d}{\Ratequiv} &= \equivrep{ad + bc, bd}{\Ratequiv}\\
135. \equivrep{a, b}{\Ratequiv} \times \equivrep{c, d}{\Ratequiv} &= \equivrep{a c, b d}{\Ratequiv}.
136. \intertext{To define $r \leq s$ on these rationals, we use the fact that
137. $r \le s$ iff $s - r$ is not negative, i.e., $r - s$ can be written as
138. $\nicefrac{i}{j}$ with $i$ non-negative and $j$~positive:}
139. \equivrep{a, b}{\Ratequiv} \leq \equivrep{c, d}{\Ratequiv} &\text{ iff }
140. \equivrep{c, d}{\Ratequiv} - \equivrep{a, b}{\Ratequiv} =
141. \equivrep{i_\Int, j_\Int}{\Ratequiv}
142. \end{align*}
143. for some $i \in \Nat$ and $0 \neq j \in \Nat$.
145. We then need to check that these definitions behave as they
146. \emph{ought} to; and we relegate this to \olref[check]{sec}. But they
147. indeed do!{} Finally, we want some way to treat integers \emph{as}
148. rationals; so for each $i \in \Int$, we stipulate that $i_\Rat =
149. \equivrep{i, 1_\Int}{\Ratequiv}$. Again, we check that all of this
150. behaves correctly in \olref[check]{sec}.
152. \begin{prob}
153. Show that $(i + j)_\Rat = i_\Rat+ j_\Rat$ and $(i \times j)_\Rat =
154. i_\Rat \times j_\Rat$ and $i \leq j \liff i_\Rat \leq j_\Rat$, for any
155. $i, j \in \Int$.
156. \end{prob}
161. \olfileid{sfr}{arith}{real}
162. \olsection{The Real Line}
164. The next step is to show how to construct the reals from the
165. rationals. Before that, we need to understand what is
166. \emph{distinctive} about the reals.
168. The reals behave very much like the rationals. (Technically, both are
169. examples of \emph{ordered fields}; for the definition of this, see
170. \olref[check]{orderedfield}.) Now, if you worked through the exercises
171. to \olref[sfr][siz][]{chap}, you will know that there are strictly
172. more reals than rationals, i.e., that $\cardless{\Rat}{\Real}$. This
173. was first proved by Cantor. But it's been known for about two and a
174. half millennia that there are irrational numbers, i.e., reals which
175. are not rational. Indeed:
177. \begin{thm}\ollabel{root2irrational}
178. $\sqrt{2}$ is not rational, i.e., $\sqrt{2} \notin \Rat$
179. \end{thm}
181. \begin{proof}
182. Suppose, for reductio, that $\sqrt{2}$ is rational. So $\sqrt{2} =
183. \nicefrac{m}{n}$ for some natural numbers $m$ and $n$. Indeed, we can
184. choose $m$ and $n$ so that the fraction cannot be reduced any further.
185. Re-organising, $m^{2} = 2n^{2}$. From here, we can complete the proof
186. in two ways:
188. \emph{First, geometrically} (following Tennenbaum).\footnote{This
189. proof is reported by \cite{Conway2006}.} Consider these squares:
190. \begin{center}
191. \begin{tikzpicture}
192. \draw[thick] (0,0) rectangle (3,3);
193. \draw[thick, fill=red!50] (0,0) rectangle (2.3,2.3);
194. \draw[thick, fill=yellow!50] (0.7,0.7) rectangle (3, 3);
195. \draw[thick, fill=orange!50] (0.7,0.7) rectangle (2.3, 2.3);
196. \draw[<->] (4, 0.7)--(4, 3);
197. \node at (4.25, 1.85) (n) {$n$};
198. \draw[<->] (5, 0)--(5, 3);
199. \node at (5.25, 1.5) (m) {$m$};
200. \end{tikzpicture}
201. \end{center}
202. Since $m^2 = 2n^2$, the region where the two squares of side $n$
203. overlap has the same area as the region which neither of the two
204. squares cover; i.e., the area of the orange square equals the sum of
205. the area of the two unshaded squares. So where the orange square has
206. side $p$, and each unshaded square has side $q$, $p^2 = 2q^2$. But now
207. $\sqrt{2} = \nicefrac{p}{q}$, with $p < m$ and $q < n$ and $p, q \in
208. \Nat$. This contradicts the fact that $m$ and $n$ were chosen to be as
209. small as possible.
211. \emph{Second, formally.} Since $m^{2} = 2n^{2}$, it follows that $m$
212. is even. (It is easy to show that, if $x$ is odd, then $x^2$ is odd.)
213. So $m = 2r$, for some $r \in \Nat$. Rearranging, $2r^2 = n^2$,
219. so $n$ is also even. So both $m$ and $n$ are even, and hence the
220. fraction $\nicefrac{m}{n}$ \emph{can} be reduced further.
221. Contradiction!
222. \end{proof}
224. In passing, this diagrammatic proof allows us to revisit the material from \olref[his][set][mythology]{sec}. Tennenbaum (1927--2006) was a thoroughly modern mathematician; but the proof is undeniably lovely, completely rigorous, and appeals to geometric intuition!
226. In any case: the reals are ``more expansive'' than the rationals. In some sense, there are ``gaps'' in the rationals, and these are filled by the reals. Weierstrass realised that this describes a single property of the real numbers, which distinguishes them from the rationals, namely the Completeness Property: \emph{Every non-empty set of real numbers with an upper bound has a least upper bound.}
228. It is easy to see that the rationals do not have the Completeness Property. For example, consider the set of rationals less than $\sqrt{2}$, i.e.:
229. \[
230. \Setabs{p \in \Rat}{p^2 < 2 \text{ or }p < 0}
231. \]
232. This has an upper bound in the rationals; its !!{element}s< are all smaller than $3$, for example. But what is its least upper bound? We want to say `$\sqrt{2}$'; but we have just seen that $\sqrt{2}$ is \emph{not} rational. And there is no \emph{least} rational number greater than $\sqrt{2}$. So the set has an upper bound but no least upper bound. Hence the rationals lack the Completeness Property.
234. By contrast, the continuum ``morally ought'' to have the Completeness Property. We do not just want $\sqrt{2}$ to be a real number; we want to fill all the ``gaps'' in the rational line. Indeed, we want the continuum itself to have no ``gaps'' in it. That is just what we will get via Completeness.
239. \olfileid{sfr}{arith}{cuts}
240. \olsection{From $\Rat$ to $\Real$}
242. In essence, the Completeness Property shows that any point $\alpha$ of
243. the real line divides that line into two halves perfectly: those for
244. which $\alpha$ is the least upper bound, and those for which $\alpha$
245. is the greatest lower bound. To \emph{construct} the real numbers from
246. the rational numbers, Dedekind suggested that we simply think of the
247. reals as the \emph{cuts} that partition the rationals. That is, we
248. identify $\sqrt{2}$ with the \emph{cut} which separates the rationals
249. $< \sqrt{2}$ from the rationals $> \sqrt{2}$.
251. Let's tidy this up. If we cut the rational numbers into two halves, we
252. can uniquely identify the partition we made just by considering its
253. \emph{bottom} half. So, getting precise, we offer the following
254. definition:
256. \begin{defn}[Cut]
257. A \emph{cut} $\alpha$ is any non-empty proper
258. initial segment of the rationals with no greatest element. That is,
259. $\alpha$ is a cut iff:
260. \begin{enumerate}
261. \item \emph{non-empty, proper}: $\emptyset \neq \alpha \subsetneq \Rat$
262. \item \emph{initial}: for all $p,q \in \Rat$: if $p < q \in \alpha$ then $p \in \alpha$
263. \item \emph{no maximum}: for all $p \in \alpha$ there is a $q \in \alpha$ such that $p < q$
264. \end{enumerate}
265. Then $\Real$ is the set of cuts.
266. \end{defn}
268. So now we can say that $\sqrt{2} = \Setabs{p \in \Rat}{p^2 < 2\text{
269. or }p < 0}$. Of course, we need to check that this \emph{is} a cut,
270. but we relegate that to \olref[check]{sec}.
272. As before, having defined some entities, we next need to define basic
273. functions and relations upon them. We begin with an easy one:
274. \begin{align*}
275. \alpha \leq \beta \text{ iff }\alpha \subseteq \beta
276. \end{align*}
277. This definition of an order allows to \emph{state} the central result,
278. that the set of cuts has the Completeness Property. Spelled out fully,
279. the statement has this shape. If $S$ is a non-empty set of cuts with
280. an upper bound, then $S$ has a least upper bound. In more detail: there is a cut, $\lambda$, which is an upper bound for $S$, i.e.\ $(\forall \alpha \in S)\alpha \subseteq
281. \lambda$, and $\lambda$ is the least such cut, i.e.\ $(\forall \beta \in \Real)((\forall \alpha \in S)\alpha \subseteq \beta \lif \lambda \subseteq \beta)$. Now here is
282. the proof of the result:
284. \begin{thm}\ollabel{realcompleteness}
285. The set of cuts has the Completeness Property.
286. \end{thm}
288. \begin{proof}
289. Let $S$ be any non-empty set of cuts with an upper bound. Let $\lambda
290. = \bigcup S$.
292. We first claim that $\lambda$ is a cut:
293. \begin{enumerate}
294. \item Since $S$ has an upper bound, at least one cut is in $S$, so
295. $\emptyset \neq \lambda$. Since $S$ is a set of cuts, $\lambda
296. \subseteq \Rat$. Since $S$ has an upper bound, some $p \in \Rat$ is
297. absent from every cut $\alpha \in S$. So $p\notin \lambda$, and hence
298. $\lambda \subsetneq \Rat$.
299. \item Suppose $p < q \in \lambda$. So there is some $\alpha \in S$
300. such that $q \in \alpha$. Since $\alpha$ is a cut, $p \in \alpha$. So
301. $p \in \lambda$.
302. \item Suppose $p \in \lambda$. So there is some $\alpha \in S$ such
303. that $p \in \alpha$. Since $\alpha$ is a cut, there is some $q \in
304. \alpha$ such that $p < q$. So $q \in \lambda$.
305. \end{enumerate}
306. This proves the claim. Moreover, clearly $(\forall \alpha \in S)\alpha
307. \subseteq \bigcup S = \lambda$, i.e.\ $\lambda$ is an upper bound on $S$. So now suppose $\beta \in \mathbb{R}$ is also an upper bound, i.e.\ $(\forall \alpha \in S)\alpha \subseteq \beta$. For any $p \in \Rat$, if $p \in \lambda$, then there is $\alpha \in S$ such that $p \in \alpha$, so that $p \in \beta$. Generalizing, $\lambda \subseteq \beta$. So $\lambda$ is the \emph{least} upper bound on $S$.
308. \end{proof}
310. So we have a bunch of entities which satisfy the Completeness
311. Property. And one way to put this is: there are no ``gaps'' in our
312. cuts. (So: taking further ``cuts'' of reals, rather than rationals,
313. would yield no interesting new objects.)
315. Next, we must define some operations on the reals. We start by
316. embedding the rationals into the reals by stipulating that $p_\Real =
317. \Setabs{q \in \Rat}{q < p}$ for each $p \in \Rat$. We then define:
318. \begin{align*}
319. \alpha + \beta &= \Setabs{p + q}{p \in \alpha \land q \in \beta}\\
321. \alpha \times \beta &=
322. \Setabs{p \times q}{0 \leq p \in \alpha \land 0 \leq q \in \beta} \cup 0^\mathbb{R} & \text{if }\alpha, \beta \geq 0_\Real
325. \end{align*}
326. To handle the other multiplication cases, first let:
327. \begin{align*}
328. -\alpha &= \Setabs{p - q}{p < 0 \land q \notin \alpha}
329. \end{align*}
330. and then stipulate:
331. \begin{align*}
332. \alpha \times \beta &\defis
333. \begin{cases}
334. \mathord{-}\alpha \times \mathord{-}\beta &\text{if }\alpha < 0_\Real\text{ and }\beta < 0_\Real\\
335. \mathord{-}(\mathord{-}\alpha \times \beta) &\text{if }\alpha < 0_\Real \text{ and }\beta > 0_\Real\\
336. \mathord{-}(\alpha \times \mathord{-}\beta) &\text{if }\alpha > 0_\Real \text{ and }\beta < 0_\Real
337. \end{cases}
338. \end{align*}
339. We then need to check that each of these definitions always yields a
340. cut. And finally, we need to go through an easy (but long-winded)
341. demonstration that the cuts, so defined, behave exactly as they
342. should. But we relegate all of this to \olref[check]{sec}.
346. \olfileid{sfr}{arith}{ref}
347. \olsection{Some Philosophical Reflections}
349. So much for the technicalities. But what did they achieve?
351. Well, pretty uncontestably, they gave us some {lovely} pure mathematics. Moreover,
352. there were some deep conceptual achievements. It was a profound
353. insight, to see that the Completeness Property expresses the crucial
354. difference between the reals and the rationals. Moreover, the explicit
355. construction of reals, as Dedekind cuts, puts the subject matter of
356. analysis on a firm footing. We know that the notion of a
357. \emph{complete ordered field} is coherent, for the cuts form just such
358. a field.
360. For all that, we should air a few reservations about these achievements.
362. First, it is not clear that thinking of reals in terms of cuts is any
363. \emph{more} rigorous than thinking of reals in terms of their familiar
364. (possibly infinite) decimal expansions. This latter ``construction''
365. of the reals has some resemblance to the construction of the reals via
366. Cauchy sequence; but in fact, it was essentially known to
367. mathematicians from the early 17th century onwards (see
368. \olref[cauchy]{sec}). The real increase in rigour came from the
369. realisation that the reals have the Completeness Property; the ability
370. to construct real numbers as particular sets is perhaps not, by
371. itself, so very interesting.
373. It is even less clear that the (much easier) arithmetization of the
374. integers, or of the rationals, increases rigour in those areas. Here,
375. it is worth making a simple observation. Having \emph{constructed} the
376. integers as equivalence classes of ordered pairs of naturals, and then
377. constructed the rationals as equivalence classes of ordered pairs of
378. integers, and then constructed the reals as sets of rationals, we
379. immediately \emph{forget about} the constructions. In particular: no
380. one would ever want to \emph{invoke} these constructions during a
381. mathematical proof (excepting, of course, a proof that the
382. constructions behaved as they were supposed to). It's much easier to
383. speak about a real, directly, than to speak about some set of sets of
384. sets of sets of sets of sets of sets of naturals.
399. It is most doubtful of all that these definitions tell us what the
400. integers, rationals, or reals \emph{are}, \emph{metaphysically
401. speaking}. That is, it is doubtful that the reals (say) \emph{are}
402. certain sets (of sets of sets\ldots). The main barrier to such a view
403. is that the construction could have been done in many different ways.
404. In the case of the reals, there are some genuinely interestingly
405. different constructions (see \olref[cauchy]{sec}). But here is a
406. really trivial way to obtain some different constructions: as in
407. \olref[sfr][rel][ref]{sec}, we could have defined ordered pairs
408. slightly differently; if we had used this alternative notion of an
409. ordered pair, then our constructions would have worked precisely as
410. well as they did, but we would have ended up with different objects.
411. As such, there are many rival set-theoretic constructions of the
412. integers, the rationals, and the reals. And now it would just be
413. arbitrary (and embarrassing) to claim that the integers (say) are
414. \emph{these} sets, rather than \emph{those}. (As in
415. \olref[sfr][rel][ref]{sec}, this is an instance of an argument made
416. famous by \citealt{Benacerraf1965}.)
418. A further point is worth raising: there is something quite \emph{odd}
419. about our constructions. We started with the natural numbers. We then
420. construct the integers, and construct ``the $0$ of the integers'',
421. i.e., $ \equivrep{0,0}{\Intequiv}$. But $0 \neq
422. \equivrep{0,0}{\Intequiv}$. Indeed, given our constructions,
423. \emph{no} natural number is an integer. But that seems extremely
424. counter-intuitive. Indeed, in \olref[sfr][set][imp]{sec}, we claimed
425. without much argument that $\Nat \subseteq \Rat$. If the constructions
426. tell us exactly \emph{what} the numbers are, this claim was trivially
427. false.
429. Standing back, then, where do we get to? Working in a na\"ive set
430. theory, and helping ourselves to the naturals, we are able to
431. \emph{treat} integers, rationals, and reals as certain sets. In that
432. sense, we can \emph{embed} the theories of these entities within a set
433. theory. But the philosophical import of this embedding is just not
434. that straightforward.
436. Of course, none of this is the last word!{} The point is only this.
437. Showing that the arithmetization of the reals \emph{is} of deep
438. philosophical significance would require some additional
439. \emph{philosophical} argument.
448. \olfileid{sfr}{arith}{check}
449. \olsection{Ordered Rings and Fields}
451. Throughout this chapter, we claimed that certain definitions behave
452. ``as they ought''. In this technical appendix, we will spell out what
453. we mean, and (sketch how to) show that the definitions do behave
454. ``correctly''.
456. In \olref[int]{sec}, we defined addition and multiplication on $\Int$.
457. We want to show that, as defined, they endow $\Int$ with the structure
458. we ``would want'' it to have. In particular, the structure in question
459. is that of a commutative ring.
461. \begin{defn}
462. A \emph{commutative ring} is a set $S$, equipped with specific elements $0$ and $1$ and operations $+$ and $\times$, satisfying these eight formulas:
463. \begin{align*}
464. \emph{Associativity}&&a + (b+ c) & = (a + b) + c \\
465. && (a \times b) \times c & = a \times (b\times c)\\
466. \emph{Commutativity}&&a + b &= b+ a \\
467. && a \times b&= b\times a\\
468. \emph{Identities}&&a + 0 &= a \\
469. && a \times 1 &= a\\
470. \emph{Additive Inverse}&&(\exists b\in S)0&=a + b\\
471. \emph{Distributivity}&&a \times (b+ c ) &= (a \times b) + (a \times c)
472. \end{align*}
473. Implicitly, these are all bound with universal quantifiers restricted to $S$. And note that the elements $0$ and~$1$ here need not be the natural numbers with the same name.
474. \end{defn}
476. So, to check that the integers form a commutative ring, we just need
477. to check that we meet these eight conditions. None of the conditions
478. is {difficult} to establish, but this is a bit laborious. For example,
479. here is how to prove \emph{Associativity}, in the case of addition:
481. \begin{proof}
482. Fix $i, j, k \in \Int$. So there are $a_1, b_1, a_2, b_2, a_3, b_3 \in
483. \Nat$ such that $i = \equivrep{a_1, b_1}{}$ and $j =
484. \equivrep{a_2,b_2}{}$ and $k = \equivrep{a_3, b_3}{}$. (For
485. legibility, we write ``$\equivrep{x, y}{}$'' rather than
486. ``$\equivrep{x, y}{\Intequiv}$''; we'll do this throughout this
487. section.) Now:
488. \begin{align*}
489. i + (j + k) &= \equivrep{a_1, b_1}{}+(\equivrep{a_2, b_2}{} + \equivrep{a_3, b_3}{}) \\
490. &= \equivrep{a_1, b_1}{} + \equivrep{a_2+a_3, b_2+b_3}{}\\
491. &= \equivrep{a_1 + (a_2 + a_3), b_1 + (b_2 + b_3)}{}\\
492. &= \equivrep{(a_1 + a_2) + a_3, (b_1 + b_2) + b_3}{}\\
493. &= \equivrep{a_1 + a_2, b_1 + b_2}{} + \equivrep{a_3, b_3}{}\\
494. &= (\equivrep{a_1, b_1}{} + \equivrep{a_2, b_2}{}) + \equivrep{a_3, b_3}{}\\
495. &= (i+j) + k
496. \end{align*}
497. helping ourselves freely to the behavior of addition on $\Nat$.
498. \end{proof}
500. Equally, here is how to prove \emph{Additive Inverse}:
502. \begin{proof}
503. Fix $i \in \Int$, so that $i = \equivrep{a,b}{}$ for some $a,b \in
504. \Nat$. Let $j = \equivrep{b,a}{} \in \Int$. Helping ourselves to the
505. behaviour of the naturals, $(a+b) + 0 = 0 + (a+b)$, so that
506. $\tuple{a+b, b+a} \sim_\Int \tuple{0,0}$ by definition, and hence
507. $\equivrep{a+b, b+a}{} = \equivrep{0, 0}{} = 0_\Int$. So now $i + j =
508. \equivrep{a,b}{}+\equivrep{b,a}{}=\equivrep{a+b, b+a}{}= \equivrep{0,
509. 0}{} = 0_\Int$.
510. \end{proof}
512. And here is a proof of \emph{Distributivity}:
514. \begin{proof}
515. As above, fix $i = \equivrep{a_1, b_1}{}$ and $j =
516. \equivrep{a_2,b_2}{}$ and $k = \equivrep{a_3, b_3}{}$. Now:
517. \begin{align*}
518. i \times (j + k)
519. &= \equivrep{a_1, b_1}{} \times (\equivrep{a_2,b_2}{} + \equivrep{a_3, b_3}{})\\
520. &= \equivrep{a_1, b_1}{} \times \equivrep{a_2 + a_3,b_2+b_3}{}\\
521. &= \equivrep{a_1 (a_2 + a_3) + b_1 (b_2+b_3), a_1 (b_2 + b_3) + b_1 (a_2 + a_3)}{}\\
522. &= \equivrep{a_1 a_2 + a_1a_3 + b_1 b_2+b_1b_3, a_1 b_2 + a_1b_3 + a_2b_1 + a_3b_1}{}\\
524. &= \equivrep{a_1a_2 + b_1b_2, a_1b_2 + a_2b_1}{} + \equivrep{a_1a_3 + b_1b_3, a_1b_3 + a_3b_1}{}\\
525. &= (\equivrep{a_1, b_1}{} \times \equivrep{a_2,b_2}{}) + (\equivrep{a_1, b_1}{} \times \equivrep{a_3, b_3}{})\\
526. &= (i \times j) + (i \times k)
527. \end{align*}
528. \end{proof}
530. We leave it as an exercise to prove the remaining five conditions.
531. Having done that, we have shown that $\Int$ constitutes a commutative
532. ring, i.e., that addition and multiplication (as defined) behave as
533. they should.
535. \begin{prob}
536. Prove that $\Int$ is a commutative ring.
537. \end{prob}
539. But our task is not over. As well as defining addition and
540. multiplication over $\Int$, we defined an ordering relation, $\leq$,
541. and we must check that this behaves as it should. In more detail, we
542. must show that $\Int$ constitutes an \emph{ordered} ring.\footnote{Recall
543. from \olref[sfr][rel][ord]{def:linearorder} that a total order
544. is a relation which is reflexive, transitive, anti-symmetric, and connected.
545. In the context of order relations, connectedness is sometimes called
546. \emph{trichotomy}, since for any $a$ and $b$ we have $a \leq b \lor a
547. = b \lor a \geq b$.}
549. \begin{defn}
550. An \emph{ordered ring} is a commutative ring which is also equipped
551. with a total order relation, $\leq$, such that:
552. \begin{align*}
553. a \leq b &\lif a + c \leq b + c\\
554. (a \leq b \land 0 \leq c) &\lif a \times c \leq b \times c
555. \end{align*}
556. \end{defn}
558. \begin{prob}
559. Prove that $\Int$ is an ordered ring.
560. \end{prob}
562. As before, it is laborious but routine to show that~$\Int$, as
563. constructed, is an ordered ring. We will leave that to you.
565. This takes care of the integers. But now we need to show very similar
566. things of the rationals. In particular, we now need to show that the
567. rationals form an ordered \emph{field}, under our given definitions of
568. $+$, $\times$, and $\leq$:
569. \begin{defn}\ollabel{orderedfield}
570. An \emph{ordered field} is an ordered ring which also satisfies:
571. \begin{align*}
572. \emph{Multiplicative Inverse}& & (\forall a \in S \setminus \{0\})(\exists b \in S) a\times b& = 1
573. \end{align*}
574. \end{defn}
576. Once you have shown that $\Int$ constitutes an ordered ring, it is
577. easy but laborious to show that $\Rat$ constitutes an ordered field.
579. \begin{prob}
580. Prove that $\Rat$ is an ordered field.
581. \end{prob}
583. Having dealt with the integers and the rationals, it only remains to
584. deal with the reals. In particular, we need to show that $\Real$
585. constitutes a \emph{complete} ordered field, i.e., an ordered field
586. with the Completeness Property. Now, \olref[cuts]{realcompleteness}
587. established that $\Real$ has the Completeness Property. However, it
588. remains to run through the (tedious) of checking that $\Real$ is an
589. ordered field.
591. Before tearing off into \emph{that} laborious exercise, we need to
592. check some more ``immediate'' things. For example, we need a guarantee
593. that $\alpha + \beta$, as defined, is indeed a \emph{cut}, for any
594. cuts $\alpha$ and $\beta$. Here is a proof of that fact:
596. \begin{proof}
597. Since $\alpha$ and $\beta$ are both cuts, $\alpha + \beta = \Setabs{p
598. + q}{p \in \alpha \land q \in \beta}$ is a non-empty proper subset of
599. $\Rat$. Now suppose $x < p + q$ for some $p \in \alpha$ and $q \in \beta$.
600. Then $x - p < q$, so $x - p \in \beta$, and $x = p + (x - p) \in
601. \alpha + \beta$. So $\alpha + \beta$ is an initial segment of $\Rat$.
602. Finally, for any $p + q \in \alpha + \beta$, since $\alpha$ and
603. $\beta$ are both cuts, there are $p_1 \in \alpha$ and $q_1 \in \beta$
604. such that $p < p_1$ and $q < q_1$; so $p + q < p_1 + q_1 \in \alpha +
605. \beta$; so $\alpha + \beta$ has no maximum.
606. \end{proof}
608. Similar efforts will allow you to check that $\alpha - \beta$ and
609. $\alpha \times \beta$ and $\alpha \div \beta$ are cuts (in the last
610. case, ignoring the case where $\beta$ is the zero-cut). Again, though,
611. we will simply leave this to you.
613. \begin{prob}
614. Prove that $\Real$ is an ordered field.
615. \end{prob}
617. But here is a small loose end to tidy up. In
618. \olref[cuts]{sec}, we suggest that we can take $\sqrt{2} =
619. \Setabs{p \in \Rat}{p < 0 \text{ or }p^2 < 2}$. But we do need to show
620. that this set is a \emph{cut}. Here is a proof of that fact:
622. \begin{proof}
623. Clearly this is a nonempty proper initial segment of the rationals; so
624. it suffices to show that it has no maximum. In particular, it suffices
625. to show that, where $p$ is a positive rational with $p^2 < 2$ and $q =
626. \frac{2p+2}{p+2}$, both $p < q$ and $q^2 < 2$. To see that $p < q$,
627. just note:
628. \begin{align*}
629. p^2 &< 2\\
630. p^2 + 2p &< 2 + 2p\\
631. p(p + 2) &< 2 + 2p\\
632. p &< \tfrac{2+2p}{p+2} = q
633. \end{align*}
634. To see that $q^2 < 2$, just note:
635. \begin{align*}
636. p^2 &< 2\\
637. 2p^2 + 4p + 2 &< p^2 + 4p+ 4\\
638. 4p^2 + 8p + 4 &< 2(p^2 + 4p + 4)\\
639. (2p+2)^2 & <2(p+2)^2\\
640. \tfrac{(2p+2)^2}{(p+2)^2} &< 2\\
641. q^2 &< 2
642. \end{align*}
643. \end{proof}
647. \olfileid{sfr}{arith}{cauchy}
649. \olsection{Appendix: the Reals as Cauchy Sequences}
651. In \olref[cuts]{sec}, we constructed the reals as Dedekind cuts. In
652. this section, we explain an alternative construction. It builds on
653. Cauchy's definition of (what we now call) a Cauchy sequence; but the
654. use of this definition to \emph{construct} the reals is due to other
655. nineteenth-century authors, notably Weierstrass, Heine, M\'{e}ray and
656. Cantor. (For a nice history, see \citeauthor{OConnorRobertson:RN}
657. \citeyear{OConnorRobertson:RN}.)
659. Before we get to the nineteenth century, it's worth considering Simon
660. Stevin (1548--1620). In brief, Stevin realised that we can think of
661. each real in terms of its decimal expansion. Thus even an irrational
662. number, like $\sqrt{2}$, has a nice decimal expansion, beginning:
663. \[
664. 1.41421356237\ldots
665. \]
666. It is very easy to model decimal expansions in set theory: simply
667. consider them as functions $d \colon \Nat \to \Nat$, where $d(n)$ is
668. the $n$th decimal place that we are interested in. We will then need a
669. bit of tweak, to handle the bit of the real number that comes before
670. the decimal point (here, just $1$). We will also need a further tweak
671. (an equivalence relation) to guarantee that, for example, $0.999\ldots
672. = 1$. But it is not difficult to offer a perfectly rigorous
673. construction of the real numbers, in the manner of Stevin, within set
674. theory.
676. Stevin is not our focus. (For more on Stevin, see
677. \citealt{KatzKatz2012}.) But here is a closely related thought.
678. Instead of treating $\sqrt{2}$'s decimal expansion directly, we can
679. instead consider a \emph{sequence} of increasingly accurate rational
680. approximations to $\sqrt{2}$, by considering the increasingly precise
681. expansions:
682. \[
683. 1, 1.4, 1.414, 1.4142, 1.41421,\ldots
684. \]
685. The idea that reals can be considered via ``increasingly good
686. approximations'' provides us with the basis for another sequence of
687. insights (akin to the realisations that we used when constructing
688. $\Rat$ from $\Int$, or $\Int$ from $\Nat$). The basic insights are
689. these:
690. \begin{enumerate}
691. \item Every real can be written as a (perhaps infinite) decimal
692. expansion.
693. \item The information encoded by a (perhaps infinite) decimal
694. expansion can be equally be encoded by a sequence of rational
695. numbers.
696. \item A sequence of rational numbers can be thought of as a
697. function from $\Nat$ to $\Rat$; just let $f(n)$ be the $n$th
698. rational in the sequence.
699. \end{enumerate}
700. Of course, not just \emph{any} function from $\Nat$ to $\Rat$ will
701. give us a real number. For instance, consider this function:
702. \[
703. f(n) =\begin{cases}
704. 1 & \text{if }n\text{ is odd}\\
705. 0 &\text{if }n\text{ is even}
706. \end{cases}
707. \]
708. Essentially the worry here is that the sequence $0,1,0,1,0,1,0,\ldots$
709. doesn't seem to ``hone in'' on any real. So: to ensure that we
710. consider sequences which do hone in on some real, we need to restrict
711. our attention to sequences which have some \emph{limit}.
713. We have already encountered the idea of a limit, in
714. \olref[his][set][limits]{sec}. But we cannot use \emph{quite} the same
715. definition as we used there. The expression ``$(\forall \epsilon>0)$''
716. there tacitly involved quantification over the real numbers; and we
717. were considering the limits of functions on the real numbers; so
718. invoking that definition would be to help ourselves to the real
719. numbers; and they are exactly what we were aiming to \emph{construct}.
720. Fortunately, we can work with a closely related idea of a limit.
721. \begin{defn}\ollabel{def:CauchySequence}
722. A function $f: \Nat \to \Rat$ is a \emph{Cauchy sequence} iff for
723. any positive $\epsilon \in \Rat$ we have that $(\exists \ell \in
724. \Nat)(\forall m, n > \ell)|f(m) - f(n)| < \epsilon$.
725. \end{defn}
727. The general idea of a limit is the same as before: if you want a
728. certain level of precision (measured by~$\epsilon$), there is a
729. ``region'' to look in (any input greater than~$\ell$). And it is easy
730. to see that our sequence $1$, $1.4$, $1.414$, $1.4142$,
731. $1.41421$\ldots has a limit: if you want to approximate $\sqrt{2}$ to
732. within an error of $\nicefrac{1}{10^{n}}$, then just look to any entry
733. after the $n$th.
735. The obvious thought, then, would be to say that a real number just
736. \emph{is} any Cauchy sequence. But, as in the constructions of $\Int$
737. and $\Rat$, this would be too na\"{i}ve: for any given real number,
738. multiple different Cauchy sequences indicate that real number. A
739. simple way to see this as follows. Given a Cauchy sequence~$f$, define
740. $g$ to be exactly the same function as~$f$, except that $g(0)\neq
741. f(0)$. Since the two sequences agree everywhere after the first
742. number, we will (ultimately) want to say that they have the same
743. limit, in the sense employed in \olref{def:CauchySequence},
744. and so should be thought of ``defining'' the same real. So, we should
745. really think of these Cauchy sequences as the same real number.
747. Consequently, we again need to define an equivalence relation on the
748. Cauchy sequences, and identify real numbers with equivalence
749. relations. First we need the idea of a function which tends to $0$ in
750. the limit. For any function $h : \Nat \to \Rat$, say that \emph{$h$
751. tends to $0$} iff for any positive $\epsilon \in \Rat$ we have that
752. $(\exists \ell \in \Nat)(\forall n > \ell)|h(n)| <
753. \epsilon$.\footnote{Compare this with the definition of $\lim_{x
754. \mathord{\rightarrow}\infty}f(x) = 0$ in
755. \olref[his][set][limits]{sec}.} Further, where $f$ and $g$ are
756. functions $\Nat \to \Rat$, let $(f-g)(n) = f(n) - g(n)$. Now define:
757. \[
758. f \Realequiv g \text{ iff $(f-g)$ tends to $0$}.
759. \]
760. We need to check that $\Realequiv$ is an equivalence relation; and it
761. is. We can then, if we like, define the reals as the equivalence
762. classes, under $\Realequiv$, of all Cauchy sequences from $\Nat \to
763. \Rat$.
765. \begin{prob}
766. Let $f(n) = 0$ for every $n$. Let $g(n) = \frac{1}{(n+1)^2}$. Show
767. that both are Cauchy sequences, and indeed that the limit of both
768. functions is $0$, so that also $f \sim_\Real g$.
769. \end{prob}
771. Having done this, we shall as usual write $\equivrep{f}{\Realequiv}$
772. for the equivalence class with $f$ as !!a{element}. However, to keep
773. things readable, in what follows we will drop the subscript and write
774. just $\equivrep{f}{}$. We also stipulate that, for each $q \in \Rat$,
775. we have $q_{\Real} = \equivrep{c_{q}}{}$, where $c_{q}$ is the
776. constant function $c_q(n) = q$ for all $n \in \Nat$. We then define
777. basic relations and operations on the reals, e.g.:
778. \begin{align*}
779. \equivrep{f}{} + \equivrep{g}{} &= \equivrep{(f + g)}{} \\
780. \equivrep{f}{} \times \equivrep{g}{} &= \equivrep{(f \times g)}{}
781. \end{align*}
782. where $(f + g)(n) = f(n) + g(n)$ and $(f \times g)(n) = f(n) \times
783. g(n)$. Of course, we also need to check that each of $(f + g)$,
784. $(f-g)$ and $(f\times g)$ are Cauchy sequences when $f$ and $g$ are;
785. but they are, and we leave this to you.
787. Finally, we define we a notion of order. Say $\equivrep{f}{}$ is
788. \emph{positive} iff both $\equivrep{f}{}\neq 0_\Rat$ and $(\exists
789. \ell \in \Nat)(\forall n > \ell)0 < f(n)$. Then say $\equivrep{f}{} <
790. \equivrep{g}{}$ iff $\equivrep{(g - f)}{}$ is positive. We have to
791. check that this is well-defined (i.e., that it does not depend upon
792. choice of ``representative'' function from the equivalence class).
797. But having done this, it is quite easy to show that these yield the
798. right algebraic properties; that is:
799. \begin{thm}\ollabel{thm:cauchyorderedfield}
800. The Cauchy sequences constitute an ordered field.
801. \end{thm}
803. \begin{proof}
804. Exercise.
805. \end{proof}
807. \begin{prob}
808. Prove that the Cauchy sequences constitute an ordered field.
809. \end{prob}
811. It is harder to prove that the reals, so constructed, have the
812. Completeness Property, so we will give the proof.
814. \begin{thm}
815. Every non-empty set of Cauchy sequences with an upper bound has a
816. least upper bound.
817. \end{thm}
819. \begin{proof}[Proof sketch] Let $S$ be any non-empty set of Cauchy
820. sequences with an upper bound. So there is some $p \in \Rat$ such that
821. $p_{\Real}$ is an upper bound for $S$. Let $r \in S$; then there is
822. some $q \in \Rat$ such that $q_{\Real} < r$. So if a least upper bound
823. on $S$ exists, it is between $q_\Real$ and $p_\Real$ (inclusive).
825. We will hone in on the l.u.b., by approaching it simultaneously from
826. below and above. In particular, we define two functions, $f, g \colon
827. \Nat \to \Rat$, with the aim that $f$ will hone in on the l.u.b.\ from
828. above, and $g$ will hone on in it from below. We start by defining:
829. \begin{align*}
830. f(0) &= p \\
831. g(0) &= q
832. \end{align*}
833. Then, where $a_n = \frac{f(n) + g(n)}{2}$, let:\footnote{This is a
834. recursive definition. But we have not \emph{yet} given any reason to
835. think that recursive definitions are ok.}
836. \begin{align*}
837. f(n+1) &=
838. \begin{cases}
839. a_n &\text{if }(\forall h \in S)\equivrep{h}{} \leq (a_n)_\Real\\
840. f(n)&\text{otherwise}
841. \end{cases}\\
842. g(n+1) &=
843. \begin{cases}
844. a_n &\text{if }(\exists h \in S)\equivrep{h}{} \geq (a_n)_\Real\\
845. g(n) &\text{otherwise}
846. \end{cases}
847. \end{align*}
848. Both $f$ and $g$ are Cauchy sequences. (This can be checked fairly
849. easily, but we leave it as an exercise.) Note that the function $(f-g)$
850. tends to $0$, since the difference between $f$ and $g$ halves at each
851. step. Hence $\equivrep{f}{} = \equivrep{g}{}$.
853. We first show that $\equivrep{f}{}$ is an upper bound on $S$, i.e.\ that $(\forall h \in S)\equivrep{h}{} \leq \equivrep{f}{}$.
854. (We will invoke \olref{thm:cauchyorderedfield} as we go.) Let $h \in S$ and
855. suppose, for reductio, that $\equivrep{f}{} < \equivrep{h}{}$, so that
856. $0_\Real < \equivrep{(h-f)}{}$. Since $f$ is a monotonically
857. decreasing Cauchy sequence, there is some $n \in \Nat$ such that
858. $\equivrep{(c_{f(n)} - f)}{} < \equivrep{(h-f)}{}$. So:
859. \[
860. (f(n))_\Real = \equivrep{c_{f(n)}}{} < \equivrep{f}{} + \equivrep{(h-f)}{} = \equivrep{h}{},
861. \]
862. contradicting the fact that, by construction, $\equivrep{h}{} \leq (f(n))_\Real$.
864. We next show that $\equivrep{f}{} = \equivrep{g}{}$ is the \emph{least} upper bound on $S$. So let $j$ be any Cauchy sequence and suppose $\equivrep{j}{} < \equivrep{g}{}$. Reasoning as above (using the fact that $g$ is \emph{increasing}), there is $n \in \Nat$ such that $\equivrep{j}{} < (g(n))_\Real$. But by construction there is $h \in S$ such that $(g(n))_\Real \leq \equivrep{h}{}$, so $\equivrep{j}{} < \equivrep{h}{}$ and therefore $\equivrep{j}{}$ is not an upper bound on $S$.
865. \end{proof}
869. \OLEndChapterHook

content/sets-functions-relations/arithmetization/arithmetization.tex

1 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 8 · structure · records structure-00040

   \olchapter{Arithmetization}

content/sets-functions-relations/arithmetization/integers.tex

58 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 10 · formula-context · records projected-formula-0002339 projected-formula-0002340

   \olfileid{sfr}{arith}{int}

2. Line 11 · formula, structure · records projected-formula-0002339 projected-formula-0002340 structure-00041

   \olsection{From $\Nat$ to $\Int$}

3. Line 14 · formula-context · records projected-formula-0002341 projected-formula-0002342

   	\begin{enumerate}

4. Line 15 · formula, formula-context · records projected-formula-0002341 projected-formula-0002342 projected-formula-0002343 projected-formula-0002344

   		\item Every integer can be written in the form $n - m$, with $n, m \in\Nat$.

5. Line 16 · formula, formula-context · records projected-formula-0002341 projected-formula-0002342 projected-formula-0002343 projected-formula-0002344

   		\item The information encoded in an expression $n - m$ can equally be encoded by an ordered pair $\tuple{n, m}$.

6. Line 17 · formula-context · records projected-formula-0002343 projected-formula-0002344 projected-formula-0002345 projected-formula-0002346

   	\end{enumerate}

7. Line 18 · formula · records projected-formula-0002345 projected-formula-0002346

   We already know that the ordered pairs of natural numbers are the !!{element}s of $\Nat^2$. And we are assuming that we understand $\Nat$. So here is a na\"{i}ve suggestion, based on the two realisations we have had: \emph{let's treat integers as ordered pairs of natural numbers}.

8. Line 20 · formula · records projected-formula-0002347 projected-formula-0002348 projected-formula-0002349

   In fact, this suggestion is too na\"{i}ve. Obviously we want it to be the case that $0- 2 = 4 - 6$. But evidently $\tuple{0, 2 }\neq \tuple{4, 6}$. So we cannot simply say that $\Nat^2$ is the set of integers. 

9. Line 22 · formula-context · records projected-formula-0002350

   Generalising from the preceding problem, what we want is the following:

10. Line 23 · formula, formula-context · records projected-formula-0002350 projected-formula-0002351 projected-formula-0002352 projected-formula-0002353

    	$$a - b = c - d \text{ iff }a + d = c + b$$

11. Line 24 · formula, formula-context · records projected-formula-0002350 projected-formula-0002351 projected-formula-0002352 projected-formula-0002353 projected-formula-0002354

    (It should be obvious that this is how integers are \emph{meant} to behave: just add $b$ and $d$ to both sides.) And the easy way to guarantee this behaviour is just to define an equivalence relation between ordered pairs, $\Intequiv$, as follows:

12. Line 25 · formula, formula-context · records projected-formula-0002351 projected-formula-0002352 projected-formula-0002353 projected-formula-0002354

    $$\tuple{ a, b } \Intequiv \tuple{c, d}\text{ iff }a + d = c + b$$  

13. Line 26 · formula-context · records projected-formula-0002354 projected-formula-0002355

    We now have to show that this is an equivalence relation.

14. Line 27 · formal-object, formula · records projected-env-000337 projected-formula-0002355

    \begin{prop} $\Intequiv$ is an equivalence relation.

15. Line 28 · formal-object, formula-context · records projected-env-000337 projected-formula-0002355

    \end{prop}

16. Line 29 · formula-context · records projected-formula-0002356

    	\begin{proof}

17. Line 30 · formula · records projected-formula-0002356

    	We must show that $\Intequiv$ is reflexive, symmetric, and transitive. 

18. Line 31 · formula-context · records projected-formula-0002356 projected-formula-0002357 projected-formula-0002358

19. Line 32 · formula · records projected-formula-0002357 projected-formula-0002358

    	\emph{Reflexivity:} Evidently $\tuple{a, b} \Intequiv \tuple{a, b}$, since $a + b = b + a$.

20. Line 33 · formula-context · records projected-formula-0002357 projected-formula-0002358 projected-formula-0002359 projected-formula-0002360 projected-formula-0002361 projected-formula-0002362

21. Line 34 · formula · records projected-formula-0002359 projected-formula-0002360 projected-formula-0002361 projected-formula-0002362

    	\emph{Symmetry:} Suppose $\tuple{a, b} \Intequiv \tuple{c, d}$, so $a + d = c + b$. Then $c + b = a + d$, so that $\tuple{c, d} \Intequiv \tuple{a, b}$.

22. Line 35 · formula-context · records projected-formula-0002359 projected-formula-0002360 projected-formula-0002361 projected-formula-0002362 projected-formula-0002363 projected-formula-0002364 projected-formula-0002365 projected-formula-0002366 projected-formula-0002367 projected-formula-0002368

23. Line 36 · formula · records projected-formula-0002363 projected-formula-0002364 projected-formula-0002365 projected-formula-0002366 projected-formula-0002367 projected-formula-0002368

    	\emph{Transitivity:} Suppose $\tuple{a, b} \Intequiv \tuple{c, d}\Intequiv \tuple{m, n}$. So $a + d = c + b$ and $c + n = m + d$. So $a + d + c + n = c + b + m + d$, and so $a + n = m + b$. Hence $\tuple{a, b } \Intequiv \tuple{m, n}$.		

24. Line 37 · formula-context · records projected-formula-0002363 projected-formula-0002364 projected-formula-0002365 projected-formula-0002366 projected-formula-0002367 projected-formula-0002368

    \end{proof}

25. Line 41 · formal-object, formula-context · records projected-env-000339 projected-formula-0002369 projected-formula-0002370

    \begin{defn}

26. Line 42 · formal-object, formula · records projected-env-000339 projected-formula-0002369 projected-formula-0002370

    		The integers are the equivalence classes, under $\Intequiv$, of  ordered pairs of natural numbers; that is, $\Int = \equivclass{\Nat^2}{\Intequiv}$.

27. Line 43 · formal-object, formula-context · records projected-env-000339 projected-formula-0002369 projected-formula-0002370

    \end{defn}

28. Line 47 · formula, formula-context, reference · records projected-formula-0002371 projected-formula-0002372 projected-formula-0002373 projected-formula-0002374 projected-formula-0002375 reference-000080

    Having said what the integers are, we shall need to define basic functions and relations on them. Let's write $\equivrep{m, n}{\Intequiv}$ for the equivalence class under $\Intequiv$ with $\tuple{m, n}$ as !!a{element}.\footnote{Note: using the notation introduced in \olref[sfr][rel][eqv]{def:equivalenceclass}, we would have written $\equivrep{\tuple{m,n}}{\Intequiv}$ for the same thing. But that's just a bit harder to read.} That is: 

    [olref reference to sfr:rel:eqv:def:equivalenceclass]

29. Line 48 · formula, formula-context · records projected-formula-0002371 projected-formula-0002372 projected-formula-0002373 projected-formula-0002374 projected-formula-0002375

    	$$\equivrep{m, n}{\Intequiv} = \Setabs{\tuple{a, b} \in \Nat^2}{\tuple{a, b}\Intequiv \tuple{m, n}}$$

30. Line 49 · formula-context · records projected-formula-0002375 projected-formula-0002376

    So now we offer some definitions:

31. Line 50 · formal-object, formula · records projected-env-000340 projected-formula-0002376

    	\begin{align*}

32. Line 51 · formal-object, formula-context · records projected-env-000340 projected-formula-0002376

    		\equivrep{a, b}{\Intequiv} + \equivrep{c, d}{\Intequiv} &= \equivrep{a + c, b + d}{\Intequiv}\\

33. Line 52 · formal-object · records projected-env-000340

    		\equivrep{a, b}{\Intequiv} \times \equivrep{c, d}{\Intequiv} &= \equivrep{a c + b  d, a  d + b c}{\Intequiv}\\

34. Line 53 · formal-object · records projected-env-000340

    		\equivrep{a, b}{\Intequiv} \leq \equivrep{c, d}{\Intequiv} &\text{ iff }a + d \leq b + c

35. Line 54 · formal-object, formula-context · records projected-env-000340 projected-formula-0002377 projected-formula-0002378

    	\end{align*}	

36. Line 55 · formula, reference, source-correction · records TR006-SOURCE-PROSE-001 projected-formula-0002377 projected-formula-0002378 reference-000081

    (As is common, I'm using `$ab$' stand for `$(a \times b)$', just to make the axioms easier to read.) Now, we need to make sure that these definitions behave as they \emph{ought} to. Spelling out what this means, and checking it through, is rather laborious; we relegate the details to \olref[check]{sec}. But the short point is: everything works! 

    [olref reference to sfr:arith:check:sec]

37. Line 60 · reference · records reference-000082

    [olref reference to sfr:arith:ref:sec]

38. Line 61 · formula-context · records projected-formula-0002379

    though, we will need some way to be able to treat natural numbers

39. Line 62 · formula, formula-context · records projected-formula-0002379 projected-formula-0002380

    \emph{as} integers. The idea is quite easy: for each $n \in \Nat$, we

40. Line 63 · formula, formula-context · records projected-formula-0002379 projected-formula-0002380 projected-formula-0002381

    just stipulate that $n_\Int = \equivrep{n, 0}{\Intequiv}$. We need to

41. Line 64 · formula, formula-context · records projected-formula-0002380 projected-formula-0002381

    confirm that this definition is well-behaved, i.e., that for any $m, n

42. Line 65 · formula-context · records projected-formula-0002381 projected-formula-0002382

    \in \Nat$

43. Line 66 · formal-object, formula · records projected-env-000341 projected-formula-0002382

    \begin{align*}

44. Line 67 · formal-object, formula-context · records projected-env-000341 projected-formula-0002382

    	(m + n)_\Int &= m_\Int + n_\Int\\

45. Line 68 · formal-object · records projected-env-000341

    	(m \times n)_\Int &= m_\Int \times n_\Int\\

46. Line 69 · formal-object · records projected-env-000341

    	m \leq n &\liff m_\Int \leq n_\Int

47. Line 70 · formal-object · records projected-env-000341

    \end{align*}

48. Line 75 · formula-context · records projected-formula-0002383

    %	Helping myself to the behaviour of the natural numbers, evidently:

49. Line 76 · formal-object, formula · records projected-env-000342 projected-formula-0002383

    	\begin{align*}

50. Line 77 · formal-object, formula-context · records projected-env-000342 projected-formula-0002383

    %		(m + n)_\Int  = \equivrep{m + n, 0}{\Intequiv} = \equivrep{m + n, 0 + 0}{\Intequiv} = \equivrep{m, 0}{\Intequiv} + \equivrep{n, 0}{\Intequiv} = m_\Int + n_\Int\\

51. Line 78 · formal-object · records projected-env-000342

    		(m \times n)_\Int  &= \equivrep{m \times n, 0}{\Intequiv} \\

52. Line 79 · formal-object · records projected-env-000342

    		&= \equivrep{m \times n + 0 \times 0, m \times 0 + 0 \times n}{\Intequiv} \\

53. Line 80 · formal-object · records projected-env-000342

    		&= \equivrep{m, 0}{\Intequiv} \times \equivrep{n, 0}{\Intequiv} \\

54. Line 81 · formal-object · records projected-env-000342

    		&= m_\Int \times n_\Int

55. Line 82 · formal-object · records projected-env-000342

    	\end{align*}

56. Line 85 · formal-object, formula-context · records projected-env-000343 projected-formula-0002384 projected-formula-0002385 projected-formula-0002386

    \begin{prob}

57. Line 86 · formal-object, formula · records projected-env-000343 projected-formula-0002384 projected-formula-0002385 projected-formula-0002386

    	Show that $(m + n)_\Int = m_\Int + n_\Int$ and $m \leq n \liff m_\Int \leq n_\Int$, for any $m, n \in \Nat$.

58. Line 87 · formal-object, formula-context · records projected-env-000343 projected-formula-0002384 projected-formula-0002385 projected-formula-0002386

    \end{prob}

content/sets-functions-relations/arithmetization/rationals.tex

54 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 9 · formula-context · records projected-formula-0002387 projected-formula-0002388

   \olfileid{sfr}{arith}{rat}

2. Line 10 · formula, structure · records projected-formula-0002387 projected-formula-0002388 structure-00042

   \olsection{From $\Int$ to $\Rat$}

3. Line 16 · formula-context · records projected-formula-0002389

   \begin{enumerate}

4. Line 17 · formula, formula-context · records projected-formula-0002389 projected-formula-0002390 projected-formula-0002391 projected-formula-0002392

   	\item Every rational can be written in the form $\nicefrac{i}{j}$,

5. Line 18 · formula, formula-context · records projected-formula-0002389 projected-formula-0002390 projected-formula-0002391 projected-formula-0002392 projected-formula-0002393

   	where both $i$ and $j$ are integers but $j$ is non-zero.

6. Line 19 · formula, formula-context · records projected-formula-0002390 projected-formula-0002391 projected-formula-0002392 projected-formula-0002393 projected-formula-0002394

   	\item The information encoded in an expression $\nicefrac{i}{j}$

7. Line 20 · formula, formula-context · records projected-formula-0002393 projected-formula-0002394

   	can equally be encoded in an ordered pair $\tuple{ i, j}$.

8. Line 21 · formula-context · records projected-formula-0002394

   \end{enumerate}

9. Line 22 · formula-context · records projected-formula-0002395

   The obvious approach would be to think of the rationals \emph{as}

10. Line 23 · formula · records projected-formula-0002395

    ordered pairs drawn from $\Int \times (\Int \setminus \{0_\Int\})$. As

11. Line 24 · formula-context · records projected-formula-0002395 projected-formula-0002396 projected-formula-0002397

    before, though, that would be a bit too na\"ive, since we want

12. Line 25 · formula · records projected-formula-0002396 projected-formula-0002397

    $\nicefrac{3}{2} = \nicefrac{6}{4}$, but $\tuple{ 3, 2}\neq \tuple{ 6,

13. Line 26 · formula-context · records projected-formula-0002396 projected-formula-0002397 projected-formula-0002398

    4}$. More generally, we will want the following:

14. Line 27 · formula · records projected-formula-0002398

    \[

15. Line 28 · formula-context · records projected-formula-0002398

    	\nicefrac{a}{b} = \nicefrac{c}{d} \text{ iff } a \times d = b \times c

16. Line 29 · formula-context · records projected-formula-0002399

    \]

17. Line 30 · formula · records projected-formula-0002399

    To get this, we define an {equivalence relation} on  $\Int \times

18. Line 31 · formula-context · records projected-formula-0002399 projected-formula-0002400

    (\Int \setminus \{0_\Int\})$ thus:

19. Line 32 · formula · records projected-formula-0002400

    \[

20. Line 33 · formula-context · records projected-formula-0002400

    	\tuple{ a, b }\Ratequiv \tuple{ c, d} \text{ iff }a \times d = b \times c

21. Line 35 · formula-context · records projected-formula-0002401

    We must check that this is an equivalence relation. This is very much

22. Line 36 · formula · records projected-formula-0002401

    like the case of $\Intequiv$, and we will leave it as an exercise. 

23. Line 37 · formal-object, formula-context · records projected-env-000345 projected-formula-0002401 projected-formula-0002402

    \begin{prob}

24. Line 38 · formal-object, formula · records projected-env-000345 projected-formula-0002402

    Show that $\Ratequiv$ is an equivalence relation.

25. Line 39 · formal-object, formula-context · records projected-env-000345 projected-formula-0002402

    \end{prob}

26. Line 41 · formal-object, formula-context · records projected-env-000346 projected-formula-0002403

    \begin{defn}

27. Line 42 · formal-object, formula, formula-context · records projected-env-000346 projected-formula-0002403 projected-formula-0002404

    The rationals are the equivalence classes, under $\Ratequiv$, of pairs

28. Line 43 · formal-object, formula, formula-context · records projected-env-000346 projected-formula-0002403 projected-formula-0002404

    of integers (whose second element is non-zero). That is, $\Rat =

29. Line 44 · formal-object, formula-context · records projected-env-000346 projected-formula-0002404

    \equivclass{(\Int \times (\Int\setminus \{0_\Int\}))}{\Ratequiv}$.

30. Line 45 · formal-object · records projected-env-000346

    \end{defn}

31. Line 47 · formula-context · records projected-formula-0002405

    As with the integers, we also want to define some basic operations.

32. Line 48 · formula, formula-context · records projected-formula-0002405 projected-formula-0002406 projected-formula-0002407

    Where $\equivrep{i,j}{\Ratequiv}$ is the equivalence class under

33. Line 49 · formula, formula-context · records projected-formula-0002405 projected-formula-0002406 projected-formula-0002407 projected-formula-0002408

    $\Ratequiv$ with $\tuple{i, j}$ as !!a{element}, we say:

34. Line 50 · formal-object, formula, formula-context · records projected-env-000347 projected-formula-0002406 projected-formula-0002407 projected-formula-0002408

    \begin{align*}

35. Line 51 · formal-object, formula-context · records projected-env-000347 projected-formula-0002408

    	\equivrep{a, b}{\Ratequiv} + \equivrep{c, d}{\Ratequiv} &= \equivrep{ad + bc,  bd}{\Ratequiv}\\

36. Line 52 · formal-object · records projected-env-000347

    	\equivrep{a, b}{\Ratequiv} \times \equivrep{c, d}{\Ratequiv} &= \equivrep{a  c, b d}{\Ratequiv}.

37. Line 53 · formal-object · records projected-env-000347

    \intertext{To define $r \leq s$ on these rationals, we use the fact that 

38. Line 54 · formal-object · records projected-env-000347

    $r \le s$ iff $s - r$ is not negative, i.e., $r - s$ can be written as 

39. Line 55 · formal-object · records projected-env-000347

    $\nicefrac{i}{j}$ with $i$ non-negative and $j$~positive:}

40. Line 56 · formal-object · records projected-env-000347

    	\equivrep{a, b}{\Ratequiv} \leq \equivrep{c, d}{\Ratequiv} &\text{ iff }

41. Line 57 · formal-object · records projected-env-000347

    	\equivrep{c, d}{\Ratequiv} - \equivrep{a, b}{\Ratequiv} = 

42. Line 58 · formal-object · records projected-env-000347

    	\equivrep{i_\Int, j_\Int}{\Ratequiv}

43. Line 59 · formal-object, formula-context · records projected-env-000347 projected-formula-0002409 projected-formula-0002410

    \end{align*}

44. Line 60 · formula · records projected-formula-0002409 projected-formula-0002410

    for some $i \in \Nat$ and $0 \neq j \in \Nat$.

45. Line 63 · reference · records reference-000083

    [olref reference to sfr:arith:check:sec]

46. Line 64 · formula-context · records projected-formula-0002411 projected-formula-0002412

    indeed do!{} Finally, we want some way to treat integers \emph{as}

47. Line 65 · formula · records projected-formula-0002411 projected-formula-0002412

    rationals; so for each $i \in \Int$, we stipulate that $i_\Rat =

48. Line 66 · formula-context · records projected-formula-0002411 projected-formula-0002412

    \equivrep{i, 1_\Int}{\Ratequiv}$. Again, we check that all of this

49. Line 67 · reference · records reference-000084

    [olref reference to sfr:arith:check:sec]

50. Line 69 · formal-object, formula-context · records projected-env-000348 projected-formula-0002413 projected-formula-0002414

    \begin{prob}

51. Line 70 · formal-object, formula, formula-context · records projected-env-000348 projected-formula-0002413 projected-formula-0002414 projected-formula-0002415

    Show that $(i + j)_\Rat = i_\Rat+ j_\Rat$ and $(i \times j)_\Rat =

52. Line 71 · formal-object, formula, formula-context · records projected-env-000348 projected-formula-0002413 projected-formula-0002414 projected-formula-0002415 projected-formula-0002416

    i_\Rat \times j_\Rat$ and $i \leq j \liff i_\Rat \leq j_\Rat$, for any

53. Line 72 · formal-object, formula, formula-context · records projected-env-000348 projected-formula-0002415 projected-formula-0002416

    $i, j \in \Int$.

54. Line 73 · formal-object, formula-context · records projected-env-000348 projected-formula-0002416

    \end{prob}

content/sets-functions-relations/arithmetization/reals.tex

49 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 10 · structure · records structure-00043

   \olsection{The Real Line}

2. Line 18 · reference · records reference-000085

   [olref reference to sfr:arith:check:orderedfield]

3. Line 19 · formula-context, reference · records projected-formula-0002417 reference-000086

   [olref reference to sfr:siz::chap]

   to \olref[sfr][siz][]{chap}, you will know that there are strictly

4. Line 20 · formula · records projected-formula-0002417

   more reals than rationals, i.e., that $\cardless{\Rat}{\Real}$. This

5. Line 21 · formula-context · records projected-formula-0002417

   was first proved by Cantor. But it's been known for about two and a

6. Line 25 · formal-object, formula-context · records projected-env-000349 projected-formula-0002418 projected-formula-0002419

   \begin{thm}\ollabel{root2irrational}

7. Line 26 · formal-object, formula · records projected-env-000349 projected-formula-0002418 projected-formula-0002419

   $\sqrt{2}$ is not rational, i.e., $\sqrt{2} \notin \Rat$

8. Line 27 · formal-object, formula-context · records projected-env-000349 projected-formula-0002418 projected-formula-0002419

   \end{thm}

9. Line 29 · formula-context · records projected-formula-0002420 projected-formula-0002421

   \begin{proof}

10. Line 30 · formula, formula-context · records projected-formula-0002420 projected-formula-0002421 projected-formula-0002422 projected-formula-0002423

    Suppose, for reductio, that $\sqrt{2}$ is rational. So $\sqrt{2} =

11. Line 31 · formula, formula-context · records projected-formula-0002420 projected-formula-0002421 projected-formula-0002422 projected-formula-0002423 projected-formula-0002424 projected-formula-0002425

    \nicefrac{m}{n}$ for some natural numbers $m$ and $n$. Indeed, we can

12. Line 32 · formula, formula-context · records projected-formula-0002422 projected-formula-0002423 projected-formula-0002424 projected-formula-0002425 projected-formula-0002426

    choose $m$ and $n$ so that the fraction cannot be reduced any further.

13. Line 33 · formula, formula-context · records projected-formula-0002424 projected-formula-0002425 projected-formula-0002426

    Re-organising, $m^{2} = 2n^{2}$. From here, we can complete the proof

14. Line 34 · formula-context · records projected-formula-0002426

    in two ways:

15. Line 37 · reference · records reference-000087

    [cite reference to Conway2006]

16. Line 39 · formal-object · records projected-env-000350

    	\begin{tikzpicture}

17. Line 40 · formal-object · records projected-env-000350

    		\draw[thick] (0,0) rectangle (3,3);

18. Line 41 · formal-object · records projected-env-000350

    		\draw[thick, fill=red!50] (0,0) rectangle (2.3,2.3);

19. Line 42 · formal-object · records projected-env-000350

    		\draw[thick, fill=yellow!50] (0.7,0.7) rectangle (3, 3);

20. Line 43 · formal-object · records projected-env-000350

    		\draw[thick, fill=orange!50] (0.7,0.7) rectangle (2.3, 2.3);

21. Line 44 · formal-object, formula-context · records projected-env-000350 projected-formula-0002427

    		\draw[<->] (4, 0.7)--(4, 3);

22. Line 45 · formal-object, formula · records projected-env-000350 projected-formula-0002427

    		\node at (4.25, 1.85) (n) {$n$};

23. Line 46 · formal-object, formula-context · records projected-env-000350 projected-formula-0002427 projected-formula-0002428

    		\draw[<->] (5, 0)--(5, 3);

24. Line 47 · formal-object, formula · records projected-env-000350 projected-formula-0002428

    		\node at (5.25, 1.5) (m) {$m$};

25. Line 48 · formal-object, formula-context · records projected-env-000350 projected-formula-0002428

    	\end{tikzpicture}

26. Line 49 · formula-context · records projected-formula-0002429 projected-formula-0002430

    \end{center}

27. Line 50 · formula · records projected-formula-0002429 projected-formula-0002430

    Since $m^2 = 2n^2$, the region where the two squares of side $n$

28. Line 51 · formula-context · records projected-formula-0002429 projected-formula-0002430

    overlap has the same area as the region which neither of the two

29. Line 53 · formula-context · records projected-formula-0002431 projected-formula-0002432 projected-formula-0002433

    the area of the two unshaded squares. So where the orange square has

30. Line 54 · formula, formula-context · records projected-formula-0002431 projected-formula-0002432 projected-formula-0002433 projected-formula-0002434 projected-formula-0002435 projected-formula-0002436 projected-formula-0002437

    side $p$, and each unshaded square has side $q$, $p^2 = 2q^2$. But now

31. Line 55 · formula, formula-context · records projected-formula-0002431 projected-formula-0002432 projected-formula-0002433 projected-formula-0002434 projected-formula-0002435 projected-formula-0002436 projected-formula-0002437 projected-formula-0002438 projected-formula-0002439

    $\sqrt{2} = \nicefrac{p}{q}$, with $p < m$ and $q < n$ and $p, q \in

32. Line 56 · formula, formula-context · records projected-formula-0002434 projected-formula-0002435 projected-formula-0002436 projected-formula-0002437 projected-formula-0002438 projected-formula-0002439

    \Nat$. This contradicts the fact that $m$ and $n$ were chosen to be as

33. Line 57 · formula-context · records projected-formula-0002438 projected-formula-0002439

    small as possible.

34. Line 58 · formula-context · records projected-formula-0002440 projected-formula-0002441

35. Line 59 · formula, formula-context · records projected-formula-0002440 projected-formula-0002441 projected-formula-0002442 projected-formula-0002443

    \emph{Second, formally.} Since $m^{2} = 2n^{2}$, it follows that $m$

36. Line 60 · formula, formula-context · records projected-formula-0002440 projected-formula-0002441 projected-formula-0002442 projected-formula-0002443 projected-formula-0002444 projected-formula-0002445 projected-formula-0002446

    is even. (It is easy to show that, if $x$ is odd, then $x^2$ is odd.)

37. Line 61 · formula, formula-context · records projected-formula-0002442 projected-formula-0002443 projected-formula-0002444 projected-formula-0002445 projected-formula-0002446

    So $m = 2r$, for some $r \in \Nat$. Rearranging, $2r^2 = n^2$, 

38. Line 62 · formula-context · records projected-formula-0002444 projected-formula-0002445 projected-formula-0002446

    		%				\begin{align*}

39. Line 66 · formula-context · records projected-formula-0002447 projected-formula-0002448 projected-formula-0002449

    		%				\end{align*}

40. Line 67 · formula, formula-context · records projected-formula-0002447 projected-formula-0002448 projected-formula-0002449 projected-formula-0002450

    so $n$ is also even. So both $m$ and $n$ are even, and hence the

41. Line 68 · formula, formula-context · records projected-formula-0002447 projected-formula-0002448 projected-formula-0002449 projected-formula-0002450

    fraction $\nicefrac{m}{n}$ \emph{can} be reduced further.

42. Line 69 · formula-context · records projected-formula-0002450

    Contradiction!

43. Line 72 · reference · records reference-000088

    [olref reference to his:set:mythology:sec]

44. Line 76 · formula, formula-context · records projected-formula-0002451 projected-formula-0002452

    It is easy to see that the rationals do not have the Completeness Property. For example, consider the set of rationals less than $\sqrt{2}$, i.e.:

45. Line 77 · formula, formula-context · records projected-formula-0002451 projected-formula-0002452

    \[

46. Line 78 · formula-context · records projected-formula-0002452

    	\Setabs{p \in \Rat}{p^2 < 2 \text{ or }p < 0}

47. Line 79 · formula-context · records projected-formula-0002453 projected-formula-0002454 projected-formula-0002455 projected-formula-0002456

    \]

48. Line 80 · formula · records projected-formula-0002453 projected-formula-0002454 projected-formula-0002455 projected-formula-0002456

    This has an upper bound in the rationals; its !!{element}s< are all  smaller than $3$, for example. But what is its least upper bound? We want to say `$\sqrt{2}$'; but we have just seen that $\sqrt{2}$ is \emph{not} rational. And there is no \emph{least} rational number greater than $\sqrt{2}$. So the set has an upper bound but no least upper bound. Hence the rationals lack the Completeness Property.

49. Line 82 · formula · records projected-formula-0002457

    By contrast, the continuum ``morally ought'' to have the Completeness Property. We do not just want $\sqrt{2}$ to be a real number; we want to fill all the ``gaps'' in the rational line. Indeed, we want the continuum itself to have no ``gaps'' in it. That is just what we will get via Completeness.

content/sets-functions-relations/arithmetization/cuts.tex

81 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 9 · formula-context · records projected-formula-0002458 projected-formula-0002459

   \olfileid{sfr}{arith}{cuts}

2. Line 10 · formula, structure · records projected-formula-0002458 projected-formula-0002459 structure-00044

   \olsection{From $\Rat$ to $\Real$}

3. Line 12 · formula · records projected-formula-0002460

   In essence, the Completeness Property shows that any point $\alpha$ of

4. Line 13 · formula-context · records projected-formula-0002460 projected-formula-0002461 projected-formula-0002462

   the real line divides that line into two halves perfectly: those for

5. Line 14 · formula · records projected-formula-0002461 projected-formula-0002462

   which $\alpha$ is the least upper bound, and those for which $\alpha$

6. Line 15 · formula-context · records projected-formula-0002461 projected-formula-0002462

   is the greatest lower bound. To \emph{construct} the real numbers from

7. Line 17 · formula-context · records projected-formula-0002463

   reals as the \emph{cuts} that partition the rationals. That is, we

8. Line 18 · formula, formula-context · records projected-formula-0002463 projected-formula-0002464 projected-formula-0002465

   identify $\sqrt{2}$ with the \emph{cut} which separates the rationals

9. Line 19 · formula, formula-context · records projected-formula-0002463 projected-formula-0002464 projected-formula-0002465

   $< \sqrt{2}$ from the rationals $> \sqrt{2}$. 

10. Line 26 · formal-object, formula-context · records projected-env-000354 projected-formula-0002466

    \begin{defn}[Cut] 

11. Line 27 · formal-object, formula · records projected-env-000354 projected-formula-0002466

    A \emph{cut} $\alpha$ is any non-empty proper

12. Line 28 · formal-object, formula-context · records projected-env-000354 projected-formula-0002466 projected-formula-0002467

    initial segment of the rationals with no greatest element. That is,

13. Line 29 · formal-object, formula · records projected-env-000354 projected-formula-0002467

    $\alpha$ is a cut iff:

14. Line 30 · formal-object, formula-context · records projected-env-000354 projected-formula-0002467 projected-formula-0002468

    \begin{enumerate}

15. Line 31 · formal-object, formula, formula-context · records projected-env-000354 projected-formula-0002468 projected-formula-0002469 projected-formula-0002470 projected-formula-0002471

    	\item \emph{non-empty, proper}: $\emptyset \neq \alpha \subsetneq \Rat$

16. Line 32 · formal-object, formula, formula-context · records projected-env-000354 projected-formula-0002468 projected-formula-0002469 projected-formula-0002470 projected-formula-0002471 projected-formula-0002472 projected-formula-0002473 projected-formula-0002474

    	\item \emph{initial}: for all $p,q \in \Rat$: if $p < q \in \alpha$ then $p \in \alpha$

17. Line 33 · formal-object, formula, formula-context · records projected-env-000354 projected-formula-0002469 projected-formula-0002470 projected-formula-0002471 projected-formula-0002472 projected-formula-0002473 projected-formula-0002474

    	\item \emph{no maximum}: for all $p \in \alpha$ there is a $q \in \alpha$ such that $p < q$ 

18. Line 34 · formal-object, formula-context · records projected-env-000354 projected-formula-0002472 projected-formula-0002473 projected-formula-0002474 projected-formula-0002475

    \end{enumerate} 

19. Line 35 · formal-object, formula · records projected-env-000354 projected-formula-0002475

    Then $\Real$ is the set of cuts. 

20. Line 36 · formal-object, formula-context · records projected-env-000354 projected-formula-0002475

    \end{defn}

21. Line 38 · formula · records projected-formula-0002476

    So now we can say that $\sqrt{2} = \Setabs{p \in \Rat}{p^2 < 2\text{

22. Line 39 · formula-context · records projected-formula-0002476

    or }p < 0}$. Of course, we need to check that this \emph{is} a cut,

23. Line 40 · reference · records reference-000089

    [olref reference to sfr:arith:check:sec]

24. Line 43 · formula-context · records projected-formula-0002477

    functions and relations upon them. We begin with an easy one:

25. Line 44 · formal-object, formula · records projected-env-000355 projected-formula-0002477

    \begin{align*}

26. Line 45 · formal-object, formula-context · records projected-env-000355 projected-formula-0002477

    	\alpha \leq \beta \text{ iff }\alpha \subseteq \beta

27. Line 46 · formal-object · records projected-env-000355

    \end{align*}

28. Line 48 · formula-context · records projected-formula-0002478

    that the set of cuts has the Completeness Property. Spelled out fully,

29. Line 49 · formula, formula-context · records projected-formula-0002478 projected-formula-0002479 projected-formula-0002480 projected-formula-0002481 projected-formula-0002482

    the statement has this shape. If $S$ is a non-empty set of cuts with

30. Line 50 · formula, formula-context · records projected-formula-0002478 projected-formula-0002479 projected-formula-0002480 projected-formula-0002481 projected-formula-0002482 projected-formula-0002483 projected-formula-0002484

    an upper bound, then $S$ has a least upper bound. In more detail: there is a cut, $\lambda$, which is an upper bound for $S$, i.e.\ $(\forall \alpha \in S)\alpha \subseteq

31. Line 51 · formula, formula-context · records projected-formula-0002479 projected-formula-0002480 projected-formula-0002481 projected-formula-0002482 projected-formula-0002483 projected-formula-0002484

    \lambda$, and $\lambda$ is the least such cut, i.e.\ $(\forall \beta \in \Real)((\forall \alpha \in S)\alpha \subseteq \beta \lif \lambda \subseteq \beta)$. Now here is

32. Line 52 · formula-context · records projected-formula-0002483 projected-formula-0002484

    the proof of the result:

33. Line 54 · formal-object · records projected-env-000356

    \begin{thm}\ollabel{realcompleteness}

34. Line 55 · formal-object · records projected-env-000356

    The set of cuts has the Completeness Property. 

35. Line 56 · formal-object · records projected-env-000356

    \end{thm}

36. Line 58 · formula-context · records projected-formula-0002485 projected-formula-0002486

    \begin{proof}

37. Line 59 · formula · records projected-formula-0002485 projected-formula-0002486

    Let $S$ be any non-empty set of cuts with an upper bound. Let $\lambda

38. Line 60 · formula-context · records projected-formula-0002485 projected-formula-0002486

    = \bigcup S$. 

39. Line 61 · formula-context · records projected-formula-0002487

    %\Setabs{p \in \Rat}{(\exists \alpha \in S)p \in \alpha}$$

40. Line 62 · formula · records projected-formula-0002487

    We first claim that $\lambda$ is a cut:

41. Line 63 · formula-context · records projected-formula-0002487 projected-formula-0002488 projected-formula-0002489

    \begin{enumerate}

42. Line 64 · formula, formula-context, source-correction · records TR006-SOURCE-PROSE-002 projected-formula-0002488 projected-formula-0002489 projected-formula-0002490 projected-formula-0002491 projected-formula-0002492

    \item Since $S$ has an upper bound, at least one cut is in $S$, so

43. Line 65 · formula, formula-context · records projected-formula-0002488 projected-formula-0002489 projected-formula-0002490 projected-formula-0002491 projected-formula-0002492 projected-formula-0002493 projected-formula-0002494

    $\emptyset \neq \lambda$. Since $S$ is a set of cuts, $\lambda

44. Line 66 · formula, formula-context · records projected-formula-0002490 projected-formula-0002491 projected-formula-0002492 projected-formula-0002493 projected-formula-0002494 projected-formula-0002495 projected-formula-0002496

    \subseteq \Rat$. Since $S$ has an upper bound, some $p \in \Rat$ is

45. Line 67 · formula, formula-context · records projected-formula-0002493 projected-formula-0002494 projected-formula-0002495 projected-formula-0002496 projected-formula-0002497

    absent from every cut $\alpha \in S$. So $p\notin \lambda$, and hence

46. Line 68 · formula, formula-context · records projected-formula-0002495 projected-formula-0002496 projected-formula-0002497 projected-formula-0002498 projected-formula-0002499

    $\lambda \subsetneq \Rat$.

47. Line 69 · formula, formula-context · records projected-formula-0002497 projected-formula-0002498 projected-formula-0002499 projected-formula-0002500 projected-formula-0002501 projected-formula-0002502

    \item Suppose $p < q \in \lambda$. So there is some $\alpha \in S$

48. Line 70 · formula, formula-context · records projected-formula-0002498 projected-formula-0002499 projected-formula-0002500 projected-formula-0002501 projected-formula-0002502 projected-formula-0002503

    such that $q \in \alpha$. Since $\alpha$ is a cut, $p \in \alpha$. So

49. Line 71 · formula, formula-context · records projected-formula-0002500 projected-formula-0002501 projected-formula-0002502 projected-formula-0002503 projected-formula-0002504 projected-formula-0002505

    $p \in \lambda$.

50. Line 72 · formula, formula-context · records projected-formula-0002503 projected-formula-0002504 projected-formula-0002505 projected-formula-0002506 projected-formula-0002507 projected-formula-0002508

    \item Suppose $p \in \lambda$. So there is some $\alpha \in S$ such

51. Line 73 · formula, formula-context · records projected-formula-0002504 projected-formula-0002505 projected-formula-0002506 projected-formula-0002507 projected-formula-0002508 projected-formula-0002509 projected-formula-0002510

    that $p \in \alpha$. Since $\alpha$ is a cut, there is some $q \in

52. Line 74 · formula, formula-context · records projected-formula-0002506 projected-formula-0002507 projected-formula-0002508 projected-formula-0002509 projected-formula-0002510

    \alpha$ such that $p < q$. So $q \in \lambda$. 

53. Line 75 · formula-context · records projected-formula-0002509 projected-formula-0002510 projected-formula-0002511

    \end{enumerate}

54. Line 76 · formula, formula-context · records projected-formula-0002511 projected-formula-0002512 projected-formula-0002513 projected-formula-0002514 projected-formula-0002515 projected-formula-0002516 projected-formula-0002517 projected-formula-0002518 projected-formula-0002519 projected-formula-0002520 projected-formula-0002521 projected-formula-0002522 projected-formula-0002523

    This proves the claim. Moreover, clearly $(\forall \alpha \in S)\alpha

55. Line 77 · formula, formula-context · records projected-formula-0002511 projected-formula-0002512 projected-formula-0002513 projected-formula-0002514 projected-formula-0002515 projected-formula-0002516 projected-formula-0002517 projected-formula-0002518 projected-formula-0002519 projected-formula-0002520 projected-formula-0002521 projected-formula-0002522 projected-formula-0002523

    \subseteq \bigcup S = \lambda$, i.e.\ $\lambda$ is an upper bound on $S$. So now suppose $\beta \in \mathbb{R}$ is also an upper bound, i.e.\ $(\forall \alpha \in S)\alpha \subseteq \beta$. For any $p \in \Rat$, if $p \in \lambda$, then there is $\alpha \in S$ such that $p \in \alpha$, so that $p \in \beta$. Generalizing, $\lambda \subseteq \beta$. So $\lambda$ is the \emph{least} upper bound on $S$.

56. Line 78 · formula-context · records projected-formula-0002512 projected-formula-0002513 projected-formula-0002514 projected-formula-0002515 projected-formula-0002516 projected-formula-0002517 projected-formula-0002518 projected-formula-0002519 projected-formula-0002520 projected-formula-0002521 projected-formula-0002522 projected-formula-0002523

    \end{proof}

57. Line 85 · formula-context · records projected-formula-0002524

    Next, we must define some operations on the reals. We start by

58. Line 86 · formula, formula-context · records projected-formula-0002524 projected-formula-0002525

    embedding the rationals into the reals by stipulating that $p_\Real =

59. Line 87 · formula, formula-context · records projected-formula-0002524 projected-formula-0002525 projected-formula-0002526

    \Setabs{q \in \Rat}{q < p}$ for each $p \in \Rat$. We then define:

60. Line 88 · formal-object, formula, formula-context · records projected-env-000359 projected-formula-0002525 projected-formula-0002526

    \begin{align*}

61. Line 89 · formal-object, formula-context · records projected-env-000359 projected-formula-0002526

    	\alpha + \beta &= \Setabs{p + q}{p \in \alpha \land q \in \beta}\\

62. Line 90 · formal-object · records projected-env-000359

    %	\alpha - \beta &\defis \Setabs{p - q}{p \in \alpha \land q \in \Rat \setminus \beta}\\

63. Line 91 · formal-object · records projected-env-000359

    	\alpha \times \beta &= 

64. Line 92 · formal-object · records projected-env-000359

    	\Setabs{p \times q}{0 \leq p \in \alpha \land 0 \leq q \in \beta} \cup 0^\mathbb{R} & \text{if }\alpha, \beta \geq 0_\Real

65. Line 93 · formal-object · records projected-env-000359

    %	\alpha \div \beta &\defis 

66. Line 94 · formal-object · records projected-env-000359

    %	\Setabs{\nicefrac{p}{q}}{p \in \alpha \land q \in \Rat \setminus \beta}  & \text{if }\alpha \geq 0_\Real, \beta > 0_\Real

67. Line 95 · formal-object · records projected-env-000359

    \end{align*}

68. Line 96 · formula-context · records projected-formula-0002527

    To handle the other multiplication cases, first let: %that $0_\Real \times \alpha = 0_\Real = \alpha \times 0_\Real$, and add:

69. Line 97 · formal-object, formula · records projected-env-000360 projected-formula-0002527

    \begin{align*}

70. Line 98 · formal-object, formula-context · records projected-env-000360 projected-formula-0002527

    	-\alpha &= \Setabs{p - q}{p < 0 \land q \notin \alpha}

71. Line 99 · formal-object · records projected-env-000360

    \end{align*}

72. Line 100 · formula-context · records projected-formula-0002528

    and then stipulate:

73. Line 101 · formal-object, formula · records projected-env-000362 projected-formula-0002528

    \begin{align*}

74. Line 102 · formal-object, formula-context · records projected-env-000362 projected-formula-0002528

    	\alpha \times \beta &\defis 

75. Line 103 · formal-object · records projected-env-000362

    	\begin{cases}

76. Line 104 · formal-object · records projected-env-000362

    		\mathord{-}\alpha \times \mathord{-}\beta &\text{if }\alpha < 0_\Real\text{ and }\beta < 0_\Real\\

77. Line 105 · formal-object · records projected-env-000362

    		\mathord{-}(\mathord{-}\alpha \times \beta) &\text{if }\alpha < 0_\Real \text{ and }\beta > 0_\Real\\

78. Line 106 · formal-object · records projected-env-000362

    		\mathord{-}(\alpha \times \mathord{-}\beta) &\text{if }\alpha > 0_\Real \text{ and }\beta < 0_\Real

79. Line 107 · formal-object · records projected-env-000362

    	\end{cases}

80. Line 108 · formal-object · records projected-env-000362

    \end{align*}

81. Line 112 · reference · records reference-000090

    [olref reference to sfr:arith:check:sec]

content/sets-functions-relations/arithmetization/reflections.tex

13 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 10 · structure · records structure-00045

   \olsection{Some Philosophical Reflections}

2. Line 31 · reference · records reference-000091

   [olref reference to sfr:arith:cauchy:sec]

3. Line 68 · reference · records reference-000092

   [olref reference to sfr:arith:cauchy:sec]

4. Line 70 · reference · records reference-000093

   [olref reference to sfr:rel:ref:sec]

5. Line 78 · reference · records reference-000094

   [olref reference to sfr:rel:ref:sec]

6. Line 79 · reference · records reference-000095

   [citealt reference to Benacerraf1965]

7. Line 82 · formula-context · records projected-formula-0002529

   about our constructions. We started with the natural numbers. We then

8. Line 83 · formula, formula-context · records projected-formula-0002529 projected-formula-0002530 projected-formula-0002531

   construct the integers, and construct ``the $0$ of the integers'',

9. Line 84 · formula, formula-context · records projected-formula-0002529 projected-formula-0002530 projected-formula-0002531

   i.e., $ \equivrep{0,0}{\Intequiv}$. But $0 \neq

10. Line 85 · formula-context · records projected-formula-0002530 projected-formula-0002531

    \equivrep{0,0}{\Intequiv}$. Indeed,  given our constructions,

11. Line 87 · formula-context, reference · records projected-formula-0002532 reference-000096

    [olref reference to sfr:set:imp:sec]

    counter-intuitive. Indeed, in \olref[sfr][set][imp]{sec}, we claimed

12. Line 88 · formula · records projected-formula-0002532

    without much argument that $\Nat \subseteq \Rat$. If the constructions

13. Line 89 · formula-context · records projected-formula-0002532

    tell us exactly \emph{what} the numbers are, this claim was trivially

content/sets-functions-relations/arithmetization/checking-details.tex

147 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 11 · structure · records structure-00046

   \olsection{Ordered Rings and Fields}

2. Line 18 · formula, formula-context, reference · records projected-formula-0002533 projected-formula-0002534 reference-000097

   In \olref[int]{sec}, we defined addition and multiplication on $\Int$.

   [olref reference to sfr:arith:int:sec]

3. Line 19 · formula, formula-context · records projected-formula-0002533 projected-formula-0002534

   We want to show that, as defined, they endow $\Int$ with the structure

4. Line 20 · formula-context · records projected-formula-0002534

   we ``would want'' it to have. In particular, the structure in question

5. Line 23 · formal-object, formula-context · records projected-env-000364 projected-formula-0002535 projected-formula-0002536 projected-formula-0002537 projected-formula-0002538 projected-formula-0002539

   \begin{defn}

6. Line 24 · formal-object, formula, formula-context · records projected-env-000364 projected-formula-0002535 projected-formula-0002536 projected-formula-0002537 projected-formula-0002538 projected-formula-0002539 projected-formula-0002540

   	A \emph{commutative ring} is a set $S$, equipped with specific elements $0$ and $1$ and operations $+$ and $\times$, satisfying these eight formulas:

7. Line 25 · formal-object, formula, formula-context · records projected-env-000363 projected-env-000364 projected-formula-0002535 projected-formula-0002536 projected-formula-0002537 projected-formula-0002538 projected-formula-0002539 projected-formula-0002540

   	\begin{align*}

8. Line 26 · formal-object, formula-context · records projected-env-000363 projected-env-000364 projected-formula-0002540

   		\emph{Associativity}&&a + (b+ c) & = (a + b) + c \\

9. Line 27 · formal-object · records projected-env-000363 projected-env-000364

   		&& (a \times b) \times c & = a \times (b\times c)\\

10. Line 28 · formal-object · records projected-env-000363 projected-env-000364

    		\emph{Commutativity}&&a + b &= b+ a  \\

11. Line 29 · formal-object · records projected-env-000363 projected-env-000364

    		&&  a \times b&= b\times a\\ 

12. Line 30 · formal-object · records projected-env-000363 projected-env-000364

    		\emph{Identities}&&a + 0 &= a \\

13. Line 31 · formal-object · records projected-env-000363 projected-env-000364

    		&& a \times 1 &= a\\

14. Line 32 · formal-object · records projected-env-000363 projected-env-000364

    		\emph{Additive Inverse}&&(\exists b\in S)0&=a + b\\

15. Line 33 · formal-object · records projected-env-000363 projected-env-000364

    		\emph{Distributivity}&&a \times (b+ c ) &= (a \times b) + (a \times c)

16. Line 34 · formal-object, formula-context · records projected-env-000363 projected-env-000364 projected-formula-0002541 projected-formula-0002542 projected-formula-0002543

    	\end{align*}

17. Line 35 · formal-object, formula · records projected-env-000364 projected-formula-0002541 projected-formula-0002542 projected-formula-0002543

    	Implicitly, these are all bound with universal quantifiers restricted to $S$. And note that the elements $0$ and~$1$ here need not be the natural numbers with the same name.

18. Line 36 · formal-object, formula-context · records projected-env-000364 projected-formula-0002541 projected-formula-0002542 projected-formula-0002543

    \end{defn}

19. Line 43 · formula-context · records projected-formula-0002544 projected-formula-0002545

    \begin{proof} 

20. Line 44 · formula, formula-context · records projected-formula-0002544 projected-formula-0002545 projected-formula-0002546 projected-formula-0002547

    Fix $i, j, k \in \Int$. So there are $a_1, b_1, a_2, b_2, a_3, b_3 \in

21. Line 45 · formula, formula-context · records projected-formula-0002544 projected-formula-0002545 projected-formula-0002546 projected-formula-0002547 projected-formula-0002548

    \Nat$ such that $i = \equivrep{a_1, b_1}{}$ and $j =

22. Line 46 · formula, formula-context · records projected-formula-0002546 projected-formula-0002547 projected-formula-0002548 projected-formula-0002549

    \equivrep{a_2,b_2}{}$ and $k = \equivrep{a_3, b_3}{}$. (For

23. Line 47 · formula, formula-context · records projected-formula-0002548 projected-formula-0002549 projected-formula-0002550

    legibility, we write ``$\equivrep{x, y}{}$'' rather than

24. Line 48 · formula, formula-context · records projected-formula-0002549 projected-formula-0002550

    ``$\equivrep{x, y}{\Intequiv}$''; we'll do this throughout this

25. Line 49 · formula-context · records projected-formula-0002550 projected-formula-0002551

    section.) Now:

26. Line 50 · formal-object, formula · records projected-env-000365 projected-formula-0002551

    \begin{align*}

27. Line 51 · formal-object, formula-context · records projected-env-000365 projected-formula-0002551

    	i + (j + k) &= \equivrep{a_1, b_1}{}+(\equivrep{a_2, b_2}{} + \equivrep{a_3, b_3}{}) \\

28. Line 52 · formal-object · records projected-env-000365

    	&= \equivrep{a_1,  b_1}{} + \equivrep{a_2+a_3, b_2+b_3}{}\\

29. Line 53 · formal-object · records projected-env-000365

    	&= \equivrep{a_1 + (a_2 + a_3), b_1 + (b_2 + b_3)}{}\\

30. Line 54 · formal-object · records projected-env-000365

    	&= \equivrep{(a_1 + a_2) + a_3, (b_1 + b_2) + b_3}{}\\

31. Line 55 · formal-object · records projected-env-000365

    	&= \equivrep{a_1 + a_2, b_1 + b_2}{} + \equivrep{a_3, b_3}{}\\

32. Line 56 · formal-object · records projected-env-000365

    	&= (\equivrep{a_1, b_1}{} + \equivrep{a_2, b_2}{}) + \equivrep{a_3, b_3}{}\\

33. Line 57 · formal-object · records projected-env-000365

    	&= (i+j) + k

34. Line 58 · formal-object, formula-context · records projected-env-000365 projected-formula-0002552

    \end{align*}

35. Line 59 · formula · records projected-formula-0002552

    helping ourselves freely to the behavior of addition on $\Nat$.

36. Line 60 · formula-context · records projected-formula-0002552

    \end{proof}

37. Line 64 · formula-context · records projected-formula-0002553 projected-formula-0002554 projected-formula-0002555

    \begin{proof}

38. Line 65 · formula, formula-context · records projected-formula-0002553 projected-formula-0002554 projected-formula-0002555 projected-formula-0002556

    Fix $i \in \Int$, so that $i = \equivrep{a,b}{}$ for some $a,b \in

39. Line 66 · formula, formula-context · records projected-formula-0002553 projected-formula-0002554 projected-formula-0002555 projected-formula-0002556 projected-formula-0002557

    \Nat$. Let $j = \equivrep{b,a}{} \in \Int$. Helping ourselves to the

40. Line 67 · formula, formula-context · records projected-formula-0002556 projected-formula-0002557 projected-formula-0002558

    behaviour of the naturals, $(a+b) + 0 = 0 + (a+b)$, so that

41. Line 68 · formula, formula-context · records projected-formula-0002557 projected-formula-0002558 projected-formula-0002559 projected-formula-0002560

    $\tuple{a+b, b+a} \sim_\Int \tuple{0,0}$ by definition, and hence

42. Line 69 · formula, formula-context · records projected-formula-0002558 projected-formula-0002559 projected-formula-0002560

    $\equivrep{a+b, b+a}{} = \equivrep{0, 0}{} = 0_\Int$. So now $i + j =

43. Line 70 · formula-context · records projected-formula-0002559 projected-formula-0002560

    \equivrep{a,b}{}+\equivrep{b,a}{}=\equivrep{a+b, b+a}{}= \equivrep{0,

44. Line 76 · formula-context · records projected-formula-0002561 projected-formula-0002562

    \begin{proof}

45. Line 77 · formula, formula-context · records projected-formula-0002561 projected-formula-0002562 projected-formula-0002563

    As above, fix $i = \equivrep{a_1, b_1}{}$ and $j =

46. Line 78 · formula, formula-context · records projected-formula-0002561 projected-formula-0002562 projected-formula-0002563 projected-formula-0002564

    \equivrep{a_2,b_2}{}$ and $k = \equivrep{a_3, b_3}{}$. Now:

47. Line 79 · formal-object, formula, formula-context · records projected-env-000368 projected-formula-0002563 projected-formula-0002564

    \begin{align*}

48. Line 80 · formal-object, formula-context · records projected-env-000368 projected-formula-0002564

    	i \times (j + k) 

49. Line 81 · formal-object · records projected-env-000368

    	&= \equivrep{a_1, b_1}{} \times (\equivrep{a_2,b_2}{} + \equivrep{a_3, b_3}{})\\

50. Line 82 · formal-object · records projected-env-000368

    	&= \equivrep{a_1, b_1}{} \times \equivrep{a_2 + a_3,b_2+b_3}{}\\

51. Line 83 · formal-object · records projected-env-000368

    	&= \equivrep{a_1  (a_2 + a_3) + b_1  (b_2+b_3), a_1  (b_2 + b_3) + b_1 (a_2 + a_3)}{}\\

52. Line 84 · formal-object · records projected-env-000368

    	&= \equivrep{a_1 a_2 + a_1a_3 + b_1 b_2+b_1b_3, a_1 b_2 + a_1b_3 + a_2b_1 + a_3b_1}{}\\		

53. Line 85 · formal-object · records projected-env-000368

    %		&= \equivrep{a_1 a_2 + b_1b_2 + a_1a_3 + b_1 b_2+b_1b_3, a_1 b_2 + a_1b_3 + a_2b_1 + a_3b_1}{}\\		

54. Line 86 · formal-object · records projected-env-000368

    	&= \equivrep{a_1a_2 + b_1b_2, a_1b_2 + a_2b_1}{} + \equivrep{a_1a_3 + b_1b_3, a_1b_3 + a_3b_1}{}\\

55. Line 87 · formal-object · records projected-env-000368

    	&= (\equivrep{a_1, b_1}{} \times \equivrep{a_2,b_2}{}) + (\equivrep{a_1, b_1}{} \times  \equivrep{a_3, b_3}{})\\

56. Line 88 · formal-object · records projected-env-000368

    	&= (i \times j) + (i \times k)

57. Line 89 · formal-object · records projected-env-000368

    \end{align*}

58. Line 92 · formula-context · records projected-formula-0002565

    We leave it as an exercise to prove the remaining five conditions.

59. Line 93 · formula · records projected-formula-0002565

    Having done that, we have shown that $\Int$ constitutes a commutative

60. Line 94 · formula-context · records projected-formula-0002565

    ring, i.e., that addition and multiplication (as defined) behave as

61. Line 97 · formal-object, formula-context · records projected-env-000370 projected-formula-0002566

    \begin{prob}

62. Line 98 · formal-object, formula · records projected-env-000370 projected-formula-0002566

    Prove that $\Int$ is a commutative ring.

63. Line 99 · formal-object, formula-context · records projected-env-000370 projected-formula-0002566

    \end{prob}

64. Line 101 · formula-context · records projected-formula-0002567 projected-formula-0002568

    But our task is not over. As well as defining addition and

65. Line 102 · formula · records projected-formula-0002567 projected-formula-0002568

    multiplication over $\Int$, we defined an ordering relation, $\leq$,

66. Line 103 · formula-context · records projected-formula-0002567 projected-formula-0002568 projected-formula-0002569

    and we must check that this behaves as it should. In more detail, we

67. Line 104 · formula · records projected-formula-0002569

    must show that $\Int$ constitutes an \emph{ordered} ring.\footnote{Recall

68. Line 105 · formula-context, reference · records projected-formula-0002569 reference-000098

    	from \olref[sfr][rel][ord]{def:linearorder} that a total order

    [olref reference to sfr:rel:ord:def:linearorder]

69. Line 107 · formula-context · records projected-formula-0002570 projected-formula-0002571 projected-formula-0002572

    	In the context of order relations, connectedness is sometimes called

70. Line 108 · formula · records projected-formula-0002570 projected-formula-0002571 projected-formula-0002572

    	\emph{trichotomy}, since for any $a$ and $b$ we have $a \leq b \lor a

71. Line 109 · formula-context · records projected-formula-0002570 projected-formula-0002571 projected-formula-0002572

    	= b \lor a \geq b$.} 

72. Line 111 · formal-object · records projected-env-000372

    \begin{defn}

73. Line 112 · formal-object, formula-context · records projected-env-000372 projected-formula-0002573

    An \emph{ordered ring} is a commutative ring which is also equipped

74. Line 113 · formal-object, formula, formula-context · records projected-env-000372 projected-formula-0002573 projected-formula-0002574

    with a total order relation, $\leq$, such that:

75. Line 114 · formal-object, formula, formula-context · records projected-env-000371 projected-env-000372 projected-formula-0002573 projected-formula-0002574

    \begin{align*}

76. Line 115 · formal-object, formula-context · records projected-env-000371 projected-env-000372 projected-formula-0002574

    	a \leq b &\lif a + c \leq b + c\\

77. Line 116 · formal-object · records projected-env-000371 projected-env-000372

    	(a \leq b \land 0 \leq c) &\lif a \times c \leq b \times c

78. Line 117 · formal-object · records projected-env-000371 projected-env-000372

    \end{align*}

79. Line 118 · formal-object · records projected-env-000372

    \end{defn}

80. Line 120 · formal-object, formula-context · records projected-env-000373 projected-formula-0002575

    \begin{prob}

81. Line 121 · formal-object, formula · records projected-env-000373 projected-formula-0002575

    Prove that $\Int$ is an ordered ring. 

82. Line 122 · formal-object, formula-context · records projected-env-000373 projected-formula-0002575

    \end{prob}

83. Line 124 · formula · records projected-formula-0002576

    As before, it is laborious but routine to show that~$\Int$, as

84. Line 125 · formula-context · records projected-formula-0002576

    constructed, is an ordered ring. We will leave that to you.

85. Line 129 · formula-context · records projected-formula-0002577 projected-formula-0002578 projected-formula-0002579

    rationals form an ordered \emph{field}, under our given definitions of

86. Line 130 · formula · records projected-formula-0002577 projected-formula-0002578 projected-formula-0002579

    $+$, $\times$, and $\leq$:

87. Line 131 · formal-object, formula-context · records projected-env-000375 projected-formula-0002577 projected-formula-0002578 projected-formula-0002579

    \begin{defn}\ollabel{orderedfield}

88. Line 132 · formal-object, formula-context · records projected-env-000375 projected-formula-0002580

    An \emph{ordered field} is an ordered ring which also satisfies:

89. Line 133 · formal-object, formula · records projected-env-000374 projected-env-000375 projected-formula-0002580

    \begin{align*}

90. Line 134 · formal-object, formula-context · records projected-env-000374 projected-env-000375 projected-formula-0002580

    	\emph{Multiplicative Inverse}& & (\forall a \in S \setminus \{0\})(\exists b \in S) a\times b& = 1

91. Line 135 · formal-object · records projected-env-000374 projected-env-000375

    \end{align*}

92. Line 136 · formal-object · records projected-env-000375

    \end{defn}

93. Line 138 · formula, formula-context · records projected-formula-0002581 projected-formula-0002582

    Once you have shown that $\Int$ constitutes an ordered ring, it is

94. Line 139 · formula, formula-context · records projected-formula-0002581 projected-formula-0002582

    easy but laborious to show that $\Rat$ constitutes an ordered field.

95. Line 141 · formal-object, formula-context · records projected-env-000376 projected-formula-0002583

    \begin{prob}

96. Line 142 · formal-object, formula · records projected-env-000376 projected-formula-0002583

    Prove that $\Rat$ is an ordered field.

97. Line 143 · formal-object, formula-context · records projected-env-000376 projected-formula-0002583

    \end{prob}

98. Line 145 · formula-context · records projected-formula-0002584

    Having dealt with the integers and the rationals, it only remains to

99. Line 146 · formula · records projected-formula-0002584

    deal with the reals. In particular, we need to show that $\Real$

100. Line 147 · formula-context · records projected-formula-0002584

     constitutes a \emph{complete} ordered field, i.e., an ordered field

101. Line 148 · formula-context, reference · records projected-formula-0002585 reference-000099

     [olref reference to sfr:arith:cuts:realcompleteness]

     with the Completeness Property. Now, \olref[cuts]{realcompleteness}

102. Line 149 · formula, formula-context · records projected-formula-0002585 projected-formula-0002586

     established that $\Real$ has the Completeness Property. However, it

103. Line 150 · formula, formula-context, source-correction · records TR006-SOURCE-PROSE-003 projected-formula-0002585 projected-formula-0002586

     remains to run through the (tedious) of checking that $\Real$ is an

104. Line 151 · formula-context · records projected-formula-0002586

     ordered field. 

105. Line 154 · formula-context · records projected-formula-0002587

     check some more ``immediate'' things. For example, we need a guarantee

106. Line 155 · formula, formula-context · records projected-formula-0002587 projected-formula-0002588 projected-formula-0002589

     that $\alpha + \beta$, as defined, is indeed a \emph{cut}, for any

107. Line 156 · formula, formula-context · records projected-formula-0002587 projected-formula-0002588 projected-formula-0002589

     cuts $\alpha$ and $\beta$. Here is a proof of that fact:

108. Line 158 · formula-context · records projected-formula-0002590 projected-formula-0002591 projected-formula-0002592

     \begin{proof}	

109. Line 159 · formula · records projected-formula-0002590 projected-formula-0002591 projected-formula-0002592

     Since $\alpha$ and $\beta$ are both cuts, $\alpha + \beta = \Setabs{p

110. Line 160 · formula-context · records projected-formula-0002590 projected-formula-0002591 projected-formula-0002592 projected-formula-0002593 projected-formula-0002594 projected-formula-0002595 projected-formula-0002596

     + q}{p \in \alpha \land q \in \beta}$ is a non-empty proper subset of

111. Line 161 · formula, formula-context · records projected-formula-0002593 projected-formula-0002594 projected-formula-0002595 projected-formula-0002596 projected-formula-0002597 projected-formula-0002598 projected-formula-0002599

     $\Rat$. Now suppose $x < p + q$ for some $p \in \alpha$ and $q \in \beta$.

112. Line 162 · formula, formula-context · records projected-formula-0002593 projected-formula-0002594 projected-formula-0002595 projected-formula-0002596 projected-formula-0002597 projected-formula-0002598 projected-formula-0002599 projected-formula-0002600 projected-formula-0002601

     Then $x - p < q$, so $x - p \in \beta$, and $x = p + (x - p) \in

113. Line 163 · formula, formula-context · records projected-formula-0002597 projected-formula-0002598 projected-formula-0002599 projected-formula-0002600 projected-formula-0002601 projected-formula-0002602 projected-formula-0002603

     \alpha + \beta$. So $\alpha + \beta$ is an initial segment of $\Rat$.

114. Line 164 · formula, formula-context · records projected-formula-0002600 projected-formula-0002601 projected-formula-0002602 projected-formula-0002603 projected-formula-0002604 projected-formula-0002605 projected-formula-0002606

     Finally, for any $p + q \in \alpha + \beta$, since $\alpha$ and

115. Line 165 · formula, formula-context · records projected-formula-0002602 projected-formula-0002603 projected-formula-0002604 projected-formula-0002605 projected-formula-0002606 projected-formula-0002607 projected-formula-0002608 projected-formula-0002609

     $\beta$ are both cuts, there are $p_1 \in \alpha$ and $q_1 \in \beta$

116. Line 166 · formula, formula-context · records projected-formula-0002604 projected-formula-0002605 projected-formula-0002606 projected-formula-0002607 projected-formula-0002608 projected-formula-0002609 projected-formula-0002610

     such that $p < p_1$ and $q < q_1$; so $p + q < p_1 + q_1 \in \alpha +

117. Line 167 · formula, formula-context · records projected-formula-0002607 projected-formula-0002608 projected-formula-0002609 projected-formula-0002610

     \beta$; so $\alpha + \beta$ has no maximum. 

118. Line 168 · formula-context · records projected-formula-0002610

     \end{proof}

119. Line 170 · formula, formula-context · records projected-formula-0002611 projected-formula-0002612 projected-formula-0002613

     Similar efforts will allow you to check that $\alpha - \beta$ and

120. Line 171 · formula, formula-context · records projected-formula-0002611 projected-formula-0002612 projected-formula-0002613 projected-formula-0002614

     $\alpha \times \beta$ and $\alpha \div \beta$ are cuts (in the last

121. Line 172 · formula, formula-context · records projected-formula-0002612 projected-formula-0002613 projected-formula-0002614

     case, ignoring the case where $\beta$ is the zero-cut). Again, though,

122. Line 173 · formula-context · records projected-formula-0002614

     we will simply leave this to you. 

123. Line 175 · formal-object, formula-context · records projected-env-000378 projected-formula-0002615

     \begin{prob}

124. Line 176 · formal-object, formula · records projected-env-000378 projected-formula-0002615

     Prove that $\Real$ is an ordered field.

125. Line 177 · formal-object, formula-context · records projected-env-000378 projected-formula-0002615

     \end{prob}

126. Line 179 · formula-context · records projected-formula-0002616

     But here is a small loose end to tidy up. In

127. Line 180 · formula, reference · records projected-formula-0002616 reference-000100

     [olref reference to sfr:arith:cuts:sec]

     \olref[cuts]{sec}, we suggest that we can take $\sqrt{2} =

128. Line 181 · formula-context · records projected-formula-0002616

     \Setabs{p \in \Rat}{p < 0 \text{ or }p^2 < 2}$. But we do need to show

129. Line 186 · formula-context · records projected-formula-0002617 projected-formula-0002618 projected-formula-0002619

     it suffices to show that it has no maximum. In particular, it suffices

130. Line 187 · formula, formula-context · records projected-formula-0002617 projected-formula-0002618 projected-formula-0002619 projected-formula-0002620 projected-formula-0002621 projected-formula-0002622

     to show that, where $p$ is a positive rational with $p^2 < 2$ and $q =

131. Line 188 · formula, formula-context · records projected-formula-0002617 projected-formula-0002618 projected-formula-0002619 projected-formula-0002620 projected-formula-0002621 projected-formula-0002622

     \frac{2p+2}{p+2}$, both $p < q$ and $q^2 < 2$. To see that $p < q$,

132. Line 189 · formula-context · records projected-formula-0002620 projected-formula-0002621 projected-formula-0002622 projected-formula-0002623

     just note:

133. Line 190 · formal-object, formula · records projected-env-000379 projected-formula-0002623

     \begin{align*}

134. Line 191 · formal-object, formula-context · records projected-env-000379 projected-formula-0002623

     	p^2 &< 2\\

135. Line 192 · formal-object · records projected-env-000379

     	p^2 + 2p &< 2 + 2p\\

136. Line 193 · formal-object · records projected-env-000379

     	p(p + 2) &< 2 + 2p\\

137. Line 194 · formal-object · records projected-env-000379

     	p &< \tfrac{2+2p}{p+2} = q

138. Line 195 · formal-object, formula-context · records projected-env-000379 projected-formula-0002624

     \end{align*}

139. Line 196 · formula, formula-context · records projected-formula-0002624 projected-formula-0002625

     To see that $q^2 < 2$, just note:

140. Line 197 · formal-object, formula, formula-context · records projected-env-000380 projected-formula-0002624 projected-formula-0002625

     \begin{align*}

141. Line 198 · formal-object, formula-context · records projected-env-000380 projected-formula-0002625

     	p^2 &< 2\\

142. Line 199 · formal-object · records projected-env-000380

     	2p^2 + 4p + 2 &< p^2 + 4p+ 4\\

143. Line 200 · formal-object · records projected-env-000380

     	4p^2 + 8p + 4 &< 2(p^2 + 4p + 4)\\

144. Line 201 · formal-object · records projected-env-000380

     	(2p+2)^2 & <2(p+2)^2\\

145. Line 202 · formal-object · records projected-env-000380

     	\tfrac{(2p+2)^2}{(p+2)^2} &< 2\\

146. Line 203 · formal-object · records projected-env-000380

     	q^2 &< 2

147. Line 204 · formal-object · records projected-env-000380

     \end{align*}

content/sets-functions-relations/arithmetization/cauchy.tex

154 exact source-coordinate anchors materialized from the accepted slice ledgers.

1. Line 11 · structure · records structure-00047

   \olsection{Appendix: the Reals as Cauchy Sequences}

2. Line 13 · reference · records reference-000101

   [olref reference to sfr:arith:cuts:sec]

3. Line 18 · reference · records reference-000102

   [citeauthor reference to OConnorRobertson:RN]

4. Line 19 · reference · records reference-000103

   [citeyear reference to OConnorRobertson:RN]

5. Line 23 · formula-context · records projected-formula-0002626

   each real in terms of its decimal expansion. Thus even an irrational

6. Line 24 · formula, formula-context · records projected-formula-0002626 projected-formula-0002627

   number, like $\sqrt{2}$, has a nice decimal expansion, beginning:

7. Line 25 · formula, formula-context · records projected-formula-0002626 projected-formula-0002627

   \[

8. Line 26 · formula-context · records projected-formula-0002627

   	1.41421356237\ldots

9. Line 28 · formula-context · records projected-formula-0002628 projected-formula-0002629

   It is very easy to model decimal expansions in set theory: simply

10. Line 29 · formula, formula-context · records projected-formula-0002628 projected-formula-0002629 projected-formula-0002630

    consider them as functions $d \colon \Nat \to \Nat$, where $d(n)$ is

11. Line 30 · formula, formula-context · records projected-formula-0002628 projected-formula-0002629 projected-formula-0002630

    the $n$th decimal place that we are interested in. We will then need a

12. Line 31 · formula-context · records projected-formula-0002630 projected-formula-0002631

    bit of tweak, to handle the bit of the real number that comes before

13. Line 32 · formula, formula-context · records projected-formula-0002631 projected-formula-0002632

    the decimal point (here, just $1$). We will also need a further tweak

14. Line 33 · formula, formula-context · records projected-formula-0002631 projected-formula-0002632

    (an equivalence relation) to guarantee that, for example, $0.999\ldots

15. Line 34 · formula-context · records projected-formula-0002632

    = 1$. But it is not difficult to offer a perfectly rigorous

16. Line 39 · formula-context, reference · records projected-formula-0002633 reference-000104

    [citealt reference to KatzKatz2012]

    \citealt{KatzKatz2012}.) But here is a closely related thought.

17. Line 40 · formula · records projected-formula-0002633

    Instead of treating $\sqrt{2}$'s decimal expansion directly, we can

18. Line 41 · formula-context · records projected-formula-0002633 projected-formula-0002634

    instead consider a  \emph{sequence} of increasingly accurate rational

19. Line 42 · formula · records projected-formula-0002634

    approximations to $\sqrt{2}$, by considering the increasingly precise

20. Line 43 · formula-context · records projected-formula-0002634 projected-formula-0002635

    expansions: 

21. Line 44 · formula · records projected-formula-0002635

    \[

22. Line 45 · formula-context · records projected-formula-0002635

    1, 1.4, 1.414, 1.4142, 1.41421,\ldots

23. Line 49 · formula-context · records projected-formula-0002636 projected-formula-0002637 projected-formula-0002638 projected-formula-0002639

    insights (akin to the realisations that we used when constructing

24. Line 50 · formula · records projected-formula-0002636 projected-formula-0002637 projected-formula-0002638 projected-formula-0002639

    $\Rat$ from $\Int$, or $\Int$ from $\Nat$). The basic insights are

25. Line 51 · formula-context · records projected-formula-0002636 projected-formula-0002637 projected-formula-0002638 projected-formula-0002639

    these:

26. Line 58 · formula-context · records projected-formula-0002640 projected-formula-0002641 projected-formula-0002642 projected-formula-0002643

    	\item A sequence of rational numbers can be thought of as a

27. Line 59 · formula · records projected-formula-0002640 projected-formula-0002641 projected-formula-0002642 projected-formula-0002643

    	function from $\Nat$ to $\Rat$; just let $f(n)$ be the $n$th

28. Line 60 · formula-context · records projected-formula-0002640 projected-formula-0002641 projected-formula-0002642 projected-formula-0002643

    	rational in the sequence.

29. Line 61 · formula-context · records projected-formula-0002644 projected-formula-0002645

    \end{enumerate}

30. Line 62 · formula · records projected-formula-0002644 projected-formula-0002645

    Of course, not just \emph{any} function from $\Nat$ to $\Rat$ will

31. Line 63 · formula-context · records projected-formula-0002644 projected-formula-0002645 projected-formula-0002646

    give us a real number. For instance, consider this function:

32. Line 64 · formula · records projected-formula-0002646

    \[

33. Line 65 · formula-context · records projected-formula-0002646

    	f(n) =\begin{cases}

34. Line 69 · formula-context · records projected-formula-0002647

    \]

35. Line 70 · formula · records projected-formula-0002647

    Essentially the worry here is that the sequence $0,1,0,1,0,1,0,\ldots$

36. Line 71 · formula-context · records projected-formula-0002647

    doesn't seem to ``hone in'' on any real. So: to ensure that we

37. Line 76 · formula-context, reference · records projected-formula-0002648 reference-000105

    [olref reference to his:set:limits:sec]

    \olref[his][set][limits]{sec}. But we cannot use \emph{quite} the same

38. Line 77 · formula · records projected-formula-0002648

    definition as we used there. The expression ``$(\forall \epsilon>0)$''

39. Line 78 · formula-context · records projected-formula-0002648

    there tacitly involved quantification over the real numbers; and we

40. Line 83 · formal-object, formula-context · records projected-env-000384 projected-formula-0002649

    \begin{defn}\ollabel{def:CauchySequence}

41. Line 84 · formal-object, formula, formula-context · records projected-env-000384 projected-formula-0002649 projected-formula-0002650 projected-formula-0002651

      A function $f: \Nat \to \Rat$ is a \emph{Cauchy sequence} iff for

42. Line 85 · formal-object, formula, formula-context · records projected-env-000384 projected-formula-0002649 projected-formula-0002650 projected-formula-0002651

      any positive $\epsilon \in \Rat$ we have that $(\exists \ell \in

43. Line 86 · formal-object, formula-context · records projected-env-000384 projected-formula-0002650 projected-formula-0002651

      \Nat)(\forall m, n > \ell)|f(m) - f(n)| < \epsilon$.

44. Line 87 · formal-object · records projected-env-000384

    \end{defn}

45. Line 89 · formula-context · records projected-formula-0002652

    The general idea of a limit is the same as before: if you want a

46. Line 90 · formula, formula-context · records projected-formula-0002652 projected-formula-0002653

    certain level of precision (measured by~$\epsilon$), there is a

47. Line 91 · formula, formula-context · records projected-formula-0002652 projected-formula-0002653 projected-formula-0002654 projected-formula-0002655 projected-formula-0002656 projected-formula-0002657

    ``region'' to look in (any input greater than~$\ell$). And it is easy

48. Line 92 · formula, formula-context · records projected-formula-0002653 projected-formula-0002654 projected-formula-0002655 projected-formula-0002656 projected-formula-0002657 projected-formula-0002658 projected-formula-0002659

    to see that our sequence $1$, $1.4$, $1.414$, $1.4142$,

49. Line 93 · formula, formula-context · records projected-formula-0002654 projected-formula-0002655 projected-formula-0002656 projected-formula-0002657 projected-formula-0002658 projected-formula-0002659 projected-formula-0002660

    $1.41421$\ldots has a limit: if you want to approximate $\sqrt{2}$ to

50. Line 94 · formula, formula-context · records projected-formula-0002658 projected-formula-0002659 projected-formula-0002660 projected-formula-0002661

    within an error of $\nicefrac{1}{10^{n}}$, then just look to any entry

51. Line 95 · formula, formula-context · records projected-formula-0002660 projected-formula-0002661

    after the $n$th.

52. Line 97 · formula-context · records projected-formula-0002662

    The obvious thought, then, would be to say that a real number just

53. Line 98 · formula, formula-context · records projected-formula-0002662 projected-formula-0002663

    \emph{is} any Cauchy sequence. But, as in the constructions of $\Int$

54. Line 99 · formula, formula-context · records projected-formula-0002662 projected-formula-0002663

    and $\Rat$, this would be too na\"{i}ve: for any given real number,

55. Line 100 · formula-context · records projected-formula-0002663 projected-formula-0002664

    multiple different Cauchy sequences indicate that real number. A

56. Line 101 · formula, formula-context, source-correction · records TR006-SOURCE-PROSE-004 projected-formula-0002664 projected-formula-0002665 projected-formula-0002666 projected-formula-0002667

    simple way to see this as follows. Given a Cauchy sequence~$f$, define

57. Line 102 · formula, formula-context · records projected-formula-0002664 projected-formula-0002665 projected-formula-0002666 projected-formula-0002667

    $g$ to be exactly the same function as~$f$, except that $g(0)\neq

58. Line 103 · formula-context · records projected-formula-0002665 projected-formula-0002666 projected-formula-0002667

    f(0)$. Since the two sequences agree everywhere after the first

59. Line 105 · reference · records reference-000106

    [olref reference to sfr:arith:cauchy:def:CauchySequence]

60. Line 110 · formula-context, source-correction · records TR006-SOURCE-PROSE-005 projected-formula-0002668

    Cauchy sequences, and identify real numbers with equivalence

61. Line 111 · formula, formula-context, source-correction · records TR006-SOURCE-PROSE-005 projected-formula-0002668 projected-formula-0002669 projected-formula-0002670

    relations. First we need the idea of a function which tends to $0$ in

62. Line 112 · formula, formula-context · records projected-formula-0002668 projected-formula-0002669 projected-formula-0002670 projected-formula-0002671 projected-formula-0002672

    the limit. For any function $h : \Nat \to \Rat$, say that \emph{$h$

63. Line 113 · formula, formula-context · records projected-formula-0002669 projected-formula-0002670 projected-formula-0002671 projected-formula-0002672 projected-formula-0002673

    tends to $0$} iff for any positive $\epsilon \in \Rat$ we have that

64. Line 114 · formula, formula-context · records projected-formula-0002671 projected-formula-0002672 projected-formula-0002673 projected-formula-0002674

    $(\exists \ell \in \Nat)(\forall n > \ell)|h(n)| <

65. Line 115 · formula, formula-context · records projected-formula-0002673 projected-formula-0002674

    \epsilon$.\footnote{Compare this with the definition of $\lim_{x

66. Line 116 · formula-context · records projected-formula-0002674 projected-formula-0002675 projected-formula-0002676

    \mathord{\rightarrow}\infty}f(x) = 0$ in

67. Line 117 · formula, formula-context, reference · records projected-formula-0002675 projected-formula-0002676 projected-formula-0002677 projected-formula-0002678 reference-000107

    [olref reference to his:set:limits:sec]

    \olref[his][set][limits]{sec}.} Further, where $f$ and $g$ are

68. Line 118 · formula, formula-context · records projected-formula-0002675 projected-formula-0002676 projected-formula-0002677 projected-formula-0002678 projected-formula-0002679

    functions $\Nat \to \Rat$, let $(f-g)(n) = f(n) - g(n)$. Now define:

69. Line 119 · formula, formula-context · records projected-formula-0002677 projected-formula-0002678 projected-formula-0002679

    \[

70. Line 120 · formula-context · records projected-formula-0002679

    	f \Realequiv g \text{ iff $(f-g)$ tends to $0$}.

71. Line 121 · formula-context · records projected-formula-0002680

    \]

72. Line 122 · formula · records projected-formula-0002680

    We need to check that $\Realequiv$ is an equivalence relation; and it

73. Line 123 · formula-context · records projected-formula-0002680 projected-formula-0002681 projected-formula-0002682

    is. We can then, if we like, define the reals as the equivalence

74. Line 124 · formula · records projected-formula-0002681 projected-formula-0002682

    classes, under $\Realequiv$, of all Cauchy sequences from $\Nat \to

75. Line 125 · formula-context · records projected-formula-0002681 projected-formula-0002682

    \Rat$.

76. Line 127 · formal-object, formula-context · records projected-env-000385 projected-formula-0002683 projected-formula-0002684 projected-formula-0002685

    \begin{prob}

77. Line 128 · formal-object, formula · records projected-env-000385 projected-formula-0002683 projected-formula-0002684 projected-formula-0002685

    Let $f(n) = 0$ for every $n$. Let $g(n) = \frac{1}{(n+1)^2}$. Show

78. Line 129 · formal-object, formula-context · records projected-env-000385 projected-formula-0002683 projected-formula-0002684 projected-formula-0002685 projected-formula-0002686 projected-formula-0002687

    that both are Cauchy sequences, and indeed that the limit of both

79. Line 130 · formal-object, formula · records projected-env-000385 projected-formula-0002686 projected-formula-0002687

    functions is $0$, so that also $f \sim_\Real g$. 

80. Line 131 · formal-object, formula-context · records projected-env-000385 projected-formula-0002686 projected-formula-0002687

    \end{prob}

81. Line 133 · formula, formula-context · records projected-formula-0002688 projected-formula-0002689

    Having done this, we shall as usual write $\equivrep{f}{\Realequiv}$

82. Line 134 · formula, formula-context · records projected-formula-0002688 projected-formula-0002689

    for the equivalence class with $f$ as !!a{element}. However, to keep

83. Line 135 · formula-context · records projected-formula-0002689 projected-formula-0002690 projected-formula-0002691

    things readable, in what follows we will drop the subscript and write

84. Line 136 · formula, formula-context · records projected-formula-0002690 projected-formula-0002691 projected-formula-0002692 projected-formula-0002693

    just $\equivrep{f}{}$. We also stipulate that, for each $q \in \Rat$,

85. Line 137 · formula, formula-context · records projected-formula-0002690 projected-formula-0002691 projected-formula-0002692 projected-formula-0002693 projected-formula-0002694 projected-formula-0002695

    we have $q_{\Real} = \equivrep{c_{q}}{}$, where $c_{q}$ is the

86. Line 138 · formula, formula-context · records projected-formula-0002692 projected-formula-0002693 projected-formula-0002694 projected-formula-0002695

    constant function $c_q(n) = q$ for all $n \in \Nat$. We then define

87. Line 139 · formula-context · records projected-formula-0002694 projected-formula-0002695 projected-formula-0002696

    basic relations and operations on the reals, e.g.:

88. Line 140 · formal-object, formula · records projected-env-000386 projected-formula-0002696

    \begin{align*}

89. Line 141 · formal-object, formula-context · records projected-env-000386 projected-formula-0002696

    	\equivrep{f}{} + \equivrep{g}{} &= 	\equivrep{(f + g)}{} \\

90. Line 142 · formal-object · records projected-env-000386

    	\equivrep{f}{} \times 	\equivrep{g}{} &= \equivrep{(f \times g)}{} 

91. Line 143 · formal-object, formula-context · records projected-env-000386 projected-formula-0002697 projected-formula-0002698

    \end{align*}

92. Line 144 · formula, formula-context · records projected-formula-0002697 projected-formula-0002698 projected-formula-0002699

    where $(f + g)(n) = f(n) + g(n)$ and $(f \times g)(n) = f(n) \times

93. Line 145 · formula, formula-context · records projected-formula-0002697 projected-formula-0002698 projected-formula-0002699 projected-formula-0002700 projected-formula-0002701 projected-formula-0002702 projected-formula-0002703

    g(n)$. Of course, we also need to check that each of  $(f + g)$,

94. Line 146 · formula, formula-context · records projected-formula-0002699 projected-formula-0002700 projected-formula-0002701 projected-formula-0002702 projected-formula-0002703

    $(f-g)$ and $(f\times g)$ are Cauchy sequences when $f$ and $g$ are;

95. Line 147 · formula-context · records projected-formula-0002700 projected-formula-0002701 projected-formula-0002702 projected-formula-0002703

    but they are, and we leave this to you.

96. Line 149 · formula, formula-context, source-correction · records TR006-SOURCE-PROSE-006 projected-formula-0002704 projected-formula-0002705 projected-formula-0002706

    Finally, we define we a notion of order. Say $\equivrep{f}{}$ is

97. Line 150 · formula, formula-context, source-correction · records TR006-SOURCE-FORMULA-007 projected-formula-0002704 projected-formula-0002705 projected-formula-0002706 projected-formula-0002707

    \emph{positive} iff both $\equivrep{f}{}\neq 0_\Rat$ and $(\exists

98. Line 151 · formula, formula-context · records projected-formula-0002705 projected-formula-0002706 projected-formula-0002707 projected-formula-0002708

    \ell \in \Nat)(\forall n > \ell)0 < f(n)$. Then say $\equivrep{f}{} <

99. Line 152 · formula, formula-context · records projected-formula-0002707 projected-formula-0002708

    \equivrep{g}{}$ iff $\equivrep{(g - f)}{}$ is positive. We have to

100. Line 153 · formula-context · records projected-formula-0002708

     check that this is well-defined (i.e., that it does not depend upon

101. Line 161 · formal-object · records projected-env-000387

     \begin{thm}\ollabel{thm:cauchyorderedfield}

102. Line 162 · formal-object · records projected-env-000387

     The Cauchy sequences constitute an ordered field.

103. Line 163 · formal-object · records projected-env-000387

     \end{thm}

104. Line 169 · formal-object · records projected-env-000389

     \begin{prob}

105. Line 170 · formal-object · records projected-env-000389

     Prove that the Cauchy sequences constitute an ordered field.

106. Line 171 · formal-object · records projected-env-000389

     \end{prob}

107. Line 176 · formal-object · records projected-env-000390

     \begin{thm}

108. Line 177 · formal-object · records projected-env-000390

     Every non-empty set of Cauchy sequences with an upper bound has a

109. Line 178 · formal-object · records projected-env-000390

     least upper bound.

110. Line 179 · formal-object · records projected-env-000390

     \end{thm}

111. Line 181 · formula, formula-context · records projected-formula-0002709 projected-formula-0002710

     \begin{proof}[Proof sketch] Let $S$ be any non-empty set of Cauchy

112. Line 182 · formula, formula-context · records projected-formula-0002709 projected-formula-0002710 projected-formula-0002711 projected-formula-0002712 projected-formula-0002713

     sequences with an upper bound. So there is some $p \in \Rat$ such that

113. Line 183 · formula, formula-context · records projected-formula-0002710 projected-formula-0002711 projected-formula-0002712 projected-formula-0002713 projected-formula-0002714 projected-formula-0002715

     $p_{\Real}$ is an upper bound for $S$. Let $r \in S$; then there is

114. Line 184 · formula, formula-context · records projected-formula-0002711 projected-formula-0002712 projected-formula-0002713 projected-formula-0002714 projected-formula-0002715 projected-formula-0002716 projected-formula-0002717 projected-formula-0002718

     some $q \in \Rat$ such that $q_{\Real} < r$. So if a least upper bound

115. Line 185 · formula, formula-context · records projected-formula-0002714 projected-formula-0002715 projected-formula-0002716 projected-formula-0002717 projected-formula-0002718

     on $S$ exists, it is between $q_\Real$ and $p_\Real$ (inclusive). 

116. Line 187 · formula-context · records projected-formula-0002719

     We will hone in on the l.u.b., by approaching it simultaneously from

117. Line 188 · formula, formula-context · records projected-formula-0002719 projected-formula-0002720

     below and above. In particular, we define two functions, $f, g \colon

118. Line 189 · formula, formula-context · records projected-formula-0002719 projected-formula-0002720 projected-formula-0002721

     \Nat \to \Rat$, with the aim that $f$ will hone in on the l.u.b.\ from

119. Line 190 · formula, formula-context, source-correction · records TR006-SOURCE-PROSE-008 projected-formula-0002720 projected-formula-0002721 projected-formula-0002722

     above, and $g$ will hone on in it from below. We start by defining:

120. Line 191 · formal-object, formula, formula-context · records projected-env-000391 projected-formula-0002721 projected-formula-0002722

     \begin{align*}

121. Line 192 · formal-object, formula-context · records projected-env-000391 projected-formula-0002722

     	f(0) &= p \\

122. Line 193 · formal-object · records projected-env-000391

     	g(0) &= q

123. Line 194 · formal-object, formula-context · records projected-env-000391 projected-formula-0002723

     \end{align*}

124. Line 195 · formula · records projected-formula-0002723

     Then, where $a_n = \frac{f(n) + g(n)}{2}$, let:\footnote{This is a

125. Line 196 · formula-context · records projected-formula-0002723

     recursive definition. But we have not \emph{yet} given any reason to

126. Line 197 · formula-context · records projected-formula-0002724

     think that recursive definitions are ok.}

127. Line 198 · formal-object, formula · records projected-env-000394 projected-formula-0002724

     \begin{align*}

128. Line 199 · formal-object, formula-context · records projected-env-000394 projected-formula-0002724

     	f(n+1) &=

129. Line 200 · formal-object · records projected-env-000394

     	\begin{cases}

130. Line 201 · formal-object · records projected-env-000394

     		a_n &\text{if }(\forall h \in S)\equivrep{h}{} \leq (a_n)_\Real\\

131. Line 202 · formal-object · records projected-env-000394

     		f(n)&\text{otherwise}

132. Line 203 · formal-object · records projected-env-000394

     	\end{cases}\\

133. Line 204 · formal-object · records projected-env-000394

     	g(n+1) &=

134. Line 205 · formal-object · records projected-env-000394

     	\begin{cases}

135. Line 206 · formal-object · records projected-env-000394

     		a_n &\text{if }(\exists h \in S)\equivrep{h}{} \geq (a_n)_\Real\\

136. Line 207 · formal-object · records projected-env-000394

     	 	g(n) &\text{otherwise}

137. Line 208 · formal-object · records projected-env-000394

     	\end{cases}

138. Line 209 · formal-object, formula-context · records projected-env-000394 projected-formula-0002725 projected-formula-0002726

     \end{align*}

139. Line 210 · formula, formula-context · records projected-formula-0002725 projected-formula-0002726 projected-formula-0002727

     Both $f$ and $g$ are Cauchy sequences. (This can be checked fairly

140. Line 211 · formula, formula-context · records projected-formula-0002725 projected-formula-0002726 projected-formula-0002727 projected-formula-0002728 projected-formula-0002729 projected-formula-0002730

     easily, but we leave it as an exercise.) Note that the function $(f-g)$

141. Line 212 · formula, formula-context · records projected-formula-0002727 projected-formula-0002728 projected-formula-0002729 projected-formula-0002730 projected-formula-0002731

     tends to $0$, since the difference between $f$ and $g$ halves at each

142. Line 213 · formula, formula-context · records projected-formula-0002728 projected-formula-0002729 projected-formula-0002730 projected-formula-0002731

     step. Hence $\equivrep{f}{} = \equivrep{g}{}$. 

143. Line 215 · formula, formula-context · records projected-formula-0002732 projected-formula-0002733 projected-formula-0002734 projected-formula-0002735

     We first show that $\equivrep{f}{}$ is an upper bound on $S$, i.e.\ that $(\forall h \in S)\equivrep{h}{} \leq \equivrep{f}{}$.  

144. Line 216 · formula, formula-context, reference · records projected-formula-0002732 projected-formula-0002733 projected-formula-0002734 projected-formula-0002735 projected-formula-0002736 reference-000108

     (We will invoke \olref{thm:cauchyorderedfield} as we go.) Let $h \in S$ and

     [olref reference to sfr:arith:cauchy:thm:cauchyorderedfield]

145. Line 217 · formula, formula-context · records projected-formula-0002735 projected-formula-0002736 projected-formula-0002737 projected-formula-0002738

     suppose, for reductio, that $\equivrep{f}{} < \equivrep{h}{}$, so that

146. Line 218 · formula, formula-context · records projected-formula-0002736 projected-formula-0002737 projected-formula-0002738 projected-formula-0002739

     $0_\Real < \equivrep{(h-f)}{}$. Since $f$ is a monotonically

147. Line 219 · formula, formula-context · records projected-formula-0002737 projected-formula-0002738 projected-formula-0002739 projected-formula-0002740

     decreasing Cauchy sequence, there is some $n \in \Nat$ such that

148. Line 220 · formula, formula-context · records projected-formula-0002739 projected-formula-0002740 projected-formula-0002741

     $\equivrep{(c_{f(n)} - f)}{} < \equivrep{(h-f)}{}$. So:

149. Line 221 · formula, formula-context · records projected-formula-0002740 projected-formula-0002741

     \[

150. Line 222 · formula-context · records projected-formula-0002741

     	(f(n))_\Real = \equivrep{c_{f(n)}}{} < \equivrep{f}{} + \equivrep{(h-f)}{} = \equivrep{h}{},

151. Line 223 · formula-context · records projected-formula-0002742

     \]

152. Line 224 · formula · records projected-formula-0002742

     contradicting the fact that, by construction, $\equivrep{h}{} \leq (f(n))_\Real$.

153. Line 226 · formula, source-correction · records TR006-SOURCE-PROSE-009 projected-formula-0002743 projected-formula-0002744 projected-formula-0002745 projected-formula-0002746 projected-formula-0002747 projected-formula-0002748 projected-formula-0002749 projected-formula-0002750 projected-formula-0002751 projected-formula-0002752 projected-formula-0002753 projected-formula-0002754

     We next show that $\equivrep{f}{} = \equivrep{g}{}$ is the \emph{least} upper bound on $S$. So let $j$ be any Cauchy sequence and suppose $\equivrep{j}{} < \equivrep{g}{}$. Reasoning as above (using the fact that $g$ is \emph{increasing}), there is $n \in \Nat$ such that $\equivrep{j}{} < (g(n))_\Real$. But by construction there is $h \in S$ such that $(g(n))_\Real \leq \equivrep{h}{}$, so $\equivrep{j}{} < \equivrep{h}{}$ and therefore $\equivrep{j}{}$ is not an upper bound on $S$.  

154. Line 227 · formula-context · records projected-formula-0002743 projected-formula-0002744 projected-formula-0002745 projected-formula-0002746 projected-formula-0002747 projected-formula-0002748 projected-formula-0002749 projected-formula-0002750 projected-formula-0002751 projected-formula-0002752 projected-formula-0002753 projected-formula-0002754

     \end{proof}

content/sets-functions-relations/sets-functions-relations-complete.tex

0 exact source-coordinate anchors materialized from the accepted slice ledgers.

content/sets-functions-relations/infinite/infinite.tex

0 exact source-coordinate anchors materialized from the accepted slice ledgers.