11.2.3 Dedekind reals are Dedekind complete

We obtained ℝ𝖽 as the type of Dedekind cutsMathworldPlanetmath on β„š. But we could have instead started with any archimedeanPlanetmathPlanetmathPlanetmath ordered field F and constructed Dedekind cuts on F. These would again form an archimedean ordered field FΒ―, the Dedekind completion of F, with F contained as a subfieldMathworldPlanetmath. What happens if we apply this construction to ℝ𝖽, do we get even more real numbers? The answer is negative. In fact, we shall prove a stronger result: ℝ𝖽 is final.

Say that an ordered field F is admissible for Ω when the strict order < on F is a map <:F→F→Ω.

Theorem 11.2.1.

Every archimedean ordered field which is admissible for Ξ© is a subfield ofΒ Rd.


Let F be an archimedean ordered field. For every x:F define L,U:β„šβ†’Ξ© by

Lx(q):≑(q<x)  and  Ux(q):≑(x<q).

(We have just used the assumptionPlanetmathPlanetmath that F is admissible for Ξ©.) Then (Lx,Ux) is a Dedekind cut. Indeed, the cuts are inhabited and rounded because F is archimedean and < is transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath, disjoint because < is irreflexiveMathworldPlanetmath, and located because < is a weak linear order. Let e:F→ℝ𝖽 be the map e(x):≑(Lx,Ux).

We claim that e is a field embeddingPlanetmathPlanetmath which preserves and reflects the order. First of all, notice that e⁒(q)=q for a rational number q. Next we have the equivalences, for all x,y:F,


so e indeed preserves and reflects the order. That e⁒(x+y)=e⁒(x)+e⁒(y) holds because, for all q:β„š,


The implicationMathworldPlanetmath from right to left is obvious. For the other direction, if q<x+y then there merely exists r:β„š such that q-y<r<x, and by taking s:≑q-r we get the desired r and s. We leave preservation of multiplicationPlanetmathPlanetmath by e as an exercise. ∎

To establish that the Dedekind cuts on ℝ𝖽 do not give us anything new, we need just one more lemma.

Lemma 11.2.2.

If F is admissible for Ξ© then so is its Dedekind completion.


Let FΒ― be the Dedekind completion of F. The strict order on FΒ― is defined by


Since U⁒(q) and L′⁒(q) are elements of Ξ©, the lemma holds as long as Ξ© is closed under conjunctionsMathworldPlanetmath and countableMathworldPlanetmath existentials, which we assumed from the outset. ∎

Corollary 11.2.3.

The Dedekind reals are Dedekind complete: for every real-valued Dedekind cut (L,U) there is a unique x:Rd such that L(y)=(y<x) and U(y)=(x<y) for all y:Rd.


By \autoreflem:cuts-preserve-admissibility the Dedekind completion ℝ¯𝖽 of ℝ𝖽 is admissible for Ξ©, so by \autorefRD-final-field we have an embedding ℝ¯𝖽→ℝ𝖽, as well as an embedding ℝ𝖽→ℝ¯𝖽. But these embeddings must be isomorphismsPlanetmathPlanetmathPlanetmathPlanetmath, because their compositions are order-preserving field homomorphisms which fix the dense subfieldΒ β„š, which means that they are the identityPlanetmathPlanetmath. The corollary now follows immediately from the fact that ℝ¯𝖽→ℝ𝖽 is an isomorphism. ∎

Title 11.2.3 Dedekind reals are Dedekind complete