Hacker News Reader

Comment by danharaj | Hacker News Reader

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.

View on HN

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.

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

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

Reply on news.ycombinator.com