# 11.2.2 Dedekind reals are Cauchy complete

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

$$ | (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\ge M(\u03f5)$
implies $$. From this we get $$ for all $\u03f5:{\mathbb{Q}}_{+}$. In fact, the map $(\u03f5\mapsto {x}_{M(\u03f5/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\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}\mathrm{\to}{\mathrm{R}}_{\mathrm{d}}$ which satisfies

$$ | (11.2.2) |

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

$$ |

###### Theorem 11.2.4.

Every Cauchy approximation in ${\mathrm{R}}_{\mathrm{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}}_{\U0001d5bd}$, define

${L}_{y}(q)$ | $:\equiv \exists (\u03f5,\theta :{\mathbb{Q}}_{+}).{L}_{{x}_{\u03f5}}(q+\u03f5+\theta ),$ | ||

${U}_{y}(q)$ | $:\equiv \exists (\u03f5,\theta :{\mathbb{Q}}_{+}).{U}_{{x}_{\u03f5}}(q-\u03f5-\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 $$. There is $\u03f5:{\mathbb{Q}}_{+}$ such that $$. Since $$ merely ${L}_{{x}_{\u03f5}}(q+2\u03f5)$ or ${U}_{{x}_{\u03f5}}(r-2\u03f5)$. 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 $\u03f5,\theta :{\mathbb{Q}}_{+}$. Because $\mathbb{Q}$ is dense in ${\mathbb{R}}_{\U0001d5bd}$ there merely exist $q,r:\mathbb{Q}$ such that

$$ |

and thus $$. Now either $$ or $$. In the first case we have

$$ |

and in the second

$$ |

In either case it follows that $$. ∎

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

###### Corollary 11.2.5.

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

$$ |

###### Proof.

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

$$ |

Title | 11.2.2 Dedekind reals are Cauchy complete^{} |

\metatable |