Timeline for Intuitionistic consistency of surjection from naturals to reals
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 20, 2018 at 19:35 | comment | added | Ingo Blechschmidt | 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. | |
| Sep 2, 2012 at 1:50 | comment | added | Sridhar Ramesh | (Also, returning to the dependent choice-based argument against a surjection from N to R, I'm not sure this argument would work when R = MacNeille reals, since it depends on the dichotomy "Either $a_n > (3u + 2v)/5$ or $a_n < (2u + 3v)/5$", which seems an example of precisely the sort of thing which isn't guaranteed for general MacNeille reals) | |
| Sep 1, 2012 at 23:51 | comment | added | Sridhar Ramesh | Well, that's the embedding I'm thinking of too, but it's not obvious to me that $1 \in e(q) \Rightarrow q$. After all, the (only classically injective) lattice homomorphism from $\Omega$ to $\Omega_{\neg \neg}$ is also given by $e(p) = \sup \{1 | p \}$ (as is any suplattice-with-top morphism on the domain $\Omega$). | |
| Sep 1, 2012 at 21:11 | comment | added | Andrej Bauer | Hmm, that is a good point. I was thinking of the embedding $e : \Omega \to [0,1]$ defined by $e(p) = \sup \lbrace 1 \mid p \rbrace$. If $e(p) = e(q)$ then $p \iff 1 \in e(p) \iff 1 \in e(q) \iff q$, therefore $e$ is injective and $\Omega$ is a subobject of $[0,1]$. Am I doing something wrong? It does not matter whether $e$ preserves any lattice structure, it just needs to be an injection. | |
| Sep 1, 2012 at 18:48 | comment | added | Sridhar Ramesh | I like that argument! But it's not obvious to me that the unique complete lattice homomorphism from truth values into MacNeille $[0,1]$ is an embedding. For example, the regular truth values form a nontrivial complete lattice, into which truth values map via double-negation. But this is only an embedding if truth values were Boolean to begin with. So simply being a nontrivial complete lattice is not enough. | |
| Aug 31, 2012 at 20:40 | comment | added | Andrej Bauer | You can embed the object of truth values into MacNeille $[0, 1]$, as you can into any nontrivial complete lattice. So if MacNeille reals were a subobject of $\mathbb{N}$, then so would be the object of truth values, which would imply excluded middle. But excluded middle implies that an uncountable set does not embed into natural numbers. Therefore there is no embedding of MacNeille reals into natural numbers. I hope I got that right, it was sure hard to type it on iPad. | |
| Aug 31, 2012 at 20:26 | comment | added | Andrej Bauer | MacNeille reals are a much more complicated object than the Cauchy/Dedekind reals. Every subobject of the natural numbers object has decidable equality. I doubt the MacNeille reals do, but I would have to think about it. | |
| Aug 31, 2012 at 19:17 | comment | added | Sridhar Ramesh | Right... I guess what I'm wondering, then, is what goes wrong for injecting MacNeille reals into N in IITM realizability that doesn't go wrong for Dedekind reals. Because if the MacNeille [0, 1] does inject into N, then we will have a surjection from N to MacNeille [0, 1] by sending each natural to the supremum of its preimage. (Or did I misunderstand which notion of reals injects into N? Was that not the Dedekind reals?) | |
| Aug 31, 2012 at 17:56 | comment | added | Andrej Bauer | 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. | |
| Aug 31, 2012 at 16:50 | comment | added | Sridhar Ramesh | 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? | |
| Aug 31, 2012 at 15:17 | comment | added | Andrej Bauer | Yes, the same idea more or less, nothing shockingly different. | |
| Aug 31, 2012 at 13:21 | comment | added | Sridhar Ramesh | 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}$? | |
| Aug 31, 2012 at 12:39 | vote | accept | Sridhar Ramesh | ||
| Aug 31, 2012 at 12:39 | comment | added | Sridhar Ramesh | 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}$. | |
| Aug 31, 2012 at 10:50 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 35 characters in body; deleted 17 characters in body
|
| Aug 31, 2012 at 10:42 | history | answered | Andrej Bauer | CC BY-SA 3.0 |