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.
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.