7
$\begingroup$

Recently arxiv submitted a new paper (Andrej Bauer, James E. Hanson, The Countable Reals) claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a topos that makes Dedekind reals countable.

I'm wondering if the constructive Eudoxus reals (see R. D. Arthan's The Eudoxus Real Numbers) are sequence-avoiding?

Also, if “all functions $\mathbb{Z} \to \mathbb{Z}$ are computable” holds, what will be the behaviour of Eudoxus reals? Would it become computable?

Improve this question
$\endgroup$
7
  • 5
    $\begingroup$ For reference, here's a bunch of discussion by Andrej Bauer mathoverflow.net/a/453340/4177 $\endgroup$
    – David Roberts ♦
    Commented Apr 12 at 6:22
  • 1
    $\begingroup$ The terminology of constructive real numbers is a giant pile of mess because subtly different concepts sometimes go by the same name or vice versa, and not every author takes the trouble to recall every relevant definition; but IIUC, the nLab page (and this question), the “Eudoxus reals” are the same as the (unmodulated?) Cauchy reals, which seems to be a more standard terminology. If this is correct, I suggest writing “Cauchy reals (aka Eudoxus reals)” in this question, unless you have some reason to emphasize Eudoxus (in which case, maybe state it). $\endgroup$
    – Gro-Tsen
    Commented Apr 12 at 13:05
  • 1
    $\begingroup$ Also, it is worth pointing out explicitly that, according to the Bauer and Hanson paper cited, “the Cauchy reals are sequence-avoiding in any parameterized realizability topos”, so if an example of a topos where the Cauchy=Eudoxus reals are countable is to be found, it should be of a different kind. $\endgroup$
    – Gro-Tsen
    Commented Apr 12 at 13:07
  • 1
    $\begingroup$ OK, now I'm even more confused. The paper you linked to, The Eudoxus Real Numbers by R. D. Arthan, takes place in classical math, and even explicitly states (last paragraph before “sources and remarks”) that the reals they construct are equivalent to the Cauchy and Dedekind ones. I don't see where there are three constructions in it, but even so, there are tons of ways to turn any classical definition into a constructive one. Now there appears to be a somewhat-standard definition of constructive Eudoxus reals, but you say that's not the one you want. [contd…] $\endgroup$
    – Gro-Tsen
    Commented Apr 13 at 6:51
  • 1
    $\begingroup$ […contd.] So, could you kindly spell out exactly what you call the (constructive) “Eudoxus reals” and how they differ from those other Eudoxus reals that happen to be equivalent to the Cauchy reals, and also what is known about the relation between the Eudoxus reals you're interested in and the Cauchy and Dedekind reals. (If you're interested in whether they can be countable, I suppose you already know a few things about them: so, could you summarize that?) $\endgroup$
    – Gro-Tsen
    Commented Apr 13 at 6:55

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .