Hacker News Reader

Comment by adamnemecek | Hacker News Reader

More mathematicians need to know about constructive mathematics https://en.m.wikipedia.org/wiki/Constructivism_(mathematics)

Basically, proof by contradiction is not a good idea.

View on HN

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.

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

I believe most mathematicians are well aware of constructive mathematics. What makes you think that they aren't?

> Basically, proof by contradiction is not a good idea.

Based on what?

That most math books I read don’t discuss it.

Maybe you should read more widely.

And maybe you should not make generalizations based on your reading list. In particular, your reading list could be selective, thereby making generalizations worthless. Or you could misread your reading list, where they do not explicitly state that they believe in and/or depend on proof by contradiction.

Do you even study mathematics? You sound like a programmer with a passing interest in mathematics, because 99% of math books don't worry about issues like the axiom of choice or constructive math. The only ones that do are logic books.

I quit after a bachelor's in math, so yes, I have studied mathematics, but no, I don't. Still, I'm not just a programmer with a passing interest in math.

Returning to the discussion: adamnemecek said that most mathematicians needed to know about constructive mathematics. When asked why he thought they didn't, he said that most math books he read didn't discuss it (presumably, "it" = "constructivist mathematics"). So I said that adamnemecek couldn't draw that conclusion on that evidence, though I should perhaps have been clearer that, as you said, "99% of math books don't worry about issues like the axiom of choice or constructive math". You're actually agreeing with what I was trying to say - you can't look at an average math book and decide whether the author knows about constructivist math or not, because it's outside the topic of the book. Even if the book does lots of proof by contradiction, that only proves that the author is not writing a constructivist book, not that the author is unaware of constructivism.

I think adamnemecek wants every math book to be explicitly constructivist. That, I think, is a complete misreading on his part of how important constructivist math is.

Ah okay :) I misread you

To paraphrase: "if it were a good idea, my books would have discussed it." Are we done here?

> More mathematicians need to know about constructive mathematics https://en.m.wikipedia.org/wiki/Constructivism_(mathematics)

> Basically, proof by contradiction is not a good idea.

The first statement is probably morally true (though I'd argue that almost every professional mathematician knows about constructivism, so maybe you meant something more like "take constructivism seriously" than just "know about constructivism"); and I think that judgements like the second probably aren't easily made scientific, and, if unscientific, are unuseable.

That said, it also seems to be almost entirely beside the point of formalisation (except in the sense that it seems that 'naturally occurring' formal logics tend to be constructive), so … why mention it here?

Two questions:

1. Are there any mathematical truths/theorems that are provable in constructivism that is not provable in "regular" (non-constructive) mathematics?

2. Are there proofs that are easier in constructive mathematics than in non-constructive mathematics?

If the answer to both questions is "no", on what do you base your opinion of the superiority of constructivism?

No. Constructivism is strictly weaker.

Strictly weaker in a weak sense, every classically true proof can be translated into a correct constructive proof of a similar theorem that is classically equivalent. So is it weaker or is it more fine-grained? That's a philosophical question.

Can it? Here's a proof that requires the law of the excluded middle. If you don't have that, you don't have a proof of that theorem. What's the correct constructive proof of a similar theorem "that is classically equivalent"?

Or, to say it differently, aren't there things that are true in "classical" (non-constructivist) math that are not true in constructivist math? My impression was that what is provably true in classical math is a strict superset of what is provably true in constructivist math.

If you use LEM to prove A, you can translate that proof into intuitionistic logic so that it proves Not (Not A). This is classically equivalent to A, but not intuitionistically. So the real difference between the two is that intuitionistic logic makes a finer distinction between propositions that classical logic says are the same.

I haven’t heard this. What do you mean by “a similar theorem that is classically equivalent”?

https://en.wikipedia.org/wiki/Double-negation_translation

Also, lets throw out the law of excluded middle and axiom of choice!

> lets throw out the law of excluded middle

I don't think that we should throw it out, but neither do I think that we shouldn't do so.

That is the mechanism by which junk drawers and attics are filled.

No, let’s replace law of excluded middle with axiom of adversarial choice.

How does one prove the undecidability of the Halting Problem without proof by contradiction? How does one prove there is no largest integer without proof by contradiction?

Its a common misconception that proofs by contradiction are not constructive. Take the proof that √2 is irrational. What you are trying to prove is that √2 is not rational, or, constructively speaking, `√2 ∈ ℚ => ⊥`. So a proof that constructs such a function must construct a contradiction given the fact that √2 is irrational. This is both a proof by contradiction and a constructive proof. The same can be done with both of the proof you mentioned. Where you really start to run in to trouble is double negation. Evidence of ~~P comes as some function `(P -> ⊥) -> ⊥`, so there isn't really any way to create evidence of P from that. The lack of LEM really stems from this fact. If you try to run through the proof that `P v ~P => T`, you get stuck on double negation. However, it is true that `~~(P v ~P) => T`, which satisfies the gut feeling that LEM can't _not_ be true.

I wouldn't go as far as calling it a bad idea but I do consider it a style error when a a proof by contradiction is used even though a proof by contraposition would do.

> I wouldn't go as far as calling it a bad idea but I do consider it a style error when a a proof by contradiction is used even though a proof by contraposition would do.

A common style of proof among novice mathematicians, and even occasionally some professionals, is the good old: "Let's prove `P` by contradiction. Assume `not P`. Then [direct proof of `P`]. Therefore, we have a contradiction."

(I think that the fondness for this technique above all others among novices is that, no matter how hard the problem, you always at least know how to start a proof by contradiction.)

While constructive mathematics is an interesting restriction to work within, it has precious little to do with the OP.

Reply on news.ycombinator.com