Skip to main content
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