Re:The weird and wonderful world of constructive mathematics...
by rocqua on Friday November 09, 2018 @05:39AM
(#18413583)
Technically, f is not well defined. Or rather, indicator functions aren't well defined.
In your case it is not provable that (x > 2 or x =< 2), that would require exactly the law of the excluded middle.
This is explained in one of the later slides.
Re:The weird and wonderful world of constructive mathematics...
by dan-robertson on Saturday November 10, 2018 @06:48PM
(#18424162)
I’ll accept that indicator functions are not well defined in general however I don’t understand why f should be ill-defined. As I understand it, negation is still allowed in intuitionist mathematics, but you don’t get that (not not X -> X). You still get that (not not not X -> not X), and that (X and not X -> bot). Furthermore it is only a general law of the excluded middle that is not allowed and it is quite possible to prove that e.g. (x : R -> (x > 2 and not x < 2 and not x = 2) or (x <= 2 and not x > 2)).
Does it break down somewhere in the definition of continuity?
Re:The weird and wonderful world of constructive mathematics...
by gergoerdi on Tuesday November 13, 2018 @09:18PM
(#18446878)
If `x` is a representation of a real number, how do you compute if it is above or below 2? Suppose you start computing its digits, and you get 2.0000000, you don't know if you will get a non-0 digit later if you keep computing.
I don’t understand how it is possible to have such an axiom. Why can you not construct the function $f : x \mapsto I(x > 2)$ where $I$ is 1 for true, 0 for false. And then prove that the preimage of $(-1,0.5)$ is $(-\infty,2]$ which is not open?