11.2.1 The algebraic structure of Dedekind reals

The construction of the algebraic and order-theoretic structureMathworldPlanetmath of Dedekind reals proceeds as usual in intuitionistic logicMathworldPlanetmath. Rather than dwelling on details we point out the differencesPlanetmathPlanetmath between the classical and intuitionistic setup. Writing Lx and Ux for the lower and upper cut of a real number x:ℝ𝖽, we define addition as

Lx+y⁒(q) :β‰‘βˆƒ(r,s:β„š).Lx(r)∧Ly(s)∧q=r+s,
Ux+y⁒(q) :β‰‘βˆƒ(r,s:β„š).Ux(r)∧Uy(s)∧q=r+s,

and the additive inverse by

L-x⁒(q) :β‰‘βˆƒ(r:β„š).Ux(r)∧q=-r,
U-x⁒(q) :β‰‘βˆƒ(r:β„š).Lx(r)∧q=-r.

With these operationsMathworldPlanetmath (ℝ𝖽,0,+,-) is an abelian groupMathworldPlanetmath. Multiplication is a bit more cumbersome:

Lxβ‹…y⁒(q) :β‰‘βˆƒ(a,b,c,d:β„š).Lx⁒(a)∧Ux⁒(b)∧Ly⁒(c)∧Uy⁒(d)∧q<min⁑(aβ‹…c,aβ‹…d,bβ‹…c,bβ‹…d),
Uxβ‹…y⁒(q) :β‰‘βˆƒ(a,b,c,d:β„š).Lx⁒(a)∧Ux⁒(b)∧Ly⁒(c)∧Uy⁒(d)∧max⁑(aβ‹…c,aβ‹…d,bβ‹…c,bβ‹…d)<q.

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


For instance, the formula for the lower cut can be read as saying that q<xβ‹…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]β‹…[c,d]. It is generally useful to think of an interval [a,b] such that Lx⁒(a) and Ux⁒(b) as an approximation ofΒ x, see \autorefex:RD-interval-arithmetic.

We now have a commutative ring with unit (ℝ𝖽,0,1,+,-,β‹…). To treat multiplicative inversesMathworldPlanetmath, we must first introduce order. Define ≀ and < as

(x≀y) Β :β‰‘βˆ€(q:β„š).Lx(q)β‡’Ly(q),
(x<y) Β :β‰‘βˆƒ(q:β„š).Ux(q)∧Ly(q).
Lemma 11.2.1.

For all x:Rd and q:Q, Lx(q)⇔(q<x) and Ux(q)⇔(x<q).


If Lx⁒(q) then by roundedness there merely is r>q such that Lx⁒(r), and since Uq⁒(r) it follows that q<x. Conversely, if q<x then there is r:β„š such that Uq⁒(r) and Lx⁒(r), hence Lx⁒(q) because Lx is a lower set. The other half of the proof is symmetricPlanetmathPlanetmath. ∎

The relationMathworldPlanetmathPlanetmath ≀ is a partial orderMathworldPlanetmath, and < is transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath and irreflexiveMathworldPlanetmath. Linearity


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

(x<y)β‡’(x<z)∨(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≑u-Ο΅ and y≑u+Ο΅ for Ο΅>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 infiniteMathworldPlanetmathPlanetmath 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:β„š such that Ux⁒(q) and Ly⁒(q). By roundedness there merely exist r,s:β„š such that r<q<s, Ux⁒(r) and Ly⁒(s). Then, by locatedness Lz⁒(r) or Uz⁒(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:ℝ𝖽 are apart from each other, written x#y, when (x<y)∨(y<x):


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

Theorem 11.2.3.

A real is invertiblePlanetmathPlanetmath 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.


Suppose xβ‹…y=1. Then there merely exist a,b,c,d:β„š such that a<x<b, c<y<d and 0<min⁑(a⁒c,a⁒d,b⁒c,b⁒d). From 0<a⁒c and 0<b⁒c 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#0.

Conversely, if x#0 then

Lx-1⁒(q) :β‰‘βˆƒ(r:β„š).Ux(r)∧((0<r∧qr<1)∨(r<0∧1<qr))
Ux-1⁒(q) :β‰‘βˆƒ(r:β„š).Lx(r)∧((0<r∧qr>1)∨(r<0∧1>qr))

defines the desired inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. Indeed, Lx-1 and Ux-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 β„š is dense in ℝ𝖽.

Theorem 11.2.5 (Archimedean principle for Rd).

For all x,y:Rd if x<y then there merely exists q:Q such that x<q<y.


By definition of <. ∎

Before tackling completeness of Dedekind reals, let us state precisely what algebraic structurePlanetmathPlanetmath they possess. In the following definition we are not aiming at a minimalPlanetmathPlanetmath 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 +, -, β‹…, min, max, and mere relations ≀, <, # such that:

  1. 1.

    (F,0,1,+,-,β‹…) is a commutative ring with unit;

  2. 2.

    x:F is invertible if, and only if, x#0;

  3. 3.

    (F,≀,min,max) is a latticeMathworldPlanetmath;

  4. 4.

    the strict order < is transitive, irreflexive, and weakly linear (x<yβ‡’x<z∨z<y);

  5. 5.

    apartness # is irreflexive, symmetric and cotransitive (x#yβ‡’x#z∨y#z);

  6. 6.

    for all x,y,z:F:

    x≀y ⇔¬⁑(y<x), x<y≀z β‡’x<z,
    x#y ⇔(x<y)∨(y<x), x≀y<z β‡’x<z,
    x≀y ⇔x+z≀y+z, x≀y∧0≀z β‡’x⁒z≀y⁒z,
    x<y ⇔x+z<y+z, 0<zβ‡’(x<y ⇔xz<yz),
    0<x+y β‡’0<x∨0<y, 0 <1.

Every such field has a canonical embeddingMathworldPlanetmathPlanetmathPlanetmath Q→F. An ordered field is archimedeanPlanetmathPlanetmathPlanetmathPlanetmath when for all x,y:F, if x<y then there merely exists q:Q such that x<q<y.

Theorem 11.2.7.

The Dedekind reals form an ordered archimedean field.


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