11.4 Comparison of Cauchy and Dedekind reals
Let us also say something about the relationship between the Cauchy and Dedekind reals. By \autorefRCarchimedeanorderedfield, ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ is an archimedean^{} ordered field. It is also admissible for $\mathrm{\Xi \copyright}$, as can be easily checked. (In case $\mathrm{\Xi \copyright}$ is the initial $\mathrm{{\rm O}\x83}$frame it takes a simple induction^{}, while in other cases it is immediate.) Therefore, by \autorefRDfinalfield there is an embedding^{} of ordered fields
$${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}\beta \x86\x92{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$$ 
which fixes the rational numbers. (We could also obtain this from \autorefRCinitialCauchycomplete,\autorefRDcauchycomplete.) In general we do not expect ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ and ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$ to coincide without further assumptions^{}.
Lemma 11.4.1.
If for every $x\mathrm{:}{\mathrm{R}}_{\mathrm{d}}$ there merely exists
$$  (11.4.1) 
then the Cauchy and Dedekind reals coincide.
Proof.
Note that the type inΒ (11.4.1) is an untruncated variant ofΒ (LABEL:eq:RDlinearorder), which states thatΒ $$ is a weak linear order. We already know that ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ embeds into ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$, so it suffices to show that every Dedekind real merely is the limit of a Cauchy sequence^{} of rational numbers.
Consider any $x:{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$. By assumption there merely exists $c$ as in the statement of the lemma, and by inhabitation of cuts there merely exist $a,b:\mathrm{\beta \x84\x9a}$ such that $$. We construct a sequence^{} $$ by recursion:

1.
Set $f(0):\beta \x89\u2018(a,b)$.

2.
Suppose $f\beta \x81\u2019(n)$ is already defined as $({q}_{n},{r}_{n})$ such that $$. Define $s:\beta \x89\u2018(2{q}_{n}+{r}_{n})/3$ and $t:\beta \x89\u2018({q}_{n}+2{r}_{n})/3$. Then $c\beta \x81\u2019(s,t)$ decides between $$ and $$. If it decides $$ then we set $f(n+1):\beta \x89\u2018(s,{r}_{n})$, otherwise $f(n+1):\beta \x89\u2018({q}_{n},t)$.
Let us write $({q}_{n},{r}_{n})$ for the $n$th term of the sequenceΒ $f$. Then it is easy to see that $$ and ${q}_{n}{r}_{n}\beta \x89\u20ac{(2/3)}^{n}\beta \x8b\x85{q}_{0}{r}_{0}$ for all $n:\mathrm{\beta \x84\x95}$. Therefore ${q}_{0},{q}_{1},\mathrm{\beta \x80\xa6}$ and ${r}_{0},{r}_{1},\mathrm{\beta \x80\xa6}$ are both Cauchy sequences converging to the Dedekind cutΒ $x$. We have shown that for every $x:{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$ there merely exists a Cauchy sequence converging to $x$. β
The lemma implies that either countable choice or excluded middle suffice for coincidence of ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\u038c}}$ and ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$.
Corollary 11.4.3.
If excluded middle or countable choice holds then ${\mathrm{R}}_{\mathrm{c}}$ and ${\mathrm{R}}_{\mathrm{d}}$ are equivalent^{}.
Proof.
If excluded middle holds then $$ can be proved: either $$ or $$. In the former case we are done, while in the latter we get $$ because $$. Therefore, we getΒ (11.4.1) so that we can apply \autoreflem:untruncatedlinearityrealscoincide.
Suppose countable choice holds. The set $$ is equivalent to $\mathrm{\beta \x84\x95}$, so we may apply countable choice to the statement that $x$ is located,
$$ 
Note that $$ is expressible as an existential statement $$. The (curried form) of the choice function is then preciselyΒ (11.4.1) so that \autoreflem:untruncatedlinearityrealscoincide is applicable again. β
Title  11.4 Comparison of Cauchy and Dedekind reals 
\metatable 