Andrej Bauer: "The countable reals"
Why MathOverflow recommends it
MathOverflow users link it as the primary source for the Bauer-Hanson result that a topos exists with a surjection from the naturals onto the Dedekind reals.
Recommended by 0 people across 0 different months, 2010 to 2023.
What it is
A Topos Institute colloquium talk by Andrej Bauer on joint work with James Hanson, constructing a topos in which the Dedekind reals are countable. The result shows higher-order intuitionistic logic cannot prove the reals uncountable without excluded middle or choice. It builds on a Miller sequence and a modified realizability topos using Turing machines with oracles.
What people said
Cites Timothy Chow · 2010-11 · MathOverflow · on “Proofs of the uncountability of the reals”
Mathematics isn't yet ready to prove results of the form, "Every proof of Theorem T must use Argument A." Think closely about how you might try to prove something like that. You would need to set up some plausible system for mathematics in which Cantor's diagonal argument is blocked and the reals are countable . Nobody has any idea how to do that. The best you can hope for is to look at each proof on a case-by-case basis and decide, subjectively, whether it is "essentially the diagonal argument in disguise." If you're lucky, you'll run into one that your intuition tells you is a fundamentally different proof, and that will settle the question to your satisfaction. But if that doesn't happen,
Cites Ingo Blechschmidt · 2022-09 · MathOverflow · on “Joyal's topos in which $[0,1]$ fails to be compact”
@aws Just to confirm, yes, Andrej's paper [LINK] shows that the realizability topos built using ITTMs has an injection $\mathbb{N}^\mathbb{N}\hookrightarrow\mathbb{N}$, but his argument is easily adapted to $\mathbb{R}\hookrightarrow\mathbb{N}$. (See Footnote 10 of this survey of mine [LINK] for a somewhat self-contained argument.) — Only in the trivial topos there can be a bijection $\mathbb{N}\cong[0,1]$. A topos containing a surjection $\mathbb{N}\to\mathbb{R}$ has recently been found [this video] by Andrej and James Henson.
Cites Sridhar Ramesh · 2022-12 · MathOverflow · on “Intuitionistic consistency of surjection from naturals to reals”
It appears the answer to the original question is finally available now, a decade later, due to Andrej Bauer and James Hanson, the former of which had already provided a helpful response here ten years ago. Though we do not have such a surjection in the effective topos per se, we can use a modification of the effective topos concept to get a nontrivial topos with a surjection from the naturals to the Dedekind reals. See [this video] .
Cites Anon · 2023-08 · MathOverflow · on “Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?”
Last year, Andrej Bauer gave a talk [this video] showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He claims in this abstract [LINK] that this was an open problem. However, it was already known [LINK] that it is consistent with CZF that every set (and in particular, the Dedekind reals) is subcountable. So is Bauer's and Hanson's result actually new? Also note that Bauer's and Hanson's result is not yet published, but it should supposedly be published soon according to Bauer's blog [LINK] . Edit: Thanks to the answers by Andrej Bauer and James Hanson, I have realized my biggest misunderstandi