Timeline for Uncountability of the real numbers from LLPO without countable choice
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 22, 2020 at 14:25 | history | edited | wlad |
edited tags
|
|
| Mar 21, 2020 at 8:24 | answer | added | Andrej Bauer | timeline score: 3 | |
| Mar 20, 2020 at 16:09 | history | edited | YCor |
edited tags
|
|
| Mar 16, 2020 at 21:55 | answer | added | Franka Waaldijk | timeline score: 4 | |
| Dec 28, 2019 at 19:51 | comment | added | Andrej Bauer | I would try to port Bas Spitters' example (Appendix A of this note) to Johstone's topological topos. If you can do that, you'll show that LLPO cannot prove the strong form of uncountability. If you cannot do it, it migth give you a clue on how to prove it. | |
| Dec 28, 2019 at 19:45 | comment | added | wlad | @tj_ The point is that LLPO is a non-constructive principle because there's no effective procedure for deciding which of $x \leq 0$ or $x \geq 0$ is true. So by working in a restricted logic which doesn't have Excluded Middle or Countable Choice, but does have access to the non-constructive principle LLPO, can we still prove the real numbers uncountable? | |
| Dec 28, 2019 at 19:34 | comment | added | wlad | @AndrejBauer Thank you. I haven't seen that thread before | |
| Dec 28, 2019 at 19:22 | comment | added | Andrej Bauer | Also, are you aware of Ingo Blechsmidt's recap at groups.google.com/forum/#!topic/constructivenews/jSvzqu1LUis? | |
| Dec 28, 2019 at 19:20 | comment | added | Andrej Bauer | My guess would be that LLPO is not going to help with uncountability of reals, at least not the strong form "for every sequence of reals there is a real that avoids it". This is so because LLPO does not allow you to construct a discontinuous map (in the Johstone topological topos LLPO holds but there are no discontinuous maps there). As soon as you can construct maps that "jump", you can employ Levy-type proofs of uncountability, see this note. | |
| Dec 28, 2019 at 19:17 | comment | added | wlad | @AndrejBauer Yes, and this is a stepping stone towards that | |
| Dec 28, 2019 at 18:58 | comment | added | Andrej Bauer | Hmm, it's doable if $\forall x \in \mathbb{R} . x \geq 0 \lor \lnot (x \geq 0)$ but I don't see immediately how we'd do it just with analytic LLPO. Interesting question! Are you trying to show that the reals are uncountable without choice, by any chance? | |
| Dec 28, 2019 at 18:31 | history | edited | wlad | CC BY-SA 4.0 |
edited title
|
| Dec 28, 2019 at 18:28 | comment | added | wlad | @Frank'aWaaldijk In fact, you can even use the Cauchy real numbers. The problem appears to be difficult regardless | |
| Dec 28, 2019 at 10:35 | comment | added | wlad | @Frank'aWaaldijk I'm defining the real numbers using Dedekind cuts | |
| Dec 28, 2019 at 9:34 | comment | added | Franka Waaldijk | in order to understand your question i seem to need your definition/construction of the real numbers, since this alone is not trivial in the absence of countable choice. | |
| Dec 28, 2019 at 7:53 | comment | added | wlad | @MikeShulman Yes, but it also uses countable choice, which I'm not allowing | |
| Dec 28, 2019 at 2:10 | comment | added | Mike Shulman | Isn't the usual proof perfectly constructive, without using any classicality axioms? | |
| Dec 28, 2019 at 1:02 | comment | added | tj_ | Note that $x\le 0$ or $0\le x$ holds for all (countably many) rational $x$. So you will need further properties of the reals to prove uncoutability. | |
| Dec 28, 2019 at 0:46 | history | edited | wlad |
edited tags
|
|
| Dec 27, 2019 at 23:26 | history | edited | wlad | CC BY-SA 4.0 |
deleted 577 characters in body
|
| Dec 27, 2019 at 23:26 | history | undeleted | wlad | ||
| Dec 27, 2019 at 22:59 | history | deleted | wlad | via Vote | |
| Dec 27, 2019 at 22:44 | history | asked | wlad | CC BY-SA 4.0 |