Added reference

- Fred Richman,
*Real numbers and other completions*, Real numbers and other completions. Mathematical Logic Quarterly, Volume 54, Issue 1, February 2008, Pages 98-108. (doi:https://onlinelibrary.wiley.com/doi/10.1002/malq.200710024)

Anonymouse

]]>Added that the coalgebraic view gives rise to the category of reals, and the reference.

dusko

]]>added pointer to:

- Nicolas Bourbaki,
*Real Numbers*, Chapter IV in:*General topology*, Elements of Mathematics, Springer (1971, 1990, 1995) [doi:10.1007/978-3-642-61701-0]

working on polishing-up the list of references

among other things, i have added publication data to this item:

- Gaëtan Gilbert,
*Formalising Real Numbers in Homotopy Type Theory*, in*CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs*(2017) 112–124 [arXiv:1610.05072, doi:10.1145/3018610.3018614]

added pointer to:

- Leo Corry, §10.5 in:
*A Brief History of Numbers*, Oxford University Press [ISBN:9780198702597]

adding another definition of the real numbers

Anonymous

]]>@24: Auke Booij proved the result for signed digit infinite decimal representations. If every Cauchy real number has an unsigned infinite decimal representation in the sense you are talking about, then the limited principle of omniscience for natural numbers holds, as proven by Errett Bishop and other constructive mathematicians.

]]>@25: My post #22 was a correction to the comment in #21 about a set isomorphism between the unit interval and decimal numerals.

]]>Gowers talks about that a bit here: https://www.dpmms.cam.ac.uk/~wtg10/decimals.html

]]>… with the appropriate corrections for trailing repeated 9’s vs repeated 0’s.

Incidentally, I may be misremembering, but I think the first rigorous proof I saw of the existence of the field of real numbers was actually given by defining the underlying set to be the decimal numbers (with its technicalities), and actually defined arithmetic via elementary school arithmetic, suitably modified to work for nonterminating decimals.

]]>That definition of the real numbers is incorrect: it is true for the integers and the rational numbers as well. One needs to additionally stipulate that for every sequence of integers bounded below by 0 and bounded above by 9, there is a real number $r$ such that the equation holds. Or one could simply include the structure of a set isomorphism between the unit interval and the type of sequences of integers bounded below by 0 and bounded above by 9.

]]>The pre-algebra real numbers:

The real numbers are an Archimedean ordered field such that for every real number $r$ in the interval $[0, 1]$, there is a sequence of integers $(a_n)_{n\in\mathbb{N}}$ bounded below by $0$ and bounded above by $9$ such that

$r = \lim_{n \to \infty} \sum_{i=0}^{n} \frac{a_i}{10^{i+1}}$If there exists a natural number $N$ such that the sequence $(a_n)_{n\in\mathbb{N}}$ is periodic for $n \geq N$, then $r$ is a rational number.

]]>I tried to repair some wrong claims about terminal archimedean structures.

]]>You should remove my version then. I thought it was simpler, but it’s so similar to the other one that there’s no real gain in having both. If we want a second example there’s the function that sends a nonnegative real to the list of how many $1$s there are between each $0$ in its binary expansion.

]]>I have added the earlier description, with the necessary adjustment. Please do not modify this addition without prior discussion.

]]>Right. I think the confusion was that you thought that my change to $\beta$ was to make it monotonic, whereas in fact I simply changed $\beta$ to allow the use of $\omega$ and $\mathbb{R}^+$ directly rather than having to replace them with $\mathbb{N}_{\geq 2}$ and $[1,\infty)$.

Then I *unrelatedly* changed the sentence that said that $\alpha$ and $\beta$ are monotonic to one which says that $(\alpha,\beta)$ is monotonic. And since we already mentioned in the definition of $F_1$ that the order on $\omega\times X$ is the ordinal product (which is lexicographic), I think the current wording already says exactly what you want.

I’ll say it here first: if $x \leq y$, then $(\alpha(x), \beta(x)) \leq (\alpha(y), \beta(y))$ using the lexicographic order.

]]>I don’t understand what you mean about product vs lexicographic. If you go ahead and make the change I’ll look at what you wrote.

]]>However, I still like my original description, which works if we simply change from the product poset $\omega \times \mathbb{R}_+$ to the lexicographic one. We can keep yours, but I want mine reentered into the record.

Added: are you sure $\beta$ is monotonic? I get $\beta(1.9) \gt \beta(2.1)$. I think in fact it’s the very same issue as before.

]]>