8
$\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.

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?
Improve this question
$\endgroup$
6
  • 7
    $\begingroup$ $\mathbb{Q}_p$ is always going to be sequence-avoiding. Cantor's diagonal argument is constructive in that context. $\endgroup$
    – James E Hanson
    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$
    – James E Hanson
    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$
    – Ember Edison
    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$
    – Ember Edison
    Commented May 13 at 1:36
  • $\begingroup$ That's an interesting question but I'm not sure how to approach it. $\endgroup$
    – James E Hanson
    Commented May 14 at 15:20

0

Reset to default

You must log in to answer this question.