Timeline for Uncountability of the real numbers from LLPO without countable choice
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 21, 2020 at 10:13 | comment | added | Andrej Bauer | I wrote down what I think equality of sequences should be in my post, and I think there's no problem at all. It's just the obvious thing. | |
| Mar 21, 2020 at 8:59 | comment | added | Franka Waaldijk | That is a very nice reply, thank you Andrej! Please allow me some time to address the equivalence issue that you mention, as I have a pressing matter outside mathematics. | |
| Mar 21, 2020 at 8:03 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
Trivial edit so I can retract my downvote. Is this really necessary?
|
| Mar 21, 2020 at 8:01 | comment | added | Andrej Bauer | You are correct, I apologize for being so impolite and rash. I was thinking of Cauchy sequences with explicit moduli (essentially the ones you call explicit). Although, if one is going to work without countable choice, one simply shouldn't use Cauchy sequences with $\forall\exists$ definition, as those won't even form a Cauchy-complete field (suitably quotiented). So my only remark left is whether you have a notion of equality of sequences (a la Bishop) that you didn't mention. Otherwise, how is $E$ a subset of reals? | |
| Mar 21, 2020 at 7:13 | comment | added | Franka Waaldijk | I've had enough now. I give a very nice answer to an intriguing question which no one has managed to answer in 2 months time, and my efforts are met with hostile and poor reading, as well as mathematical errors. This is Mathoverflow, supposedly for professionals, and I have no inclination at all to spell out the obvious. | |
| Mar 21, 2020 at 7:07 | comment | added | Franka Waaldijk | Yes but my answer shows a lot more, namely that the uncountable subset contains a representative of all the real equivalence classes. That is precisely the point of using fLLPO. | |
| Mar 21, 2020 at 4:31 | comment | added | wlad | Also, showing that the real numbers contain an uncountable subset is easy: The irrational numbers are always uncountable. And even then, so what? In Recursive foundations, the natural numbers have an uncountable subset | |
| Mar 21, 2020 at 4:28 | comment | added | wlad | Andrej's point is that a Cauchy real number is by definition an equivalence class of Cauchy sequences, rather than a single Cauchy sequence on its own. As a result, your "explicit reals" are not a subset of the real numbers | |
| Mar 20, 2020 at 21:41 | comment | added | Franka Waaldijk | sorry, I should have added that the explicit reals form a field also in the absence of countable choice, but the proof then requires etc. | |
| Mar 20, 2020 at 21:31 | comment | added | Franka Waaldijk | @jkabrg Yes the explicit reals form a field, but the proof calls for tedious bookkeeping, as I mentioned in the answer. | |
| Mar 20, 2020 at 21:29 | comment | added | Franka Waaldijk | @AndrejBauer your last remark is patently untrue. If you think that a simple diagonal argument will show that the Cauchy reals are uncountable, then please write this argument down in an answer of your own... good luck. I repeat there is nothing wrong with my definitions, nor is there anything wrong with my answer. I asked the OP in the comments if the definition of the reals was limited to a specific one and the OP replied: "In fact, you can even use the Cauchy real numbers. The problem appears to be difficult regardless". | |
| Mar 20, 2020 at 18:40 | comment | added | Andrej Bauer | $E$ is not a subset of reals because the real number $0$ is represented by many different explicit reals. Are you using an implied Bishop-style equality relation on $E$, and similarly for $\mathbb{R}$? In this case there is no problem whatsoever with uncountability of reals, because the Cauchy sequences never get quotiented and a simple diagonal argument, much like the one you spelled out, simply works. | |
| Mar 20, 2020 at 18:38 | comment | added | Andrej Bauer | The OP clearly stated that they use the Dedekind reals, whereas you are using rapidly converging Cauchy sequences of rationals and Cauchy reals. The distinction between LLPO and fLLPO is precisely the absence of propositional truncation in the latter. | |
| Mar 20, 2020 at 17:59 | comment | added | Franka Waaldijk | @Andrej: I did not modify the definition of the reals, and if you cannot see the relation between LLPO and fLLPO... well. Do you have a real question here? | |
| Mar 20, 2020 at 17:42 | comment | added | Andrej Bauer | You modified both the definition of reals and LLPO, so I wonder how much your answer is related to the original question. | |
| Mar 20, 2020 at 14:23 | comment | added | wlad | Without assuming countable choice, are the explicit reals a field? | |
| Mar 20, 2020 at 14:16 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
gave a more complete answer.
|
| Mar 16, 2020 at 23:09 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
lay-out
|
| Mar 16, 2020 at 21:55 | history | answered | Franka Waaldijk | CC BY-SA 4.0 |