11.2.1 The algebraic structure of Dedekind reals
The construction of the algebraic and ordertheoretic 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:{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$, we define addition as
${L}_{x+y}\beta \x81\u2019(q)$  $:\beta \x89\u2018\beta \x88\x83(r,s:\mathrm{\beta \x84\x9a}).{L}_{x}(r)\beta \x88\S {L}_{y}(s)\beta \x88\S q=r+s,$  
${U}_{x+y}\beta \x81\u2019(q)$  $:\beta \x89\u2018\beta \x88\x83(r,s:\mathrm{\beta \x84\x9a}).{U}_{x}(r)\beta \x88\S {U}_{y}(s)\beta \x88\S q=r+s,$ 
and the additive inverse by
${L}_{x}\beta \x81\u2019(q)$  $:\beta \x89\u2018\beta \x88\x83(r:\mathrm{\beta \x84\x9a}).{U}_{x}(r)\beta \x88\S q=r,$  
${U}_{x}\beta \x81\u2019(q)$  $:\beta \x89\u2018\beta \x88\x83(r:\mathrm{\beta \x84\x9a}).{L}_{x}(r)\beta \x88\S q=r.$ 
With these operations^{} $({\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}},0,+,)$ is an abelian group^{}. Multiplication is a bit more cumbersome:
${L}_{x\beta \x8b\x85y}\beta \x81\u2019(q)$  $$  
${U}_{x\beta \x8b\x85y}\beta \x81\u2019(q)$  $$ 
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]\beta \x8b\x85[c,d]=[\mathrm{min}\beta \x81\u2018(a\beta \x81\u2019c,a\beta \x81\u2019d,b\beta \x81\u2019c,b\beta \x81\u2019d),\mathrm{max}\beta \x81\u2018(a\beta \x81\u2019c,a\beta \x81\u2019d,b\beta \x81\u2019c,b\beta \x81\u2019d)].$$ 
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, such that $q$ is to the left of $[a,b]\beta \x8b\x85[c,d]$. It is generally useful to think of an interval $[a,b]$ such that ${L}_{x}\beta \x81\u2019(a)$ and ${U}_{x}\beta \x81\u2019(b)$ as an approximation ofΒ $x$, see \autorefex:RDintervalarithmetic.
We now have a commutative ring with unit $({\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}},0,1,+,,\beta \x8b\x85)$. To treat multiplicative inverses^{}, we must first introduce order. Define $\beta \x89\u20ac$ and $$ as
$(x\beta \x89\u20acy)$  $\mathrm{{\rm B}}:\beta \x89\u2018\beta \x88\x80(q:\mathrm{\beta \x84\x9a}).{L}_{x}(q)\beta \x87\x92{L}_{y}(q),$  
$$  $\mathrm{{\rm B}}:\beta \x89\u2018\beta \x88\x83(q:\mathrm{\beta \x84\x9a}).{U}_{x}(q)\beta \x88\S {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}\beta \x81\u2019(q)$ then by roundedness there merely is $r>q$ such that ${L}_{x}\beta \x81\u2019(r)$, and since ${U}_{q}\beta \x81\u2019(r)$ it follows that $$. Conversely, if $$ then there is $r:\mathrm{\beta \x84\x9a}$ such that ${U}_{q}\beta \x81\u2019(r)$ and ${L}_{x}\beta \x81\u2019(r)$, hence ${L}_{x}\beta \x81\u2019(q)$ because ${L}_{x}$ is a lower set. The other half of the proof is symmetric^{}. β
The relation^{} $\beta \x89\u20ac$ 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 with linear order. But if we take $x\beta \x89\u2018u\mathrm{{\rm O}\u0385}$ and $y\beta \x89\u2018u+\mathrm{{\rm O}\u0385}$ for $\mathrm{{\rm O}\u0385}>0$, then we get
$$ 
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 $$. Then there merely exists $q:\mathrm{\beta \x84\x9a}$ such that ${U}_{x}\beta \x81\u2019(q)$ and ${L}_{y}\beta \x81\u2019(q)$. By roundedness there merely exist $r,s:\mathrm{\beta \x84\x9a}$ such that $$, ${U}_{x}\beta \x81\u2019(r)$ and ${L}_{y}\beta \x81\u2019(s)$. Then, by locatedness ${L}_{z}\beta \x81\u2019(r)$ or ${U}_{z}\beta \x81\u2019(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:{\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$ are apart from each other, written $x\#y$, when $$:
$$ 
If $x\#y$, then $\mathrm{{\rm B}\neg}\beta \x81\u2018(x=y)$. The converse is true if we assume excluded middle, but is not provable constructively. Indeed, if $\mathrm{{\rm B}\neg}\beta \x81\u2018(x=y)$ implies $x\#y$, then a little bit of excluded middle follows; see \autorefex:realsapartneqMP.
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 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\beta \x8b\x85y=1$. Then there merely exist $a,b,c,d:\mathrm{\beta \x84\x9a}$ such that $$, $$ and $$. From $$ and $$ it follows that $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}}\beta \x81\u2019(q)$  $$  
${U}_{{x}^{1}}\beta \x81\u2019(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 the form which says that $\mathrm{\beta \x84\x9a}$ is dense in ${\mathrm{\beta \x84\x9d}}_{\mathrm{\pi \x9d\x96\xbd}}$.
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 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 $\mathrm{0}$, $\mathrm{1}$, operations $\mathrm{+}$, $\mathrm{}$, $\mathrm{\beta \x8b\x85}$, $\mathrm{min}$, $\mathrm{max}$, and mere relations $\mathrm{\beta \x89\u20ac}$, $$, $\mathrm{\#}$ such that:

1.
$(F,0,1,+,,\beta \x8b\x85)$ is a commutative ring with unit;

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

3.
$(F,\beta \x89\u20ac,\mathrm{min},\mathrm{max})$ is a lattice^{};

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

5.
apartness $\#$ is irreflexive, symmetric and cotransitive ($x\#y\beta \x87\x92x\#z\beta \x88\xa8y\#z$);

6.
for all $x,y,z:F$:
$x\beta \x89\u20acy$ $$ $$ $$ $x\#y$ $$ $$ $$ $x\beta \x89\u20acy$ $\beta \x87\x94x+z\beta \x89\u20acy+z,$ $x\beta \x89\u20acy\beta \x88\S 0\beta \x89\u20acz$ $\beta \x87\x92x\beta \x81\u2019z\beta \x89\u20acy\beta \x81\u2019z,$ $$ $$ $$ $$ $$ $$ $0$ $$
Every such field has a canonical embedding^{} $\mathrm{Q}\mathrm{\beta \x86\x92}F$. An ordered field is archimedean^{} when 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 theorem plausible. β
Title  11.2.1 The algebraic structure of Dedekind reals 
\metatable 