6 ms·

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 group

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.

Ivoirians 8y ago
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.
- deleted 8y ago
  [deleted]
- intuitionist 8y ago
  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.
  - Ivoirians 8y ago
    Ah, you're right, thanks for the insight.
im3w1l 8y ago
Constructive mathematics and non-constructive mathematics are both valuable. Rejecting the latter is crackpottery.
- Ivoirians 8y ago
  Thank you--I think I'll start saying this in the future instead. #NotAllConstructivists, I suppose.
- JadeNB 8y ago
  > 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-01556-4/S0273-0979-2016-01556-4.pdf 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).

Ivoirians 8y ago

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.

deleted 8y ago
[deleted]
intuitionist 8y ago
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.
- Ivoirians 8y ago
  Ah, you're right, thanks for the insight.

im3w1l 8y ago

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

Ivoirians 8y ago
Thank you--I think I'll start saying this in the future instead. #NotAllConstructivists, I suppose.
JadeNB 8y ago
> 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-01556-4/S0273-0979-2016-01556-4.pdf 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).