8
$\begingroup$

In constructive mathematics without choice, we have three different versions of the real numbers (each embedding into the next).

  1. Regular Cauchy reals (functions $f : \mathbb N \to \mathbb Q$ such that $|f(n) - f(m)| < 2^{-n} + 2^{-m}$, modulo functions approaching $0$), which are equivalent to the Eudoxus reals (functions from $\mathbb Z$ to $\mathbb Z$ that are almost linear, modulo bounded functions), which are equivalent to Dedekind reals that have a locator (a locator for $r$ is a function $f : \{(p,q) \in \mathbb Q \times \mathbb Q : p < q \} \to \{0, 1\}$ such that $f((p,q)) = 0 \implies p < r$ and $f((p,q)) = 1 \implies r < q$)
  2. Unmodulated Cauchy reals (a.k.a. Cantor reals) (functions $f : \mathbb N \to \mathbb Q$ such that $\forall \varepsilon \in \mathbb Q_+. \exists N \in \mathbb N. \forall n, m \in \mathbb N. |f(n) - f(m)| < \varepsilon$, modulo functions approaching $0$)
  3. Multi-valued Cauchy reals (multi-valued functions that otherwise satisfy the definition of a regular Cauchy real, modulo multi-valued functions approaching 0), which are equivalent to the generalized Cauchy reals, which are equivalent to the multi-valued Eudoxus reals (multi-valued functions that otherwise satisfy the definition of an Eudoxus Cauchy real, modulo bounded multi-valued functions), which are equivalent to the Dedekind reals.

Assuming $\text{AC}_{\mathbb N, 2}$ (which is implied by LEM or countable choice), every Dedekind real has a locator and all these definitions collapse. (When the distinction matters, saying "the real numbers" without qualification usually refers to version 3, since they are only the version that is Cauchy complete.)

Conspicuously missing is a definition in terms of the Dedekind or Eudoxus reals for the second version. Technically we could just take the image of the embedding from the Cantor reals to the third version, but is there a more natural way to define the Eudoxus and/or Dedekind reals that is equivalent to the Cantor reals?

I think the difficulty lies in the difference between functions and total relations (a.k.a. multi-valued functions). The first version of the real numbers only involves functions. The third version only involves total relations.

The second version is a weird mix of both; $f$ is given to be a single-valued function but the relationship between $\varepsilon$ and $N$ is that of a total relation. The difference between the sequence of approximations and the rate of convergence simply doesn't show up in the definitions of the Dedekind reals and Eudoxus reals.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ There are at least two other definitions I can think of: namely the smallest subset of the Dedekind reals which contains the rationals and is closed under limits of unmodulated Cauchy sequences (resp. under limits of modulated Cauchy sequences). I haven't thought about them too much, so maybe they collapse, and this doesn't really relate to your question, but your mention that the multi-valued Cauchy reals “are only the version that is Cauchy complete” made me think of this, as the reals I mention are, by definition, unmodulated-Cauchy-complete (resp. modulated-Cauchy-complete). $\endgroup$
    – Gro-Tsen
    Commented Aug 14 at 18:47
  • 2
    $\begingroup$ (And of course we might mention all sorts of other Dedekind-related reals: like the “MacNeille reals”, also known as the “bounded extended” reals in Troelstra & van Dale — I think they're the same thing —, and the “classical” reals from op. cit. — which I think are the $\neg\neg$-sheafification of the Dedekind reals. Someone should really write a guide to the 1729 flavors of “real numbers” in constructive math!) $\endgroup$
    – Gro-Tsen
    Commented Aug 14 at 18:54
  • $\begingroup$ @Gro-Tsen each one also leads to a different notion of "completion of a metric space". Given a metric space $M$, its completion is the set of functions $f : M \to \mathbb R$ such that $\forall x, y \in M. |d(x,y) - f(y)| \le f(x)$ and $\forall \epsilon \in \mathbb Q_+. \exists x \in M. f(x) < \epsilon$. The completeness properties of this space depends on the completeness properties of the $\mathbb R$ used. $\endgroup$
    – Christopher King
    Commented Aug 14 at 19:20
  • $\begingroup$ @Gro-Tsen I think the normal definition of the MacNeille reals requires that the sets of upper and lower bounds be inhabited. I'm guessing that the elements of the $\neg\neg$-sheafification of the Dedekind reals would only in general have these be non-empty. $\endgroup$
    – James E Hanson
    Commented Aug 15 at 4:53
  • $\begingroup$ @JamesEHanson I agree. My sentence was awfully convoluted: ⓐthe Troelstra & van Dalen “bounded extended” reals require the two parts of the cut to be inhabited (and I think they're the same as MacNeille reals); whereas ⓑthe T&vD “classical” reals require both parts to be non-empty; and it's the latter which I think are the $\neg\neg$-sheafification of the Dedekind reals. But this is all a digression wrt OP's question, I'm just playing the part of the guy who likes to draw attention to the fact that there are at least $7$ flavors of “reals” not to be confused. $\endgroup$
    – Gro-Tsen
    Commented Aug 15 at 9:50

0

Reset to default

You must log in to answer this question.