11.2.1 The algebraic structure of Dedekind reals

The construction of the algebraic and order-theoretic structure of Dedekind reals proceeds as usual in intuitionistic logic. Rather than dwelling on details we point out the differences between the classical and intuitionistic setup. Writing $L_{x}$ and $U_{x}$ for the lower and upper cut of a real number $x:\mathbb{R}_{\mathsf{d}}$ , we define addition as

	$\displaystyle L_{x+y}(q)$	$\displaystyle:\!\!\equiv\exists(r,s:\mathbb{Q}).\,L_{x}(r)\land L_{y}(s)\land q% =r+s,$
	$\displaystyle U_{x+y}(q)$	$\displaystyle:\!\!\equiv\exists(r,s:\mathbb{Q}).\,U_{x}(r)\land U_{y}(s)\land q% =r+s,$

and the additive inverse by

	$\displaystyle L_{-x}(q)$	$\displaystyle:\!\!\equiv\exists(r:\mathbb{Q}).\,U_{x}(r)\land q=-r,$
	$\displaystyle U_{-x}(q)$	$\displaystyle:\!\!\equiv\exists(r:\mathbb{Q}).\,L_{x}(r)\land q=-r.$

With these operations $(\mathbb{R}_{\mathsf{d}},0,{+},{-})$ is an abelian group. Multiplication is a bit more cumbersome:

	$\displaystyle L_{x\cdot y}(q)$	$\displaystyle:\!\!\equiv\begin{aligned} \displaystyle\exists(a,b,c,d:\mathbb{Q% }).&\displaystyle L_{x}(a)\land U_{x}(b)\land L_{y}(c)\land U_{y}(d)\land\\ &\displaystyle\qquad q<\min(a\cdot c,a\cdot d,b\cdot c,b\cdot d),\end{aligned}$
	$\displaystyle U_{x\cdot y}(q)$	$\displaystyle:\!\!\equiv\begin{aligned} \displaystyle\exists(a,b,c,d:\mathbb{Q% }).&\displaystyle L_{x}(a)\land U_{x}(b)\land L_{y}(c)\land U_{y}(d)\land\\ &\displaystyle\qquad\max(a\cdot c,a\cdot d,b\cdot c,b\cdot d)<q.\end{aligned}$

These formulas are related to multiplication of intervals in interval arithmetic, where intervals $[a,b]$ and $[c,d]$ with rational endpoints multiply to the interval

$[a,b]\cdot[c,d]=[\min(ac,ad,bc,bd),\max(ac,ad,bc,bd)].$

For instance, the formula for the lower cut can be read as saying that $q<x\cdot y$ when there are intervals $[a,b]$ and $[c,d]$ containing $x$ and $y$ , respectively, such that $q$ is to the left of $[a,b]\cdot[c,d]$ . It is generally useful to think of an interval $[a,b]$ such that $L_{x}(a)$ and $U_{x}(b)$ as an approximation of $x$ , see \autorefex:RD-interval-arithmetic.

We now have a commutative ring with unit $(\mathbb{R}_{\mathsf{d}},0,1,{+},{-},{\cdot})$ . To treat multiplicative inverses, we must first introduce order. Define $\leq$ and $<$ as

	$\displaystyle(x\leq y)$	$\displaystyle\ :\!\!\equiv\ \forall(q:\mathbb{Q}).\,L_{x}(q)\Rightarrow L_{y}(% q),$
	$\displaystyle(x<y)$	$\displaystyle\ :\!\!\equiv\ \exists(q:\mathbb{Q}).\,U_{x}(q)\land L_{y}(q).$

Lemma 11.2.1.

For all $x:\mathbb{R}_{\mathsf{d}}$ and $q:\mathbb{Q}$ , $L_{x}(q)\Leftrightarrow(q<x)$ and $U_{x}(q)\Leftrightarrow(x<q)$ .

Proof.

If $L_{x}(q)$ then by roundedness there merely is $r>q$ such that $L_{x}(r)$ , and since $U_{q}(r)$ it follows that $q<x$ . Conversely, if $q<x$ then there is $r:\mathbb{Q}$ such that $U_{q}(r)$ and $L_{x}(r)$ , hence $L_{x}(q)$ because $L_{x}$ is a lower set. The other half of the proof is symmetric. ∎

The relation $\leq$ is a partial order, and $<$ is transitive and irreflexive. Linearity

$(x<y)\lor(y\leq x)$

is valid if we assume excluded middle, but without it we get weak linearity

$(x<y)\Rightarrow(x<z)\lor(z<y).$

(11.2.2)

At first sight it might not be clear what (11.2.2) has to do with linear order. But if we take $x\equiv u-\epsilon$ and $y\equiv u+\epsilon$ for $\epsilon>0$ , then we get

$(u-\epsilon<z)\lor(z<u+\epsilon).$

This is linearity “up to a small numerical error”, i.e., since it is unreasonable to expect that we can actually compute with infinite precision, we should not be surprised that we can decide $<$ only up to whatever finite precision we have computed.

To see that (11.2.2) holds, suppose $x<y$ . Then there merely exists $q:\mathbb{Q}$ such that $U_{x}(q)$ and $L_{y}(q)$ . By roundedness there merely exist $r,s:\mathbb{Q}$ such that $r<q<s$ , $U_{x}(r)$ and $L_{y}(s)$ . Then, by locatedness $L_{z}(r)$ or $U_{z}(s)$ . In the first case we get $x<z$ and in the second $z<y$ .

Classically, multiplicative inverses exist for all numbers which are different from zero. However, without excluded middle, a stronger condition is required. Say that $x,y:\mathbb{R}_{\mathsf{d}}$ are apart from each other, written $x\mathrel{\#}y$ , when $(x<y)\lor(y<x)$ :

$(x\mathrel{\#}y):\!\!\equiv(x<y)\lor(y<x).$

If $x\mathrel{\#}y$ , then $\lnot(x=y)$ . The converse is true if we assume excluded middle, but is not provable constructively. Indeed, if $\lnot(x=y)$ implies $x\mathrel{\#}y$ , then a little bit of excluded middle follows; see \autorefex:reals-apart-neq-MP.

Theorem 11.2.3.

A real is invertible if, and only if, it is apart from $0$ .

Remark 11.2.4.

We observe that a real is invertible if, and only if, it is merely invertible. Indeed, the same is true in any ring, since a ring is a set, and multiplicative inverses are unique if they exist. See the discussion following \autorefcor:UC.

Proof.

Suppose $x\cdot y=1$ . Then there merely exist $a,b,c,d:\mathbb{Q}$ such that $a<x<b$ , $c<y<d$ and $0<\min(ac,ad,bc,bd)$ . From $0<ac$ and $0<bc$ it follows that $a$ , $b$ , and $c$ are either all positive or all negative. Hence either $0<a<x$ or $x<b<0$ , so that $x\mathrel{\#}0$ .

Conversely, if $x\mathrel{\#}0$ then

	$\displaystyle L_{x^{-1}}(q)$	$\displaystyle:\!\!\equiv\exists(r:\mathbb{Q}).\,U_{x}(r)\land((0<r\land qr<1)% \lor(r<0\land 1<qr))$
	$\displaystyle U_{x^{-1}}(q)$	$\displaystyle:\!\!\equiv\exists(r:\mathbb{Q}).\,L_{x}(r)\land((0<r\land qr>1)% \lor(r<0\land 1>qr))$

defines the desired inverse. Indeed, $L_{x^{-1}}$ and $U_{x^{-1}}$ are inhabited because $x\mathrel{\#}0$ . ∎

The archimedean principle can be stated in several ways. We find it most illuminating in the form which says that $\mathbb{Q}$ is dense in $\mathbb{R}_{\mathsf{d}}$ .

Theorem 11.2.5 (Archimedean principle for $\mathbb{R}_{\mathsf{d}}$ ).

For all $x,y:\mathbb{R}_{\mathsf{d}}$ if $x<y$ then there merely exists $q:\mathbb{Q}$ such that $x<q<y$ .

Proof.

By definition of $<$ . ∎

Before tackling completeness of Dedekind reals, let us state precisely what algebraic structure they possess. In the following definition we are not aiming at a minimal axiomatization, but rather at a useful amount of structure and properties.

Definition 11.2.6.

An ordered field is a set $F$ together with constants $0$ , $1$ , operations $+$ , $-$ , $\cdot$ , $\min$ , $\max$ , and mere relations $\leq$ , $<$ , $\mathrel{\#}$ such that:

1.

$(F,0,1,{+},{-},{\cdot})$ is a commutative ring with unit;
2.

$x : F$ is invertible if, and only if, $x\mathrel{\#}0$ ;
3.

$(F,{\leq},{\min},{\max})$ is a lattice;
4.

the strict order $<$ is transitive, irreflexive, and weakly linear ( $x<y\Rightarrow x<z\lor z<y$ );
5.

apartness $\mathrel{\#}$ is irreflexive, symmetric and cotransitive ( $x\mathrel{\#}y\Rightarrow x\mathrel{\#}z\lor y\mathrel{\#}z$ );

for all $x, y, z : F$ :

$\displaystyle x\leq y$	$\displaystyle\Leftrightarrow\lnot(y<x),$	$\displaystyle x<y\leq z$	$\displaystyle\Rightarrow x<z,$
$\displaystyle x\mathrel{\#}y$	$\displaystyle\Leftrightarrow(x<y)\lor(y<x),$	$\displaystyle x\leq y<z$	$\displaystyle\Rightarrow x<z,$
$\displaystyle x\leq y$	$\displaystyle\Leftrightarrow x+z\leq y+z,$	$\displaystyle x\leq y\land 0\leq z$	$\displaystyle\Rightarrow xz\leq yz,$
$\displaystyle x<y$	$\displaystyle\Leftrightarrow x+z<y+z,$	$\displaystyle 0<z\Rightarrow(x<y$	$\displaystyle\Leftrightarrow xz<yz),$
$\displaystyle 0<x+y$	$\displaystyle\Rightarrow 0<x\lor 0<y,$	$\displaystyle 0$	$\displaystyle<1.$

Every such field has a canonical embedding $\mathbb{Q}\to F$ . An ordered field is archimedean when for all $x, y : F$ , if $x<y$ then there merely exists $q:\mathbb{Q}$ such that $x<q<y$ .

Theorem 11.2.7.

The Dedekind reals form an ordered archimedean field.

Proof.

We omit the proof in the hope that what we have demonstrated so far makes the theorem plausible. ∎

Title	11.2.1 The algebraic structure of Dedekind reals
\metatable

11.2.1 The algebraic structure of Dedekind reals

Lemma 11.2.1.

Proof.

Theorem 11.2.3.

Remark 11.2.4.

Proof.

Theorem 11.2.5 (Archimedean principle for Rd<math id="Thmprethm2.m1" class="ltx_Math" alttext="\mathbb{R}_{\mathsf{d}}" display="inline"><msub><mi mathvariant="normal">R</mi><mi mathvariant="normal">d</mi></msub></math>).

Proof.

Definition 11.2.6.

Theorem 11.2.7.

Proof.

Theorem 11.2.5 (Archimedean principle for $\mathbb{R}_{\mathsf{d}}$ ).