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)

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 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 $\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 and $U_{x}(q)\Leftrightarrow(x.

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. Conversely, if $q 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  . ∎

 $(x

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

 $(x (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

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. 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, $U_{x}(r)$ and $L_{y}(s)$. Then, by locatedness $L_{z}(r)$ or $U_{z}(s)$. In the first case we get $x and in the second $z.

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:

 $(x\mathrel{\#}y):\!\!\equiv(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.

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, $c and $0<\min(ac,ad,bc,bd)$. From $0 and $0 it follows that $a$, $b$, and $c$ are either all positive or all negative. Hence either $0 or $x, 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 $\displaystyle U_{x^{-1}}(q)$ $\displaystyle:\!\!\equiv\exists(r:\mathbb{Q}).\,L_{x}(r)\land((01)% \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 then there merely exists $q:\mathbb{Q}$ such that $x.

Proof.

By definition of $<$. ∎

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

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

2. 2.

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

3. 3.

$(F,{\leq},{\min},{\max})$

4. 4.

the strict order $<$ is transitive, irreflexive, and weakly linear ($x);

5. 5.

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

6. 6.

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

 $\displaystyle x\leq y$ $\displaystyle\Leftrightarrow\lnot(y $\displaystyle x $\displaystyle\Rightarrow x $\displaystyle x\mathrel{\#}y$ $\displaystyle\Leftrightarrow(x $\displaystyle x\leq y $\displaystyle\Rightarrow x $\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 $\displaystyle\Leftrightarrow x+z $\displaystyle 0 $\displaystyle\Leftrightarrow xz $\displaystyle 0 $\displaystyle\Rightarrow 0 $\displaystyle 0$ $\displaystyle<1.$

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

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