Hacker News Reader

Comment by Ivoirians | Hacker News Reader

Mathematicians know about constructivism, they just tend to rightfully reject statements like "proof by contradiction is not a good idea" as crackpottery. Mathematics will continue to be done, constructivists and finitists be damned.

View on HN

There are settings where LEM is inadmissible. A lot of important mathematics comes from importing some theory into another, e.g. the theory of topological groups. Knowing in fine detail what principles a proof relies on let's you know whether a theorem carries through for free or not.

It might fail if it absolutely must rely on LEM, but a weaker doubly negated version will still work. This might be a deep, important fact in some setting or another.

If anyone thinks constructivism is crackpottery, then they're just ignorant and it's only incidental if it hasn't impoverished their toolkit.

I'll admit that calling all constructivists crackpots is unfair, as there are legitimate mathematicians studying homotopy type theory and whatnot that goes way over my head. What I refer to as crackpottery is people who argue that a random proof by contradiction is invalid or who reject things like Cantor's diagonalization argument with no justification besides their personal "intuition" or "philosophy" that math should be constructivist. And I think the latter group vastly outnumbers the former, at least on random internet forums. But I'll apologize if I offend any of those mathematicians with my flippant generalizations.

I'll not take offense, nor will I spout off about metaphysics here, but I can't let it pass without noting that Cantor's diagonal argument is in fact constructively valid --- given a function from a set S to its power set 2^S, Cantor constructs an element of 2^S which can't be in the image of f. The subtlety here is that there are statements equivalent to Cantor's theorem in classical settings that are not intuitionistically valid, for instance that there's no injection from 2^S -> S.

Ah, you're right, thanks for the insight.

Constructive mathematics and non-constructive mathematics are both valuable. Rejecting the latter is crackpottery.

> Constructive mathematics and non-constructive mathematics are both valuable. Rejecting the latter is crackpottery.

As Andrej Bauer likes to point out—see, for example, Section 3.1 on p. 486 of http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-... —non-constructive mathematics is a special case of mathematics (in essentially the same way that untyped = unityped programming is a special case of typed programming).

Thank you--I think I'll start saying this in the future instead. #NotAllConstructivists, I suppose.

Finitism sounds like a good idea actually because Mathematicians have a terribly bad habit of playing with infinity when they could be doing real work :)

The problem is that "youtube mathematics" focuses on Hilbert's hotel and Aleph Nought, while actual mathematics as it's taught in unversities barely mention these issues.

Infinity simplifies mathematics _a lot_ in proving things from the basics of calculus (i.e. analysis).

Reply on news.ycombinator.com