11.2.1 The algebraic structure of Dedekind reals

The construction of the algebraic and order-theoretic structure of Dedekind reals proceedsas usual in intuitionistic logic. Rather than dwelling on details we point out thedifferences between the classical and intuitionistic setup. Writing $L_x$ and $U_x$ forthe lower and upper cut of a real number $x:{ℝ}_{𝖽}$, we define addition as

$L_{x+y}(q)$$:\equiv \exists (r,s:\mathbb{Q}).L_x(r)\wedge L_y(s)\wedge q=r+s,$

$U_{x+y}(q)$$:\equiv \exists (r,s:\mathbb{Q}).U_x(r)\wedge U_y(s)\wedge q=r+s,$

and the additive inverse by

$L_{-x}(q)$$:\equiv \exists (r:\mathbb{Q}).U_x(r)\wedge q=-r,$

$U_{-x}(q)$$:\equiv \exists (r:\mathbb{Q}).L_x(r)\wedge q=-r.$

With these operations $({ℝ}_{𝖽},0,+,-)$ is an abelian group. Multiplication is a bitmore cumbersome:

$L_{x\cdot y}(q)$

$U_{x\cdot y}(q)$

These formulas are related to multiplication of intervals in interval arithmetic, whereintervals $[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 when there are intervals $[a,b]$ and $[c,d]$ containing $x$ and $y$, respectively, suchthat $q$ is to the left of $[a,b]\cdot [c,d]$. It is generally useful to think of aninterval $[a,b]$ such that $L_x(a)$ and $U_x(b)$ as an approximation of $x$, seeex:RD-interval-arithmetic.

We now have a commutative ring with unit$({ℝ}_{𝖽},0,1,+,-,\cdot )$. To treatmultiplicative inverses, we must first introduce order. Define $\le$ and as

$(x\le y)$$\mathrm{ }:\equiv \forall (q:\mathbb{Q}).L_x(q)\Rightarrow L_y(q),$

$\mathrm{ }:\equiv \exists (q:\mathbb{Q}).U_x(q)\wedge L_y(q).$

Lemma 11.2.1.

For all $x\mathrm{:}{\mathrm{R}}_{\mathrm{d}}$ and $q\mathrm{:}\mathrm{Q}$, and .

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 . Conversely, if then there is $r:\mathbb{Q}$ suchthat $U_q(r)$ and $L_x(r)$, hence $L_x(q)$ because $L_x$ is a lower set. The other halfof the proof is symmetric.∎

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

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

(11.2.2)

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

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

To see that (11.2.2) holds, suppose . 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 , $U_x(r)$and $L_y(s)$. Then, by locatedness $L_z(r)$ or $U_z(s)$. In the first case we get and in the second .

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:{ℝ}_{𝖽}$are apartfrom each other, written $x\#y$, when :

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

Theorem 11.2.3.

A real is invertible if, and only if, it is apart from $\mathrm{0}$.

Remark 11.2.4.

We observe that a real is invertible if, and only if, it is merelyinvertible. Indeed, the same is true in any ring, since a ring is a set, andmultiplicative inverses are unique if they exist. See the discussionfollowing cor:UC.

Proof.

Suppose $x\cdot y=1$. Then there merely exist $a,b,c,d:\mathbb{Q}$ such that, and . From and it followsthat $a$, $b$, and $c$ are either all positive or all negative.Hence either or , so that $x\#0$.

Conversely, if $x\#0$ then

$L_{x^{-1}}(q)$

$U_{x^{-1}}(q)$

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

The archimedean principle can be stated in several ways. We find it most illuminating in theform which says that $\mathbb{Q}$ is dense in ${ℝ}_{𝖽}$.

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

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

Proof.

By definition of .∎

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

Definition 11.2.6.

An ordered fieldis a set $F$ together withconstants $\mathrm{0}$, $\mathrm{1}$, operations $\mathrm{+}$, $\mathrm{-}$, $\mathrm{\cdot }$, $\min$, $\max$, and mere relations$\mathrm{\le }$, , $\mathrm{\#}$ such that:

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

2. $x:F$ is invertible if, and only if, $x\#0$;

3. $(F,\le ,\min ,\max )$ is a lattice;

4. the strict order is transitive, irreflexive,and weakly linear ();

5. apartness $\#$ is irreflexive, symmetric and cotransitive ($x\#y\Rightarrow x\#z\vee y\#z$);

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

   $x\le y$

   $x\#y$

   $x\le y$$\iff x+z\le y+z,$$x\le y\wedge 0\le z$$\Rightarrow xz\le yz,$

   $0$

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

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 theoremplausible.∎