6 ms·

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

More mathematicians need to know about constructive mathematics https://en.m.wikipedia.org/wiki/Constructivism_(mathematics) https://en.m.wikipedia.org/wiki/Constructivism_(mathematics) Basically, proof by contradiction is not a good idea.

Yajirobe 8y ago
Also, lets throw out the law of excluded middle and axiom of choice!
- adamnemecek 8y ago
  No, let’s replace law of excluded middle with axiom of adversarial choice.
- JadeNB 8y ago
  > 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.
  - stan_rogers 8y ago
    That is the mechanism by which junk drawers and attics are filled.
archgoon 8y ago
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?
- adamnemecek 8y ago
  That most math books I read don’t discuss it.
  - AnimalMuppet 8y ago
    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.
    - llamaz 8y ago
      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.
      - AnimalMuppet 8y ago
        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.
        llamaz 8y ago
        Ah okay :) I misread you
Ivoirians 8y ago
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.
- bodas 8y ago
  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 :)
  - llamaz 8y ago
    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).
- danharaj 8y ago
  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.
contravariant 8y ago
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.
- JadeNB 8y ago
  > 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.)
JadeNB 8y ago
> More mathematicians need to know about constructive mathematics https://en.m.wikipedia.org/wiki/Constructivism_(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?
AnimalMuppet 8y ago
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?
- monochromatic 8y ago
  No. Constructivism is strictly weaker.
  - danharaj 8y ago
    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.
    - monochromatic 8y ago
      I haven’t heard this. What do you mean by “a similar theorem that is classically equivalent”?
      - danharaj 8y ago
        https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation
    - AnimalMuppet 8y ago
      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.
scott_s 8y ago
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?
- deleted 8y ago
  [deleted]
- waluigi 8y ago
  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.
ur-whale 8y ago
While constructive mathematics is an interesting restriction to work within, it has precious little to do with the OP.

Yajirobe 8y ago

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

adamnemecek 8y ago
No, let’s replace law of excluded middle with axiom of adversarial choice.
JadeNB 8y ago
> 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.
- stan_rogers 8y ago
  That is the mechanism by which junk drawers and attics are filled.

archgoon 8y ago

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?

adamnemecek 8y ago
That most math books I read don’t discuss it.
- AnimalMuppet 8y ago
  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.
  - llamaz 8y ago
    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.
    - AnimalMuppet 8y ago
      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.
      - llamaz 8y ago
        Ah okay :) I misread you

Ivoirians 8y ago

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.

bodas 8y ago
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 :)
- llamaz 8y ago
  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).
danharaj 8y ago
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.

contravariant 8y ago

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.

JadeNB 8y ago
> 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.)

JadeNB 8y ago

> More mathematicians need to know about constructive mathematics https://en.m.wikipedia.org/wiki/Constructivism_(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?

AnimalMuppet 8y ago

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?

monochromatic 8y ago
No. Constructivism is strictly weaker.
- danharaj 8y ago
  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.
  - monochromatic 8y ago
    I haven’t heard this. What do you mean by “a similar theorem that is classically equivalent”?
    - danharaj 8y ago
      https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation
  - AnimalMuppet 8y ago
    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.

scott_s 8y ago

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?

deleted 8y ago
[deleted]
waluigi 8y ago
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.

ur-whale 8y ago

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