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 alsoadmissible for $\\Omega$ , as can be easily checked. (In case $\\Omega$ is the initial $\\sigma$ -frameit 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 coincidewithout 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 variantof (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 Dedekindreal 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 thelemma, 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}$ byrecursion:

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 easyto 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 sequencesconverging to the Dedekind cut $x$ . We have shown that for every $x:\\mathbb{R}_{\\mathsf{d}}$ there merelyexists a Cauchy sequence converging to $x$ .∎

The lemma implies that either countable choice or excluded middle suffice for coincidenceof $\\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 wecan 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}}}\\tox%<r)$ . The (curried form) ofthe choice function is then precisely (11.4.1) so that\\autoreflem:untruncated-linearity-reals-coincide is applicable again.∎