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).

Proof.

Definition 11.2.6.

Theorem 11.2.7.

Proof.

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