Dedekind reals are equivalent to multi-valued Cauchy reals
A (modulated) Cauchy real is represented by a set $S \subseteq \mathbb N \times \mathbb Q$ with the following properties:
- $$\forall n \in \mathbb N. \exists! q \in \mathbb Q. (n, q) \in S$$
- $$\forall (n, q) \in S, (m, r) \in S. |q - r| \le 2^{-n} + 2^{-m}$$
And sets $S_1$ and $S_2$ represent the same Cauchy real iff
- $$\forall (n, q) \in S_1, (m, r) \in S_2. |q - r| \le 2^{-n} + 2^{-m}$$
The multi-valued Cauchy reals are the same except we replace 1 with
1*. $$\forall n \in \mathbb N. \exists q \in \mathbb Q. (n, q) \in S$$
leaving 2 and 3 exactly the same. We just drop the requirement that there is only one $q$ for each $n$. The computational content is basically the same; a constructive proof of 1* gives an algorithm to rationally approximate the real number. There just might be multiple such proofs that give different approximations for the same $S$.
With the axiom of countable choice, every multi-valued Cauchy real is equal to an ordinary, single-valued Cauchy real.
But even without that axiom, the multi-valued Cauchy reals and the Dedekind reals are isomorphic, so you can give Dedekind reals computational meaning by treating them as multi-valued Cauchy reals.
In the other direction, if you modify the definition of the Dedekind reals to require that locatedness is witnessed by a functionlocatedness is witnessed by a function, the resulting object will be isomorphic to the Cauchy reals as originally defined. So the difference really is just "do you want functions or just existential statements", which is what choice principles conflate.
Here is the proof that the Dedekind reals are isomorphic to multi-valued Cauchy reals.
Proof:
We embed the multi-valued Cauchy reals into the Dedekind reals as you might expect. For a multi-valued Cauchy real represented by $S$, we define:
$$L = \{ r \in \mathbb Q: \exists (n, q) \in S. q - r > 2^{-n} \}$$$$L = \{ p \in \mathbb Q: \exists (n, q) \in S. q - p > 2^{-n} \}$$ $$U = \{ r \in \mathbb Q: \exists (n, q) \in S. q - r < -2^{-n} \}$$$$U = \{ p \in \mathbb Q: \exists (n, q) \in S. q - p < -2^{-n} \}$$
Now we will show that every Dedekind real can be defined this way.
Let $y$ be a Dedekind real. We define $S$ as $$S = \{ (n, q) \in \mathbb N \times \mathbb Q : -2^{-n} \le q - y \le 2^{-n} \}$$
For an ordinary Cauchy real we'd need the axiom of countable choice to select $q$, but this is unnecessary for multi-valued Cauchy reals.
Verifying property (2) is just a little bit of algebra. Let's check property (1*).
Let $x, z \in \mathbb Q$ such that $x < y < z$. We prove that for any $k \in \mathbb N$, there is $q \in \mathbb Q$ such that $$-(\frac 23)^k (z - x) < q - y < (\frac 23)^k (z - x)$$ by induction on $k$.
- Base case: For $k=0$ let $q = z$.
- Induction step: Let $q'$ satisfy the theorem for $k$. To find $q$ for the $k+1$ case, we split into cases using locatedness:
- $q' - y < \frac 13 (\frac 23)^k (z - x)$: Let $q = q' + \frac 13 (\frac 23)^k (z - x)$. We know that $- \frac 33 (\frac 23)^k (z - x) < q' - y < \frac 13 (\frac 23)^k (z - x)$ and thus $-(\frac 23)^{k+1} (z - x) < q - y < (\frac 23)^{k+1} (z - x)$.
- $q' - y > - \frac 13 (\frac 23)^k (z - x)$: Let $q = q' - \frac 13 (\frac 23)^k (z - x)$. We know that $- \frac 13 (\frac 23)^k (z - x) < q' - y < \frac 33 (\frac 23)^k (z - x)$ and thus $-(\frac 23)^{k+1} (z - x) < q - y < (\frac 23)^{k+1} (z - x)$.
(Note, again, that we don't need countable choice since we don't need $q$ to be a function of $k$.)
Let $n \in \mathbb N$. Since $\lim_{k \to \infty} (\frac 23)^k (z - x) = 0$, there is a $k$ large enough that there is a $q \in \mathbb Q$ such that $-2^{-n} < q - y < 2^{-n}$. Then $(n,q) \in S$, demonstrating property (1*).
Verifying that the embedding into the Dedekind reals sends $S$ to $y$ is just a little bit of algebra.
$\square$