Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
    
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
add comment

1 Answer

up vote 10 down vote accepted

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.

share|improve this answer
    
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
show 7 more comments

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.