Skip to main content
2 of 4
tags, links, paper details
David Roberts
  • 35.5k
  • 11
  • 124
  • 349

The constructive Eudoxus reals

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 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?