11.2 Dedekind reals

Let us first recall the basic idea of Dedekind’s construction. We use two-sided Dedekindcuts, as opposed to an often used one-sided version, because the symmetry makesconstructions more elegant, and it works constructively as well as classically.A Dedekind cut consists of a pair $(L,U)$ of subsets $L,U\subseteq \mathbb{Q}$, called thelower and upper cut respectively, which are:

1. inhabited: there are $q\in L$ and $r\in U$,

2. rounded: and ,

3. disjoint: $\mathrm{\neg }(q\in L\wedge q\in U)$, and

4. located: .

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. Thelocatedness condition states that there is no large gap between $L$ and $U$. Because cutsare always open, they never include the “point in between”, even when it is rational. Atypical Dedekind cut looks like this:

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

We might naively translate the informal definition into type theory by saying that a cutis a pair of maps $L,U:\mathbb{Q}\to \mathrm{𝖯𝗋𝗈𝗉}$. But we saw in subsec:prop-subsets that$\mathrm{𝖯𝗋𝗈𝗉}$ is an ambiguous notation for ${\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_i}$ where ${𝒰}_i$ is a universe. Once weuse a particular ${𝒰}_i$ to define cuts, the type of reals will reside in the nextuniverse ${𝒰}_{i+1}$, a property of reals two levels higher in ${𝒰}_{i+2}$, a property ofsubsets of reals in ${𝒰}_{i+3}$, etc. In principle we should be able to keep track of theuniverse levels, especially with the help of a proof assistant, but doing so here wouldjust burden us with bureaucracy that we prefer to avoid. We shall therefore make asimplifying assumption that a single type of propositions $\mathrm{\Omega }$ is sufficient for allour purposes.

In fact, the construction of the Dedekind reals is quite resilient to logicalmanipulations. There are several ways in which we can make sense of using a single type$\mathrm{\Omega }$:

1. We could identify $\mathrm{\Omega }$ with the ambiguous $\mathrm{𝖯𝗋𝗈𝗉}$ and track all the universesthat appear in definitions and constructions.

2. We could assume the propositional resizing axiom,as in subsec:prop-subsets, which essentially collapses the ${\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_i}$’s to thelowest level, which we call $\mathrm{\Omega }$.

3. A classical mathematician who is not interested in the intricacies of type-theoreticuniverses or computation may simply assume the law of excluded middle (LABEL:eq:lem) formere propositions so that $\mathrm{\Omega }\equiv \mathrm{𝟐}$.This not only eradicates questions aboutlevels of $\mathrm{𝖯𝗋𝗈𝗉}$, but also turns everything we do into the standard classicalconstruction of real numbers.

4. On the other end of the spectrum one might ask for a minimal requirement that makesthe constructions work. The condition that a mere predicate be a Dedekind cut isexpressible using only conjunctions, disjunctions, and existential quantifiers over $\mathbb{Q}$, whichis a countable set. Thus we could take $\mathrm{\Omega }$ to be the initial $\sigma$-frame,i.e., a lattice with countable joins in which binary meets distribute over countablejoins. (The initial $\sigma$-frame cannot be the two-point lattice $\mathrm{𝟐}$ because$\mathrm{𝟐}$ is not closed under countable joins, unless we assume excluded middle.) Thiswould lead to a construction of $\mathrm{\Omega }$ as a higher inductive-inductive type, but oneexperiment of this kind in sec:cauchy-reals is enough.

In all of the above cases $\mathrm{\Omega }$ is a set.Without further ado, we translate the informal definition into type theory.Throughout this chapter, we use thelogical notation from defn:logical-notation.

Definition 11.2.1.

A Dedekind cutis a pair $\mathrm{(}L\mathrm{,}U\mathrm{)}$ of mere predicates $L\mathrm{:}\mathrm{Q}\mathrm{\to }\mathrm{\Omega }$ and $U\mathrm{:}\mathrm{Q}\mathrm{\to }\mathrm{\Omega }$ which is:

1. inhabited: $\exists (q:\mathbb{Q}).L(q)$ and $\exists (r:Q).U(r)$,

2. rounded: for all $q,r:\mathbb{Q}$,

   $L(q)$

   $U(r)$

3. disjoint: $\mathrm{\neg }(L(q)\wedge U(q))$ for all $q:\mathbb{Q}$,

4. located: for all $q,r:\mathbb{Q}$.

We let $\mathrm{isCut}\mathit{}\mathrm{(}L\mathrm{,}U\mathrm{)}$ denote the conjunction of these conditions. The type ofDedekind reals is

$${ℝ}_{𝖽}:\equiv (L,U):(\mathbb{Q}\to \mathrm{\Omega })\times (\mathbb{Q}\to \mathrm{\Omega })|\mathrm{𝗂𝗌𝖢𝗎𝗍}(L,U).$$

It is apparent that $\mathrm{𝗂𝗌𝖢𝗎𝗍}(L,U)$ is a mere proposition, and since $\mathbb{Q}\to \mathrm{\Omega }$ is aset the Dedekind reals form a set too. Seeex:RD-extended-reals,ex:RD-lower-cuts,ex:RD-interval-arithmetic for variants ofDedekind cuts which lead to extended reals, lower and upper reals, and the intervaldomain.

There is an embedding $\mathbb{Q}\to {ℝ}_{𝖽}$ which associates with each rational $q:\mathbb{Q}$ the cut$(L_q,U_q)$ where

We shall simply write $q$ for the cut $(L_q,U_q)$ associated with a rational number.