News for hackers. Stuff that matters.
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.