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...]



Intuitionistic consistency of surjection from naturals to reals
**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](http://math.andrej.com/2011/12/06/embedding-the-baire-space-into-natural-numbers/). But since IITM realizability is a realizability topos, there is no surjection going the other way in this model.


