Hacker News Reader

Comment by logicchains | Hacker News Reader

The continuous requires the law of the excluded middle, which makes it harder to imagine as it's not easy to "construct" an image of x in our mind purely from a proof of "not not x". That's why non-continuous (constructive) maths is also known as intuitionistic maths. For anyone who's not familiar with why constructive mathematics is non-continuous, it's because without the law of the excluded middle, only the computable real numbers (and analogues) exist, not the whole real number line that's present in classical mathematics.

The Banach–Tarski paradox is an example of an unintuitive result of the LEM, a paradox that doesn't exist in constructive mathematics.

View on HN

I'm sorry, but classical mathematics is perfectly able to handle continuous functions. And in fact it does so more easily. Which is why most of the important theorems were proven classically first.

Sure, Errett Bishop came along with https://www.amazon.com/Foundations-Constructive-Analysis-Err... and fixed that. But it is harder. And sure, as soon as you start looking at error bounds in numerical analysis, the classical shortcuts start to take work. But it is simply wrong to assert that the continuous REQUIRES the law of the excluded middle.

In fact every mathematician has been through the classical treatments of continuity in courses on real analysis and topology. Very few can say much that is sensible about constructivism.

The current state of the metatheory of Banach tarski is that it follows from the ZF + Ultrafilter, but not ZF + dependent choice, and has very little to do with the excluded middle.

It's common to say that constructive mathematics is continuous, as it cannot prove the existence of a discontinuous function. One can certainly reason constructively about the various things traditionally considered continuous mathematics. I find your opposite perspective on it a bit odd.

I wouldn't say that it cannot prove the existence of a discontinuous function. Rather it can prove that a point of discontinuity makes it not a function.

Can't you define a discontinuous function over some other set besides the reals, such as the set of all computable numbers? For instance, a step function is discontinuous at a single point. You can also define a function that's discontinuous at every point, such as the indicator function of the rationals.

I don't have any experience with constructive set theory, so maybe I'm missing something.

Reply on news.ycombinator.com