9 ms·
> 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 real
by kmill 5y ago
> 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.
- logicchains 5y ago>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.
- kmill 5y agoOk, 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).