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, ℝ𝖼 is an archimedeanPlanetmathPlanetmathPlanetmathPlanetmath ordered field. It is also admissible for Ξ©, as can be easily checked. (In case Ξ© is the initial Οƒ-frame it takes a simple inductionMathworldPlanetmath, while in other cases it is immediate.) Therefore, by \autorefRD-final-field there is an embeddingMathworldPlanetmathPlanetmath of ordered fields


which fixes the rational numbers. (We could also obtain this from \autorefRC-initial-Cauchy-complete,\autorefRD-cauchy-complete.) In general we do not expect ℝ𝖼 and ℝ𝖽 to coincide without further assumptionsPlanetmathPlanetmath.

Lemma 11.4.1.

If for every x:Rd there merely exists

c:∏q,r:β„š(q<r)β†’(q<x)+(x<r) (11.4.1)

then the Cauchy and Dedekind reals coincide.


Note that the type inΒ (11.4.1) is an untruncated variant ofΒ (LABEL:eq:RD-linear-order), which states thatΒ < is a weak linear order. We already know that ℝ𝖼 embeds into ℝ𝖽, so it suffices to show that every Dedekind real merely is the limit of a Cauchy sequenceMathworldPlanetmathPlanetmath of rational numbers.

Consider any x:ℝ𝖽. By assumption there merely exists c as in the statement of the lemma, and by inhabitation of cuts there merely exist a,b:β„š such that a<x<b. We construct a sequenceMathworldPlanetmath f:β„•β†’\setof(q,r)βˆˆβ„šΓ—β„š|q<r by recursion:

  1. 1.

    Set f(0):≑(a,b).

  2. 2.

    Suppose f⁒(n) is already defined as (qn,rn) such that qn<rn. Define s:≑(2qn+rn)/3 and t:≑(qn+2rn)/3. Then c⁒(s,t) decides between s<x and x<t. If it decides s<x then we set f(n+1):≑(s,rn), otherwise f(n+1):≑(qn,t).

Let us write (qn,rn) for the n-th term of the sequenceΒ f. Then it is easy to see that qn<x<rn and |qn-rn|≀(2/3)nβ‹…|q0-r0| for all n:β„•. Therefore q0,q1,… and r0,r1,… are both Cauchy sequences converging to the Dedekind cutΒ x. We have shown that for every x:ℝ𝖽 there merely exists a Cauchy sequence converging to x. ∎

The lemma implies that either countable choice or excluded middle suffice for coincidence of ℝ𝖼 and ℝ𝖽.

Corollary 11.4.3.

If excluded middle or countable choice holds then Rc and Rd are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath.


If excluded middle holds then (x<y)β†’(x<z)+(z<y) can be proved: either x<z or ¬⁑(x<z). In the former case we are done, while in the latter we get z<y because z≀x<y. Therefore, we getΒ (11.4.1) so that we can apply \autoreflem:untruncated-linearity-reals-coincide.

Suppose countable choice holds. The set S=\setof(q,r)βˆˆβ„šΓ—β„š|q<r is equivalent to β„•, so we may apply countable choice to the statement that x is located,


Note that (q<x)∨(x<r) is expressible as an existential statement βˆƒ(b:𝟐).(b=0πŸβ†’q<x)∧(b=1πŸβ†’x<r). The (curried form) of the choice function is then preciselyΒ (11.4.1) so that \autoreflem:untruncated-linearity-reals-coincide is applicable again. ∎

Title 11.4 Comparison of Cauchy and Dedekind reals