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
7 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Sep 6, 2023 at 11:02 | history | edited | Sam Sanders | CC BY-SA 4.0 |
added 17 characters in body
|
Sep 6, 2023 at 10:50 | comment | added | Andrej Bauer | "There is injection $X \to \mathbb{N}$" is not countability of X. That is subcountability. Countability (for inhabited $X$) is "there is a surjection $ \mathbb{N}\to X$". Please see my answer where I clarify these notions. They seem to be creating some confusion. | |
Sep 6, 2023 at 10:48 | comment | added | Sam Sanders | @AndrejBauer Firstly, the same 'hardness' result holds for Cantor space, Baire space, and the reals with your favourite representation. I have clarified this in my answer. Secondly, which of the probably hundreds of "usual" proofs are you talking about? You need "a lot" of excluded middle/comprehension/... to prove NIN. | |
Sep 6, 2023 at 10:46 | history | edited | Sam Sanders | CC BY-SA 4.0 |
added some info based on Andrej Bauer's comments
|
Sep 5, 2023 at 22:07 | comment | added | Andrej Bauer | And furthermore, how are classical theories relevant here? With excluded middle you can just show, using the usual proof, that the reals are uncountable. | |
Sep 5, 2023 at 21:50 | comment | added | Andrej Bauer | Excuse me, but what does the Cantor space have to do with the Dedekind reals? | |
Aug 24, 2023 at 18:51 | history | answered | Sam Sanders | CC BY-SA 4.0 |