12
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ 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$. $\endgroup$ Aug 31, 2012 at 8:12
  • 2
    $\begingroup$ Ah, I was right to be unconvinced by my self-convincing, then... :) $\endgroup$ Aug 31, 2012 at 12:32

2 Answers 2

17
$\begingroup$

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.

$\endgroup$
13
  • $\begingroup$ 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}$. $\endgroup$ Aug 31, 2012 at 12:39
  • $\begingroup$ 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}$? $\endgroup$ Aug 31, 2012 at 13:21
  • $\begingroup$ Yes, the same idea more or less, nothing shockingly different. $\endgroup$ Aug 31, 2012 at 15:17
  • $\begingroup$ 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? $\endgroup$ Aug 31, 2012 at 16:50
  • 1
    $\begingroup$ I don't believe that the definition "$e(p) = \sup\{1 \,|\, p \}$" works, since the MacNeille reals are only conditionally complete (any inhabited subset with an upper bound has a least upper bound). One could fix that by changing the definition to "$e(p) = \sup(\{0\} \cup \{1\,|\,p\})$". In any case, @Sridhar: One can prove without any form of choice that for any map from the naturals to the MacNeille reals, there is a MacNeille real which is not in the image of that map. That is to say, the MacNeille reals are constructively uncountable in a strong sense. $\endgroup$ Oct 20, 2018 at 19:35
9
$\begingroup$

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 https://www.youtube.com/watch?v=4CBFUojXoq4.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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