Question

Is it consistent intuitionistically (in the sense of topos theory) for there to be a surjection from the natural numbers to the (Dedekind, let us say) real numbers? [I've managed to convince myself this happens in the effective topos, but not so convincingly as I'd like; I suspect others will be able to answer more confidently and cleanly...]

Answer 1

Theorem (Intuitionistic logic with Dependent Choice): For every sequence $a : \mathbb{N} \to \mathbb{R}$ there is $x \in \mathbb{R}$ such that $|x - a_n| > 0$ for all $n \in \mathbb{N}$.

Proof. Define a nested sequence of closed intervals $I_0 \supseteq I_1 \supseteq I_2 \supseteq \cdots$ such that the length of $I_n$ is $(1/5)^n$, as follows. Begin with $I_0 = [0, 1]$. Suppose $I_n = [u, v]$ has been defined already. Using dependent choice we choose $I_{n+1}$ to be either $[u, (4 u + v)/ 5]$ or $[(u + 4 v)/5, v]$ so that $$a_n > (3 u + 2 v)/5 \Rightarrow I_{n+1} = [u, (4 u + v)/ 5]$$ and $$a_n < (2 u + 3 v)/5 \Rightarrow I_{n+1} = [(u + 4 v)/5, v].$$ (You should draw a picture of $[u,v]$ divided into five equal parts.) Observe that the choice of $I_{n+1}$ guarantees $|y - a_n| > (1/5)^n$ for every $y \in I_{n+1}$.

There is a unique real number $x$ which is contained in all the intervals. It satisfies $|x - a_n| > (1/5)^n$ for all $n \in \mathbb{N}$. QED.

Remark: With a bit of work we can replace Dependent Choice with Number Choice, as is typical in such situations. I will leave it as exercise. (Hint: for every pair of possible endpoints of the intervals, make the choice before constructing the intervals.) Also, the proof works for Dedekind as well as Cauchy reals.

Corollary: There is no surjection $\mathbb{N} \to \mathbb{R}$ in any realizability topos, such as the Effective topos.

Proof. Dependent Choice is valid in a realizability topos. Thus every sequence of reals misses a real by the above theorem. QED.

Now the really interesting question is whether we can do without choice. I remember thinking about this with someone someplace sometime, but we never arrived at a conclusion.

By the way, it is intuitionistically consistent to assume that there is an injection $\mathbb{R} \to \mathbb{N}$. This is validated in Infinite Time Turing Machine (IITM) realizability. But since IITM realizability is a realizability topos, there is no surjection going the other way in this model.