# 11.4 Comparison of Cauchy and Dedekind reals

Let us also say something about the relationship between the Cauchy and Dedekind reals. By \autorefRC-archimedean-ordered-field, $\mathbb{R}_{\mathsf{c}}$ is an archimedean ordered field. It is also admissible for $\Omega$, as can be easily checked. (In case $\Omega$ is the initial $\sigma$-frame it takes a simple induction, while in other cases it is immediate.) Therefore, by \autorefRD-final-field there is an embedding of ordered fields

 $\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{d}}$

which fixes the rational numbers. (We could also obtain this from \autorefRC-initial-Cauchy-complete,\autorefRD-cauchy-complete.) In general we do not expect $\mathbb{R}_{\mathsf{c}}$ and $\mathbb{R}_{\mathsf{d}}$ to coincide without further assumptions.

###### Lemma 11.4.1.

If for every $x:\mathbb{R}_{\mathsf{d}}$ there merely exists

 $c:\mathchoice{\prod_{q,r:\mathbb{Q}}\,}{\mathchoice{{\textstyle\prod_{(q,r:% \mathbb{Q})}}}{\prod_{(q,r:\mathbb{Q})}}{\prod_{(q,r:\mathbb{Q})}}{\prod_{(q,r% :\mathbb{Q})}}}{\mathchoice{{\textstyle\prod_{(q,r:\mathbb{Q})}}}{\prod_{(q,r:% \mathbb{Q})}}{\prod_{(q,r:\mathbb{Q})}}{\prod_{(q,r:\mathbb{Q})}}}{\mathchoice% {{\textstyle\prod_{(q,r:\mathbb{Q})}}}{\prod_{(q,r:\mathbb{Q})}}{\prod_{(q,r:% \mathbb{Q})}}{\prod_{(q,r:\mathbb{Q})}}}(q (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:RD-linear-order), which states that $<$ is a weak linear order. We already know that $\mathbb{R}_{\mathsf{c}}$ embeds into $\mathbb{R}_{\mathsf{d}}$, so it suffices to show that every Dedekind real merely is the limit of a Cauchy sequence of rational numbers.

Consider any $x:\mathbb{R}_{\mathsf{d}}$. By assumption there merely exists $c$ as in the statement of the lemma, and by inhabitation of cuts there merely exist $a,b:\mathbb{Q}$ such that $a. We construct a sequence $f:\mathbb{N}\to\setof{{\mathopen{}(q,r)\mathclose{}}\in\mathbb{Q}\times\mathbb% {Q}|q by recursion:

1. 1.

Set $f(0):\!\!\equiv{\mathopen{}(a,b)\mathclose{}}$.

2. 2.

Suppose $f(n)$ is already defined as ${\mathopen{}(q_{n},r_{n})\mathclose{}}$ such that $q_{n}. Define $s:\!\!\equiv(2q_{n}+r_{n})/3$ and $t:\!\!\equiv(q_{n}+2r_{n})/3$. Then $c(s,t)$ decides between $s and $x. If it decides $s then we set $f(n+1):\!\!\equiv{\mathopen{}(s,r_{n})\mathclose{}}$, otherwise $f(n+1):\!\!\equiv{\mathopen{}(q_{n},t)\mathclose{}}$.

Let us write ${\mathopen{}(q_{n},r_{n})\mathclose{}}$ for the $n$-th term of the sequence $f$. Then it is easy to see that $q_{n} and $|q_{n}-r_{n}|\leq(2/3)^{n}\cdot|q_{0}-r_{0}|$ for all $n:\mathbb{N}$. Therefore $q_{0},q_{1},\ldots$ and $r_{0},r_{1},\ldots$ are both Cauchy sequences converging to the Dedekind cut $x$. We have shown that for every $x:\mathbb{R}_{\mathsf{d}}$ there merely exists a Cauchy sequence converging to $x$. ∎

The lemma implies that either countable choice or excluded middle suffice for coincidence of $\mathbb{R}_{\mathsf{c}}$ and $\mathbb{R}_{\mathsf{d}}$.

###### Corollary 11.4.3.

If excluded middle or countable choice holds then $\mathbb{R}_{\mathsf{c}}$ and $\mathbb{R}_{\mathsf{d}}$ are equivalent.

###### Proof.

If excluded middle holds then $(x can be proved: either $x or $\lnot(x. In the former case we are done, while in the latter we get $z because $z\leq x. Therefore, we get (11.4.1) so that we can apply \autoreflem:untruncated-linearity-reals-coincide.

Suppose countable choice holds. The set $S=\setof{{\mathopen{}(q,r)\mathclose{}}\in\mathbb{Q}\times\mathbb{Q}|q is equivalent to $\mathbb{N}$, so we may apply countable choice to the statement that $x$ is located,

 $\forall({\mathopen{}(q,r)\mathclose{}}:S).\,(q

Note that $(q is expressible as an existential statement $\exists(b:\mathbf{2}).\,(b={0_{\mathbf{2}}}\to q. The (curried form) of the choice function is then precisely (11.4.1) so that \autoreflem:untruncated-linearity-reals-coincide is applicable again. ∎

 Title 11.4 Comparison of Cauchy and Dedekind reals \metatable