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<r)\to(q<x)+(x<r)

(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<x<b$ . We construct a sequence $f:\mathbb{N}\to\setof{{\mathopen{}(q,r)\mathclose{}}\in\mathbb{Q}\times\mathbb% {Q}|q<r}$ by recursion:

1.

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

Suppose $f(n)$ is already defined as ${\mathopen{}(q_{n},r_{n})\mathclose{}}$ such that $q_{n}<r_{n}$ . Define $s:\!\!\equiv(2q_{n}+r_{n})/3$ and $t:\!\!\equiv(q_{n}+2r_{n})/3$ . Then $c(s,t)$ decides between $s<x$ and $x<t$ . If it decides $s<x$ 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}<x<r_{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<y)\to(x<z)+(z<y)$ can be proved: either $x<z$ or $\lnot(x<z)$ . In the former case we are done, while in the latter we get $z<y$ because $z\leq x<y$ . 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<r}$ 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<x)\lor(x<r).

Note that $(q<x)\lor(x<r)$ is expressible as an existential statement $\exists(b:\mathbf{2}).\,(b={0_{\mathbf{2}}}\to q<x)\land(b={1_{\mathbf{2}}}\to x% <r)$ . 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