Decimal expansion definition of real numbers, constructively

Question

The two most common definitions of $\mathbb{R}$ are as Dedekind cuts or Cauchy sequences of rational numbers.

A real analysis student of mine is working out of the book Real Analysis and Applications by Davidson and Donsig, who use a different definition based on decimal expansions. A real number is a sequence $$x:\mathbb{N}\to\mathbb{Z}$$ where $x_0$ is the 'whole number part' of $x$ and the remainder of the sequence takes values in $\{0,...,9\}$, interpreted as the 'decimal part' of $x$. They observe that this gives rise to ambiguities like $0.999...=1.000...$, and so they define an equivalence relation on these functions to identify sequences that are 'infinitesimally close' to one another.

How does this construction compare constructively to the other two?

My understanding is that the Dedekind and Cauchy reals are ismoprphic classically, but constructively things get more subtle (mostly things go wrong with Dedekind cuts?). Are there any references that construct the reals in the above manner constructively, e.g. in a topos?

Answer 1

We have a well defined map from decimal expansions to Cauchy real numbers, so by taking the image factorisation of this map, we can always quotient out the set of decimal expansions to get a subobject of the Cauchy reals. This subobject is $\neg \neg$-dense, i.e. every Cauchy real does not lack a decimal expansion, corresponding to the fact that every computable real number has a computable decimal expansion. However, it is still the case in general in constructive mathematics that not every Cauchy real has to have a decimal expansion, corresponding to the fact that there is no uniformly computable way to find decimal expansions of computable Cauchy sequences.

In the presence of countable choice, the Dedekind and Cauchy reals are the same, and the following are equivalent (if I recall correctly weak countable choice is sufficient for these equivalences, but lets stick to countable choice for simplicity):

1. Every real number has a decimal expansion.
2. Decimal expansions are closed under addition.
3. The lesser limited principle of omniscience (LLPO): for every binary sequence $\alpha$ with at most one $i$ such that $\alpha(i) = 1$, either $\alpha(2i) = 0$ for all $i$, or $\alpha(2i + 1) = 0$ for all $i$.

For $1 \Rightarrow 2$, just use that Cauchy real numbers are closed under addition.

For $2 \Rightarrow 3$, let $\alpha$ be a binary sequence with at most one $1$, and define two decimal expansions $a := 0.a_0 a_1 a_2 a_3 \ldots$ and $b := 0.b_0 b_1 b_2 b_3 \ldots$ where $$ a_i = \begin{cases} 9 & \alpha(2i) = 0 \\ 0 & \alpha(2i) = 1 \end{cases} $$ $$ b_i = \begin{cases} 0 & \alpha(2 i + 1) = 0 \\ 1 & \alpha(2 i + 1) = 1. \end{cases} $$ If the first digit of the decimal expansion of $a + b$ is $1$, then $\alpha(2i) = 0$ for all $i$, and if the first digit is $0$, then $\alpha(2 i + 1) = 0$ for all $i$.

Fer $3 \Rightarrow 1$, note that we can build the decimal expansion up a stage at time. If the current Cauchy approximation of a real $a$ at stage $n$ is exactly $0.a_1\ldots a_n$, and we need to find the $n$th decimal digit, we can use LLPO to show there exists $a_n' \in \{a_n - 1, a_n\}$ such that if $a_n' = a_n - 1$, then $a \leq 0.a_1\ldots a_n$ and if $a_n' = a_n$, then $a \geq 0.a_1\ldots a_n$, and we can choose such an $a_n'$ (for all elements of the countable set of finite decimal expansions) by countable choice.