Re:How many real numbers exist? New proof moves closer to an...
by logicchains on Saturday July 24, 2021 @12:17AM
(#27938358)
>suppose we define the reals through Dedekind cuts
You can't define the classical reals this way in a constructive setting, only the computable reals.
Re:How many real numbers exist? New proof moves closer to an...
by kmill on Saturday July 24, 2021 @01:56PM
(#27943043)
Ok, but I'm not sure what your point is. Throwing out only the axiom of choice (which is the difference between ZFC and ZF) does not make things constructive. If you're thinking of Diaconescu's theorem, it's that choice implies the law of the excluded middle, but the converse is certainly not true.
I was objecting to this:
> Generally a lot of counter-intuitive constructions disappear when eliminating the axiom of choice (such as [...] non-continuous functions).
I think the step function doesn't depend on choice. Say f(x) = 0 if x < 0 and f(x) = 1 if x >= 0. Also, suppose we define the reals through Dedekind cuts. We can define f(x) by checking whether 0 is an element of x as a cut. We can prove f is discontinuous in the usual way.
What I had heard is that Brouwer proved, using some kind of constructive/intuitionistic logic, that every function is continuous, but ZF is still based in classical logic. I believe the step function is not definable constructively.