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...]
$\begingroup$
$\endgroup$
2
asked Aug 31, 2012 at 6:11
-
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$– Wouter StekelenburgCommented Aug 31, 2012 at 8:12
-
2$\begingroup$ Ah, I was right to be unconvinced by my self-convincing, then... :) $\endgroup$– Sridhar RameshCommented Aug 31, 2012 at 12:32
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
13
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.
answered Aug 31, 2012 at 10:42
-
$\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$ Commented 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$ Commented Aug 31, 2012 at 13:21
-
$\begingroup$ Yes, the same idea more or less, nothing shockingly different. $\endgroup$ Commented 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$ Commented 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$ Commented Oct 20, 2018 at 19:35
$\begingroup$
$\endgroup$
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.
answered Dec 26, 2022 at 15:54