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 tocompute rates of convergence—an approximation without an error estimate carries littleuseful information. By thm:ttac, (11.2.1) yields a function $M:{\mathbb{Q}}_{+}\to \mathbb{N}$, called the modulus of convergence, such that $m,k\ge M(ϵ)$implies . From this we get for all $ϵ:{\mathbb{Q}}_{+}$. In fact, the map $(ϵ\mapsto x_{M(ϵ/2)}):{\mathbb{Q}}_{+}\to \mathbb{Q}$ carries the same information about the limit as theoriginal Cauchy condition (11.2.1). We shall work with theseapproximation functions rather than with Cauchy sequences.

Definition 11.2.2.

A Cauchy approximationis a map $x\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}\mathrm{\to }{\mathrm{R}}_{\mathrm{d}}$ which satisfies

(11.2.2)

The limitof a Cauchy approximation $x\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}\mathrm{\to }{\mathrm{R}}_{\mathrm{d}}$ is a number $\mathrm{\ell }\mathrm{:}{\mathrm{R}}_{\mathrm{d}}$ suchthat

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 {ℝ}_{𝖽}$, define

$L_y(q)$$:\equiv \exists (ϵ,\theta :{\mathbb{Q}}_{+}).L_{x_{ϵ}}(q+ϵ+\theta ),$

$U_y(q)$$:\equiv \exists (ϵ,\theta :{\mathbb{Q}}_{+}).U_{x_{ϵ}}(q-ϵ-\theta ).$

It is clear that $L_y$ and $U_y$ are inhabited, rounded, and disjoint. To establishlocatedness, consider any $q,r:\mathbb{Q}$ such that . There is $ϵ:{\mathbb{Q}}_{+}$ suchthat . Since merely$L_{x_{ϵ}}(q+2ϵ)$ or $U_{x_{ϵ}}(r-2ϵ)$. In the first casewe have $L_y(q)$ and in the second $U_y(r)$.

To show that $y$ is the limit of $x$, consider any $ϵ,\theta :{\mathbb{Q}}_{+}$. Because$\mathbb{Q}$ is dense in ${ℝ}_{𝖽}$ 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). Thenthere exists $y\mathrm{:}{\mathrm{R}}_{\mathrm{d}}$ such that

Proof.

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