11.2.2 Dedekind reals are Cauchy complete

Recall that x: is a Cauchy sequenceMathworldPlanetmathPlanetmath when it satisfies

(ϵ:+)(n:)(m,kn)|xm-xk|<ϵ. (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:+, called the modulus of convergence, such that m,kM(ϵ) implies |xm-xk|<ϵ. From this we get |xM(δ/2)-xM(ϵ/2)|<δ+ϵ for all ϵ:+. In fact, the map (ϵxM(ϵ/2)):+ 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:Q+Rd which satisfies

(δ,ϵ:+).|xδ-xϵ|<δ+ϵ. (11.2.2)

The limit of a Cauchy approximation x:Q+Rd is a number :Rd such that

Theorem 11.2.4.

Every Cauchy approximation in Rd has a limit.


Note that we are showing existence, not mere existence, of the limit. Given a Cauchy approximation x:+𝖽, define

Ly(q) :(ϵ,θ:+).Lxϵ(q+ϵ+θ),
Uy(q) :(ϵ,θ:+).Uxϵ(q-ϵ-θ).

It is clear that Ly and Uy are inhabited, rounded, and disjoint. To establish locatedness, consider any q,r: such that q<r. There is ϵ:+ such that 5ϵ<r-q. Since q+2ϵ<r-2ϵ merely Lxϵ(q+2ϵ) or Uxϵ(r-2ϵ). In the first case we have Ly(q) and in the second Uy(r).

To show that y is the limit of x, consider any ϵ,θ:+. Because is dense in 𝖽 there merely exist q,r: such that


and thus q<y<r. Now either y<xϵ+θ/2 or xϵ-θ/2<y. In the first case we have


and in the second


In either case it follows that |y-xϵ|<ϵ+θ. ∎

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

Corollary 11.2.5.

Suppose x:NRd satisfies the Cauchy condition (11.2.1). Then there exists y:Rd such that


By \autorefthm:ttac there is M:+ such that x¯(ϵ):xM(ϵ/2) is a Cauchy approximation. Let y be its limit, which exists by \autorefRD-cauchy-complete. Given any ϵ:+, let n:M(ϵ/4) and observe that, for any mn,

Title 11.2.2 Dedekind reals are Cauchy completePlanetmathPlanetmath