11.2 Dedekind reals


Let us first recall the basic idea of Dedekind’s construction. We use two-sided Dedekind cuts, as opposed to an often used one-sided version, because the symmetry makes constructions more elegant, and it works constructively as well as classically. A Dedekind cut consists of a pair (L,U) of subsets L,U, called the lower and upper cut respectively, which are:

  1. 1.

    inhabited: there are qL and rU,

  2. 2.

    rounded: qL(r).q<rrL and rU(q).qUq<r,

  3. 3.

    disjoint: ¬(qLqU), and

  4. 4.

    located: q<rqLrU.

Reading the roundedness condition from left to right tells us that cuts are open, and from right to left that they are lower, respectively upper, sets. The locatedness condition states that there is no large gap between L and U. Because cuts are always open, they never include the “point in between”, even when it is rational. A typical Dedekind cut looks like this:

{tikzpicture}

[x=] \draw[¡-),line width=0.75pt] (0,0) – (0.297,0) node[anchor=south east]L; \draw[(-¿,line width=0.75pt] (0.300, 0) node[anchor=south west]U – (0.9, 0) ;

We might naively translate the informal definition into type theoryPlanetmathPlanetmath by saying that a cut is a pair of maps L,U:𝖯𝗋𝗈𝗉. But we saw in \autorefsubsec:prop-subsets that 𝖯𝗋𝗈𝗉 is an ambiguous notation for 𝖯𝗋𝗈𝗉𝒰i where 𝒰i is a universePlanetmathPlanetmath. Once we use a particular 𝒰i to define cuts, the type of reals will reside in the next universe 𝒰i+1, a property of reals two levels higher in 𝒰i+2, a property of subsets of reals in 𝒰i+3, etc. In principle we should be able to keep track of the universe levels, especially with the help of a proof assistant, but doing so here would just burden us with bureaucracy that we prefer to avoid. We shall therefore make a simplifying assumptionPlanetmathPlanetmath that a single type of propositions Ω is sufficient for all our purposes.

In fact, the construction of the Dedekind reals is quite resilient to logical manipulations. There are several ways in which we can make sense of using a single type Ω:

  1. 1.

    We could identify Ω with the ambiguous 𝖯𝗋𝗈𝗉 and track all the universes that appear in definitions and constructions.

  2. 2.

    We could assume the propositional resizing axiom, as in \autorefsubsec:prop-subsets, which essentially collapses the 𝖯𝗋𝗈𝗉𝒰i’s to the lowest level, which we call Ω.

  3. 3.

    A classical mathematician who is not interested in the intricacies of type-theoretic universes or computation may simply assume the law of excluded middleMathworldPlanetmathPlanetmath (LABEL:eq:lem) for mere propositions so that Ω𝟐. This not only eradicates questions about levels of 𝖯𝗋𝗈𝗉, but also turns everything we do into the standard classical construction of real numbers.

  4. 4.

    On the other end of the spectrum one might ask for a minimalPlanetmathPlanetmath requirement that makes the constructions work. The condition that a mere predicateMathworldPlanetmath be a Dedekind cut is expressible using only conjunctionsMathworldPlanetmath, disjunctionsMathworldPlanetmath, and existential quantifiersMathworldPlanetmath over , which is a countable set. Thus we could take Ω to be the initial σ-frame, i.e., a latticeMathworldPlanetmath with countableMathworldPlanetmath joins in which binary meets distribute over countable joins. (The initial σ-frame cannot be the two-point lattice 𝟐 because 𝟐 is not closed underPlanetmathPlanetmath countable joins, unless we assume excluded middle.) This would lead to a construction of Ω as a higher inductive-inductive type, but one experiment of this kind in \autorefsec:cauchy-reals is enough.

In all of the above cases Ω is a set. Without further ado, we translate the informal definition into type theory. Throughout this chapter, we use the logical notation from \autorefdefn:logical-notation.

Definition 11.2.1.

A Dedekind cut is a pair (L,U) of mere predicates L:QΩ and U:QΩ which is:

  1. 1.

    inhabited: (q:).L(q) and (r:Q).U(r),

  2. 2.

    rounded: for all q,r:,

    L(q) (r:).(q<r)L(r)  𝑎𝑛𝑑
    U(r) (q:).(q<r)U(q),
  3. 3.

    disjoint: ¬(L(q)U(q)) for all q:,

  4. 4.

    located: (q<r)L(q)U(r) for all q,r:.

We let isCut(L,U) denote the conjunction of these conditions. The type of Dedekind reals is

𝖽:\setof(L,U):(Ω)×(Ω)|𝗂𝗌𝖢𝗎𝗍(L,U).

It is apparent that 𝗂𝗌𝖢𝗎𝗍(L,U) is a mere proposition, and since Ω is a set the Dedekind reals form a set too. See \autorefex:RD-extended-reals,ex:RD-lower-cuts,ex:RD-interval-arithmetic for variants of Dedekind cuts which lead to extended reals, lower and upper reals, and the interval domain.

There is an embeddingPlanetmathPlanetmathPlanetmath 𝖽 which associates with each rational q: the cut (Lq,Uq) where

Lq(r):(r<q)  and  Uq(r):(q<r).

We shall simply write q for the cut (Lq,Uq) associated with a rational number.

Title 11.2 Dedekind reals
\metatable