# 11.2.2 Dedekind reals are Cauchy complete

Recall that $x:\mathbb{N}\to\mathbb{Q}$ is a Cauchy sequence when it satisfies

 $\mathchoice{\prod_{(\epsilon:\mathbb{Q}_{+})}\,}{\mathchoice{{\textstyle\prod_% {(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}\mathchoice{\sum_{(n:\mathbb{N})}\,}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{% \sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}\mathchoice{\prod_{(m,k\geq n)}\,}{\mathchoice{{\textstyle\prod_{(m,k% \geq n)}}}{\prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}}{% \mathchoice{{\textstyle\prod_{(m,k\geq n)}}}{\prod_{(m,k\geq n)}}{\prod_{(m,k% \geq n)}}{\prod_{(m,k\geq n)}}}{\mathchoice{{\textstyle\prod_{(m,k\geq n)}}}{% \prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}}|x_{m}-x_{k}|<\epsilon.$ (11.2.1)

Note that we did not truncate the inner existential because we actually want to compute rates of convergence—an approximation without an error estimate carries little useful information. By \autorefthm:ttac, (11.2.1) yields a function $M:\mathbb{Q}_{+}\to\mathbb{N}$, called the modulus of convergence, such that $m,k\geq M(\epsilon)$ implies $|x_{m}-x_{k}|<\epsilon$. From this we get $|x_{M(\delta/2)}-x_{M(\epsilon/2)}|<\delta+\epsilon$ for all $\epsilon:\mathbb{Q}_{+}$. In fact, the map $(\epsilon\mapsto x_{M(\epsilon/2)}):\mathbb{Q}_{+}\to\mathbb{Q}$ carries the same information about the limit as the original Cauchy condition (11.2.1). We shall work with these approximation functions rather than with Cauchy sequences.

###### Definition 11.2.2.

A Cauchy approximation is a map $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{d}}$ which satisfies

 $\forall(\delta,\epsilon:\mathbb{Q}_{+}).\,|x_{\delta}-x_{\epsilon}|<\delta+\epsilon.$ (11.2.2)

The limit of a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{d}}$ is a number $\ell:\mathbb{R}_{\mathsf{d}}$ such that

 $\forall(\epsilon,\theta:\mathbb{Q}_{+}).\,|x_{\epsilon}-\ell|<\epsilon+\theta.$
###### Theorem 11.2.4.

Every Cauchy approximation in $\mathbb{R}_{\mathsf{d}}$ has a limit.

###### Proof.

Note that we are showing existence, not mere existence, of the limit. Given a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{d}}$, define

 $\displaystyle L_{y}(q)$ $\displaystyle:\!\!\equiv\exists(\epsilon,\theta:\mathbb{Q}_{+}).\,L_{x_{% \epsilon}}(q+\epsilon+\theta),$ $\displaystyle U_{y}(q)$ $\displaystyle:\!\!\equiv\exists(\epsilon,\theta:\mathbb{Q}_{+}).\,U_{x_{% \epsilon}}(q-\epsilon-\theta).$

It is clear that $L_{y}$ and $U_{y}$ are inhabited, rounded, and disjoint. To establish locatedness, consider any $q,r:\mathbb{Q}$ such that $q. There is $\epsilon:\mathbb{Q}_{+}$ such that $5\epsilon. Since $q+2\epsilon merely $L_{x_{\epsilon}}(q+2\epsilon)$ or $U_{x_{\epsilon}}(r-2\epsilon)$. In the first case we have $L_{y}(q)$ and in the second $U_{y}(r)$.

To show that $y$ is the limit of $x$, consider any $\epsilon,\theta:\mathbb{Q}_{+}$. Because $\mathbb{Q}$ is dense in $\mathbb{R}_{\mathsf{d}}$ there merely exist $q,r:\mathbb{Q}$ such that

 $x_{\epsilon}-\epsilon-\theta/2

and thus $q. Now either $y or $x_{\epsilon}-\theta/2. In the first case we have

 $x_{\epsilon}-\epsilon-\theta/2

and in the second

 $x_{\epsilon}-\theta/2

In either case it follows that $|y-x_{\epsilon}|<\epsilon+\theta$. ∎

For sake of completeness we record the classic formulation as well.

###### Corollary 11.2.5.

Suppose $x:\mathbb{N}\to\mathbb{R}_{\mathsf{d}}$ satisfies the Cauchy condition (11.2.1). Then there exists $y:\mathbb{R}_{\mathsf{d}}$ such that

 $\mathchoice{\prod_{(\epsilon:\mathbb{Q}_{+})}\,}{\mathchoice{{\textstyle\prod_% {(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}\mathchoice{\sum_{(n:\mathbb{N})}\,}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{% \sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}\mathchoice{\prod_{(m\geq n)}\,}{\mathchoice{{\textstyle\prod_{(m\geq n% )}}}{\prod_{(m\geq n)}}{\prod_{(m\geq n)}}{\prod_{(m\geq n)}}}{\mathchoice{{% \textstyle\prod_{(m\geq n)}}}{\prod_{(m\geq n)}}{\prod_{(m\geq n)}}{\prod_{(m% \geq n)}}}{\mathchoice{{\textstyle\prod_{(m\geq n)}}}{\prod_{(m\geq n)}}{\prod% _{(m\geq n)}}{\prod_{(m\geq n)}}}|x_{m}-y|<\epsilon.$
###### Proof.

By \autorefthm:ttac there is $M:\mathbb{Q}_{+}\to\mathbb{N}$ such that $\bar{x}(\epsilon):\!\!\equiv x_{M(\epsilon/2)}$ is a Cauchy approximation. Let $y$ be its limit, which exists by \autorefRD-cauchy-complete. Given any $\epsilon:\mathbb{Q}_{+}$, let $n:\!\!\equiv M(\epsilon/4)$ and observe that, for any $m\geq n$,

 $|x_{m}-y|\leq|x_{m}-x_{n}|+|x_{n}-y|=|x_{m}-x_{n}|+|\bar{x}(\epsilon/2)-y|<% \epsilon/4+\epsilon/2+\epsilon/4=\epsilon.\qed$
 Title 11.2.2 Dedekind reals are Cauchy complete \metatable