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.

However, mainstream constructive $p$-adic implementation, such as Cauchy $p$-adic and HoTT $p$-adic, or just base-$p$ expansion $p$-adic, are uncountable.

I would like to know:

  1. Is there exists a $p$-adic implementation that is not sequence-avoiding?
  2. Is there a topos in infinite-time Turing machines where the $p$-adic is countable?
  3. If so, how many metrically complete can be hold in this topos? Can $\mathbb{Q}_p,\mathbb{C}_p,\Omega_p$ be countable?
  • 6
    $\begingroup$ $\mathbb{Q}_p$ is always going to be sequence-avoiding. Cantor's diagonal argument is constructive in that context. $\endgroup$ Commented May 12 at 22:06
  • 2
    $\begingroup$ $\mathbb{C}_p$ is a good question. I'm not entirely sure what's going on there. On the other hand, it's unclear to me if the construction of $\Omega_p$ even really makes sense constructively. Usually it's built with an ultrapower. $\endgroup$ Commented May 12 at 22:08
  • $\begingroup$ @JamesEHanson I was actually thinking the same thing: there should be a simple theorem based on fundamentals that clears all p-adic families of sequence-avoiding at once. But my brain didn't catch it. $\endgroup$ Commented May 12 at 23:54
  • $\begingroup$ @JamesEHanson Consider a weak problem, what is the "largest" field that satisfies strong triangle inequality that is uncountable in the classical and not sequence-avoiding in the construction? $\endgroup$ Commented May 13 at 1:36
  • $\begingroup$ That's an interesting question but I'm not sure how to approach it. $\endgroup$ Commented May 14 at 15:20


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.