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\subseteq\mathbb{Q}$ , called the lower and upper cut respectively, which are:

1.

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

rounded: $q\in L\Leftrightarrow\exists(r\in\mathbb{Q}).\,q<r\land r\in L$ and $r\in U\Leftrightarrow\exists(q\in\mathbb{Q}).\,q\in U\land q<r$ ,
3.

disjoint: $\lnot(q\in L\land q\in U)$ , and
4.

located: $q<r\Rightarrow q\in L\lor r\in U$ .

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 theory by saying that a cut is a pair of maps $L,U:\mathbb{Q}\to\mathsf{Prop}$ . But we saw in \autorefsubsec:prop-subsets that $\mathsf{Prop}$ is an ambiguous notation for $\mathsf{Prop}_{\mathcal{U}_{i}}$ where $\mathcal{U}_{i}$ is a universe. Once we use a particular $\mathcal{U}_{i}$ to define cuts, the type of reals will reside in the next universe $\mathcal{U}_{i+1}$ , a property of reals two levels higher in $\mathcal{U}_{i+2}$ , a property of subsets of reals in $\mathcal{U}_{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 assumption that a single type of propositions $\Omega$ 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 $\Omega$ :

1.

We could identify $\Omega$ with the ambiguous $\mathsf{Prop}$ and track all the universes that appear in definitions and constructions.
2.

We could assume the propositional resizing axiom, as in \autorefsubsec:prop-subsets, which essentially collapses the $\mathsf{Prop}_{\mathcal{U}_{i}}$ ’s to the lowest level, which we call $\Omega$ .
3.

A classical mathematician who is not interested in the intricacies of type-theoretic universes or computation may simply assume the law of excluded middle (LABEL:eq:lem) for mere propositions so that $\Omega\equiv\mathbf{2}$ . This not only eradicates questions about levels of $\mathsf{Prop}$ , but also turns everything we do into the standard classical construction of real numbers.
4.

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

In all of the above cases $\Omega$ 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:\mathbb{Q}\to\Omega$ and $U:\mathbb{Q}\to\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}$ ,

$\displaystyle L(q)$ $\displaystyle\Leftrightarrow\exists(r:\mathbb{Q}).\,(q<r)\land L(r)\qquad\text% {and}$

$\displaystyle U(r)$ $\displaystyle\Leftrightarrow\exists(q:\mathbb{Q}).\,(q<r)\land U(q),$
3.

disjoint: $\lnot(L(q)\land U(q))$ for all $q:\mathbb{Q}$ ,
4.

located: $(q<r)\Rightarrow L(q)\lor U(r)$ for all $q,r:\mathbb{Q}$ .

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

\mathbb{R}_{\mathsf{d}}:\!\!\equiv\setof{(L,U):(\mathbb{Q}\to\Omega)\times(% \mathbb{Q}\to\Omega)|\mathsf{isCut}(L,U)}.

It is apparent that $\mathsf{isCut}(L,U)$ is a mere proposition, and since $\mathbb{Q}\to\Omega$ 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 embedding $\mathbb{Q}\to\mathbb{R}_{\mathsf{d}}$ which associates with each rational $q:\mathbb{Q}$ the cut $(L_{q},U_{q})$ where

L_{q}(r):\!\!\equiv(r<q)\qquad\text{and}\qquad U_{q}(r):\!\!\equiv(q<r).

We shall simply write $q$ for the cut $(L_{q},U_{q})$ associated with a rational number.

Title	11.2 Dedekind reals
\metatable

	$\displaystyle L(q)$	$\displaystyle\Leftrightarrow\exists(r:\mathbb{Q}).\,(q<r)\land L(r)\qquad\text% {and}$
	$\displaystyle U(r)$	$\displaystyle\Leftrightarrow\exists(q:\mathbb{Q}).\,(q<r)\land U(q),$