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
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.
For all and , and .
is valid if we assume excluded middle, but without it we get weak linearity
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.
A real is invertible if, and only if, it is apart from .
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 . 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 .
Conversely, if then
defines the desired inverse. Indeed, and are inhabited because . ∎
Theorem 11.2.5 (Archimedean principle for ).
For all if then there merely exists such that .
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.
An ordered field is a set together with constants , , operations , , , , , and mere relations , , such that:
is a commutative ring with unit;
is invertible if, and only if, ;
is a lattice;
the strict order is transitive, irreflexive, and weakly linear ();
apartness is irreflexive, symmetric and cotransitive ();
for all :
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|