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?

The Eudoxus Real Numbersby 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$2more comments