Timeline for Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Current License: CC BY-SA 4.0
28 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 21, 2023 at 4:38 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
linked to comment, fixed typo
|
| Sep 5, 2023 at 22:42 | comment | added | Simon Henry | @AndrejBauer no this time Idisagree. I clearly said "depending which classically equivalent definition of countable and of the reals you are using". Subcountable is a very reasonable classicaly equivalent way to define what countable mean. Sorry I had missed your question above! | |
| Sep 5, 2023 at 22:05 | comment | added | Andrej Bauer | @SimonHenry: In your Edit you state: it was already known that "You cannot prove the reals are uncountable in IZF(that is ZFC without AC and LEM)". No, this was not known at all, not to my knowledge. Where did you get this from? What was known is: "You cannot prove the reals are not subcountable" (because they are subcountable in the effective topos) – but that is a very different statement. | |
| Sep 5, 2023 at 21:59 | comment | added | Andrej Bauer | @Nikolaj-K: Beautiful, thanks you. Here's one way to reduce your argument to the usual Cantor's theorem: given $S \subseteq \mathbb{N}$, there is a surjection $h : P\mathbb{N} \to PS$, namely $h(B) = B \cap S$. if we had a surjection $S \to P\mathbb{N}$, then $h \circ f : S \to PS$ would be a surjection also, contradicting Cantor's theorem. | |
| Sep 5, 2023 at 17:43 | comment | added | Nikolaj-K | @AndrejBauer As for the question from the 23th, that should also be just taking a $f\colon S\to {\mathcal P}{\mathbb N}$, looking at $D=\{n\in {\mathbb N}\mid n\in S\setminus f(n)\}$ and finding $f(k)=D$ implies $k\in D\leftrightarrow k\notin D$. It's stated for ECTS+recursion in the Aczel/Rathjen book draft p.79 but I've also seen it elsewhere. That set theory context has Replacement and uses Separation in a way where the subset $D\in{\mathcal P}{\mathbb N}$ is broader than as with $2^{\mathbb N}$ where subcountability remains permitted. | |
| Aug 31, 2023 at 12:57 | comment | added | aws | The construction of the Dedekind reals in CZF is a classic application of subset collection. With only exponentiation instead of subset collection, it is not possible. | |
| Aug 25, 2023 at 0:53 | history | edited | Simon Henry | CC BY-SA 4.0 |
deleted 112 characters in body
|
| Aug 25, 2023 at 0:51 | comment | added | Simon Henry | Thanks, that is very surprising - I need to look at this... | |
| Aug 24, 2023 at 21:39 | comment | added | David Roberts♦ | Martin Escardo pointed out elsewhere that CZF does actually construct the Dedekind reals as a set: Crosilla, L., Ishihara, H. and Schuster, P. (2005) “On constructing completions,” The Journal of Symbolic Logic. Cambridge University Press, 70(3), pp. 969–978. doi: 10.2178/jsl/1122038923. | |
| Aug 24, 2023 at 2:36 | comment | added | Simon Henry | something like this can be said everytime one says that something can't be proved "without xyz" though... but I've removed that unfortunate phrasing, because you are right - it doesn't mean anything. | |
| Aug 24, 2023 at 2:34 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 59 characters in body
|
| Aug 23, 2023 at 22:49 | comment | added | Andrej Bauer | @SimonHenry: Excuse me for complaining so much, but it is not true that one "needs LEM to show that the reals are uncountable". Countable choice also suffices. | |
| Aug 23, 2023 at 22:12 | comment | added | Andrej Bauer | @SimonHenry: The usual Cantor's diagonal argument shows that there is no surjection $\mathbb{N} \to P(\mathbb{N})$. How do you get from that we cannot show subcountability of $P(\mathbb{N})$? | |
| Aug 23, 2023 at 20:13 | comment | added | LSpice | I edited to do some proofreading. In particular, I assume that the references to "the real" and "the natural number" were supposed to be "the [set of] reals" and "the [set of] natural numbers", and edited accordingly. If I am mangling usual jargon thereby, then I apologise. I also tried to link to @AndrejBauer's comment that you referenced, but I wasn't sure which one you meant, so I just linked both in this thread (although there is also another comment above). I hope this was correct. | |
| Aug 23, 2023 at 20:12 | history | edited | LSpice | CC BY-SA 4.0 |
Proofreading and links
|
| Aug 23, 2023 at 19:56 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 1005 characters in body
|
| Aug 23, 2023 at 19:47 | comment | added | Simon Henry | Oh right. Sorry, In that case I withdraw my objection and will edit my answer! | |
| Aug 23, 2023 at 19:01 | comment | added | Andrej Bauer | Yes, it was known that there is a topos in which $\mathbb{R}$ is subcountable (a quotient of a subset of $\mathbb{N}$), namely the effective topos. | |
| Aug 23, 2023 at 18:57 | comment | added | Simon Henry | @Andrej Thanks for pointing this out, I should have mentioned it but I still believe the difference between predicative and intuitionist is the main point: Was it know before that it is consistent in IZF/topos logic that the real are subcountable? To me the OP was aware of the distinction (because different name!) but considered that it was maybe not important enough to be the novelty in your result... But maybe I'm just projecting my own opinion here. And in any case, you are right that it is good to spell it out! | |
| Aug 23, 2023 at 17:27 | comment | added | Andrej Bauer | This answer fails to call out the OP's unspoken false assumption, namely that somehow subcountability implies countability. Constructively we cannot show that an injection from $A \to B$ with $A$ inhabited yields a surjection $B \to A$ (in any variation of constructive mathematics, because we would get excluded middle). All this talk about predicativity, and flavors of constructive mathematics, etc., is a red herring. | |
| Aug 23, 2023 at 16:36 | comment | added | Simon Henry | Absolutely. "ZFC without choice and LEM" is IZF (of course up to details as "ZFC without xyz" doesn't mean anything), which is considerably stronger than CZF. | |
| Aug 23, 2023 at 16:29 | vote | accept | Anon | ||
| Aug 29, 2023 at 15:18 | |||||
| Aug 23, 2023 at 16:29 | comment | added | Anon | I see, so in some sense, CZF removes more than just choice and LEM. So when Bauer says "Can the real numbers be shown uncountable without excluded middle and without the axiom of choice? An answer has not been found so far", the CZF result did not give an answer because it was even weaker than the stated question. But now Bauer's and Hanson's topos result resolves the question (I think). | |
| Aug 23, 2023 at 16:21 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 54 characters in body
|
| Aug 23, 2023 at 16:16 | comment | added | Simon Henry | Oh sorry, I've corrected! | |
| Aug 23, 2023 at 16:16 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 54 characters in body
|
| Aug 23, 2023 at 16:15 | comment | added | Anon | To clarify, my understanding is that the topos construction is joint work between Bauer and Hanson together. | |
| Aug 23, 2023 at 16:11 | history | answered | Simon Henry | CC BY-SA 4.0 |