# Intuitionistic consistency of surjection from naturals to reals

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

-
You are wrong about the effective topos. The real numbers are a quotient of a set the natural number there, but this covering set is not the image of a function $\mathbb N\to\mathbb N$. –  Wouter Stekelenburg Aug 31 '12 at 8:12
Ah, I was right to be unconvinced by my self-convincing, then... :) –  Sridhar Ramesh Aug 31 '12 at 12:32

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.

-
Thanks! For what it's worth, the part of my self-convincing that doesn't go through must be the idea that subsingletons of reals surject onto reals (I was imagining this could work by sending a subset of the reals to its least upper bound (I suppose by "reals" here, I really mean something like $[0, 1]$)); had that been so, an injection from $\mathbb{R}$ to $\mathbb{N}$ could be reversed into a surjection from $\mathbb{N}$ to $\mathbb{R}$. –  Sridhar Ramesh Aug 31 '12 at 12:39
Also, just to make sure: the provided link only demonstrates an injection $\mathbb{N}^{\mathbb{N}} \to \mathbb{N}$. I'm assuming essentially the same ideas work when the domain is switched to $\mathbb{R}$? –  Sridhar Ramesh Aug 31 '12 at 13:21
Yes, the same idea more or less, nothing shockingly different. –  Andrej Bauer Aug 31 '12 at 15:17
Also, motivated by the dependence of my original argument on the existence of suprema... is there anything interesting to say about intuitionistic surjections from N onto the MacNeille reals? –  Sridhar Ramesh Aug 31 '12 at 16:50
Doesn't the same argument go through? All you need to know is that a Cauchy sequence of rationals has a limit, which is the case for MacNeille reals. –  Andrej Bauer Aug 31 '12 at 17:56