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 and for
the lower and upper cut of a real number , we define addition as
and the additive inverse by
With these operations is an abelian group
. Multiplication is a bit
more cumbersome:
These formulas are related to multiplication of intervals in interval arithmetic, where
intervals and with rational endpoints multiply to the interval
For instance, the formula for the lower cut can be read as saying that when there are intervals and containing and , respectively, such that is to the left of . It is generally useful to think of an interval such that and as an approximation ofΒ , see \autorefex:RD-interval-arithmetic.
We now have a commutative ring with unit
. To treat
multiplicative inverses, we must first introduce order. Define and as
Lemma 11.2.1.
For all and , and .
Proof.
If then by roundedness there merely is such that , and since
it follows that . Conversely, if then there is such
that and , hence because is a lower set. The other half
of the proof is symmetric.
β
The relation 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 and for , 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 such that and . By roundedness there merely exist such that , and . Then, by locatedness or . 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 are apart from each other, written , when :
If , then . The converse is true if we assume excluded middle, but is not provable constructively. Indeed, if implies , 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 .
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 . Then there merely exist such that , and . From and it follows that , , and are either all positive or all negative. Hence either or , so that .
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 ).
For all if then there merely exists 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 together with constants , , operations , , , , , and mere relations , , such that:
-
1.
is a commutative ring with unit;
-
2.
is invertible if, and only if, ;
-
3.
is a lattice
;
-
4.
the strict order is transitive, irreflexive, and weakly linear ();
-
5.
apartness is irreflexive, symmetric and cotransitive ();
-
6.
for all :
Every such field has a canonical embedding . An ordered field is
archimedean
when for all , if then there merely exists 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 |