5 ms·

Proofs By Contradiction And Other Dangers

53 points by jackfoxy 16y ago

sz 16y ago
"Since is formally a for-all/there-exists ($\Pi_2$) statement of arithmetic, there is a principle that such a proof should be convertible to one without contradiction" Where can I find more information about this sort of thing?
- pohl 16y ago
  Is it Constructivism in mathematics that you would like more information about? If so, try this... http://en.wikipedia.org/wiki/Constructive_mathematics http://en.wikipedia.org/wiki/Constructive_mathematics Or are you looking for more about transforming a proof into a constructive one?
  - sz 16y ago
    I was wondering what subfield coined the label $\Pi_2$, specifically. I haven't looked much into the structure of propositions and proofs per se, and I'm curious about what can be said about it.
    - pohl 16y ago
      That is an excellent question. I've only seen capital pi used for repeated multiplication. I, too, would like to know what it means in this context. I don't know if you missed it, but the author links to a PDF that mentions this notation in the abstract. I haven't had a chance to digest it, though: http://www.cs.cmu.edu/~crary/819-f09/Murthy91.pdf http://www.cs.cmu.edu/~crary/819-f09/Murthy91.pdf Edit: Behold... http://en.wikipedia.org/wiki/Descriptive_set_theory http://en.wikipedia.org/wiki/Descriptive_set_theory http://en.wikipedia.org/wiki/Arithmetical_hierarchy http://en.wikipedia.org/wiki/Arithmetical_hierarchy http://en.wikipedia.org/wiki/Analytical_hierarchy http://en.wikipedia.org/wiki/Analytical_hierarchy
- btilly 16y ago
  All simple proofs which have contradiction at their center can be rewritten using the contrapositive. The contrapositive is the statement that A implies B is the same as not B implies not A. (The equivalence can be seen from the fact that both statements are equivalent to saying that you cannot have A and not B true at the same time.) For a formal version you can search for Gödel's 1933 proof that intuitionistic and classical logic are equiconsistent. Meaning that a contradiction in one would have to be a contradiction in another. Half of this is easy. Every proof in intuitionistic logic is a proof in classical logic. So a contradiction in intuitionistic logic is a contradiction in classical logic. The reverse is much harder. For this he created a procedure that can take any proof in classical logic (where proof by contradiction is allowed) and convert it into a proof in intuitionistic logic (where proof by contradiction is not allowed). In the conversion the statement being proven may change (classical logic and intuitionistic logic very much do not prove the same statements). The interesting thing about the procedure is that the converted proof is a proof in classical logic, of the exact same statement that the original proof proved. But it doesn't use contradiction. That procedure is the source of the principle that is mentioned. (Incidentally this proof is a large part of why constructivism came to be abandoned. A major argument for constructivism was that being careful in your reasoning might avoid potential paradoxes around infinity. Gödel's proof showed that all of the extra effort gave no such reward.)
- primodemus 16y ago
  Regarding the principle that a forall exists statement of arithmetic can be translated to one without contradiction, the paper linked right next to your quote is basically a procedure to extract computational evidence from a clasical proof, using a translation based on the kolmogorov interpretation: http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%9... Terry Tao has a nice article comparing common proofs by contradiction to its contrapositive versions: http://terrytao.wordpress.com/2010/10/18/the-no-self-defeating-object-argument-revisited/ http://terrytao.wordpress.com/2010/10/18/the-no-self-defeati...
joe_the_user 16y ago
"The difficulty is what if the contradiction comes not from the assumption that P=NP, but rather from some error in the proof of one of the lemmas or theorems? A problem. A serious problem. Then the proof is wrong." For a proof to be correct, every step of the proof has to be correct. I can't see this as a problem specific to proof by contradiction. I suppose long proofs are more dangerous than short proofs because long proofs have more steps that need to be taken. If someone really thought they had a P/=NP proof, it would be prudent for them to break it up into Lemmas which stood on their own and only at the end point out what they'd proved. But these considerations seem completely orthogonal to the method of proof. Am I missing something (seriously, I am only an amateur myself)?
- mjw 16y ago
  I wondered this too as an amateur. Although how about this: Normally the emergence of a contradiction in the course of a proof serves as a red flag that something's wrong. When proving by contradiction, you're operating without the safety of these warning signs as you progress through the proof. If you reach a contradiction, you have to question whether or not you got there suspiciously easily. If you're aiming for something more specific than just falsehood -- "not X", say, as in the contrapositive approach -- you might be less likely to get there incorrectly. If you reach a contradiction along the way, you don't go on to say "and I'm done since contradiction implies everything including not-P", (even though technically speaking this would be perfectly valid) instead you question where you went wrong in the proof, because this is too easy. But yes this certainly feels like more of a fuzzy psychological argument doesn't it. I don't know how (or if) you could formalise a notion of "how susceptible is this proof tactic to accidents".
  - gwern 16y ago
    If we were discussing a machine-checked proof, then this would basically not be a problem. The correctness of an accepted proof would have little to nothing to do with its length. Unfortunately, any proof about NP would be very gnarly and likely to be a mammoth task to formalize into a machine-checkable proof and so likely not done for a long time, if ever - the proof-checkers would be other human mathematicians. And humans are empirically unreliable. Invalid proofs have been accepted for years, decades, and even millennia (Bertrand Russell, IIRC, found a number of gaps and hidden assumptions in Euclid). If you were looking through a program someone written, wouldn't you assume that there will be a certain bug rate per KLOC? Wouldn't you assume there is a certain bug-I-will-not-catch-reading-through rate per KLOC? Now imagine you are looking at thousands of lines of the most fragile program ever written... From a philosophical standpoint, I am reminded of Quine's famous attack on Popperian falsificationism - when we observe that Uranus is not on the orbit Newton would predict, we could reject Newton's laws of motion, or we could postulate some additional unobserved physical fact like the existence of a seventh planet called Neptune. Our observation has only forced us to reject the consolidated theory Newton+6-planets, it doesn't tell us which of the 2 to spare. Similarly, when our potential proof finally terminates in a contradiction, all it tells us is that somewhere we went wrong; it doesn't tell us which axiom or theorem we ought to throw away as false.

53 points by jackfoxy 16y ago

sz 16y ago

"Since is formally a for-all/there-exists ($\Pi_2$) statement of arithmetic, there is a principle that such a proof should be convertible to one without contradiction" Where can I find more information about this sort of thing?

pohl 16y ago
Is it Constructivism in mathematics that you would like more information about? If so, try this... http://en.wikipedia.org/wiki/Constructive_mathematics http://en.wikipedia.org/wiki/Constructive_mathematics Or are you looking for more about transforming a proof into a constructive one?
- sz 16y ago
  I was wondering what subfield coined the label $\Pi_2$, specifically. I haven't looked much into the structure of propositions and proofs per se, and I'm curious about what can be said about it.
  - pohl 16y ago
    That is an excellent question. I've only seen capital pi used for repeated multiplication. I, too, would like to know what it means in this context. I don't know if you missed it, but the author links to a PDF that mentions this notation in the abstract. I haven't had a chance to digest it, though: http://www.cs.cmu.edu/~crary/819-f09/Murthy91.pdf http://www.cs.cmu.edu/~crary/819-f09/Murthy91.pdf Edit: Behold... http://en.wikipedia.org/wiki/Descriptive_set_theory http://en.wikipedia.org/wiki/Descriptive_set_theory http://en.wikipedia.org/wiki/Arithmetical_hierarchy http://en.wikipedia.org/wiki/Arithmetical_hierarchy http://en.wikipedia.org/wiki/Analytical_hierarchy http://en.wikipedia.org/wiki/Analytical_hierarchy
btilly 16y ago
All simple proofs which have contradiction at their center can be rewritten using the contrapositive. The contrapositive is the statement that A implies B is the same as not B implies not A. (The equivalence can be seen from the fact that both statements are equivalent to saying that you cannot have A and not B true at the same time.) For a formal version you can search for Gödel's 1933 proof that intuitionistic and classical logic are equiconsistent. Meaning that a contradiction in one would have to be a contradiction in another. Half of this is easy. Every proof in intuitionistic logic is a proof in classical logic. So a contradiction in intuitionistic logic is a contradiction in classical logic. The reverse is much harder. For this he created a procedure that can take any proof in classical logic (where proof by contradiction is allowed) and convert it into a proof in intuitionistic logic (where proof by contradiction is not allowed). In the conversion the statement being proven may change (classical logic and intuitionistic logic very much do not prove the same statements). The interesting thing about the procedure is that the converted proof is a proof in classical logic, of the exact same statement that the original proof proved. But it doesn't use contradiction. That procedure is the source of the principle that is mentioned. (Incidentally this proof is a large part of why constructivism came to be abandoned. A major argument for constructivism was that being careful in your reasoning might avoid potential paradoxes around infinity. Gödel's proof showed that all of the extra effort gave no such reward.)
primodemus 16y ago
Regarding the principle that a forall exists statement of arithmetic can be translated to one without contradiction, the paper linked right next to your quote is basically a procedure to extract computational evidence from a clasical proof, using a translation based on the kolmogorov interpretation: http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%9... Terry Tao has a nice article comparing common proofs by contradiction to its contrapositive versions: http://terrytao.wordpress.com/2010/10/18/the-no-self-defeating-object-argument-revisited/ http://terrytao.wordpress.com/2010/10/18/the-no-self-defeati...

joe_the_user 16y ago

"The difficulty is what if the contradiction comes not from the assumption that P=NP, but rather from some error in the proof of one of the lemmas or theorems? A problem. A serious problem. Then the proof is wrong." For a proof to be correct, every step of the proof has to be correct. I can't see this as a problem specific to proof by contradiction. I suppose long proofs are more dangerous than short proofs because long proofs have more steps that need to be taken. If someone really thought they had a P/=NP proof, it would be prudent for them to break it up into Lemmas which stood on their own and only at the end point out what they'd proved. But these considerations seem completely orthogonal to the method of proof. Am I missing something (seriously, I am only an amateur myself)?

mjw 16y ago
I wondered this too as an amateur. Although how about this: Normally the emergence of a contradiction in the course of a proof serves as a red flag that something's wrong. When proving by contradiction, you're operating without the safety of these warning signs as you progress through the proof. If you reach a contradiction, you have to question whether or not you got there suspiciously easily. If you're aiming for something more specific than just falsehood -- "not X", say, as in the contrapositive approach -- you might be less likely to get there incorrectly. If you reach a contradiction along the way, you don't go on to say "and I'm done since contradiction implies everything including not-P", (even though technically speaking this would be perfectly valid) instead you question where you went wrong in the proof, because this is too easy. But yes this certainly feels like more of a fuzzy psychological argument doesn't it. I don't know how (or if) you could formalise a notion of "how susceptible is this proof tactic to accidents".
- gwern 16y ago
  If we were discussing a machine-checked proof, then this would basically not be a problem. The correctness of an accepted proof would have little to nothing to do with its length. Unfortunately, any proof about NP would be very gnarly and likely to be a mammoth task to formalize into a machine-checkable proof and so likely not done for a long time, if ever - the proof-checkers would be other human mathematicians. And humans are empirically unreliable. Invalid proofs have been accepted for years, decades, and even millennia (Bertrand Russell, IIRC, found a number of gaps and hidden assumptions in Euclid). If you were looking through a program someone written, wouldn't you assume that there will be a certain bug rate per KLOC? Wouldn't you assume there is a certain bug-I-will-not-catch-reading-through rate per KLOC? Now imagine you are looking at thousands of lines of the most fragile program ever written... From a philosophical standpoint, I am reminded of Quine's famous attack on Popperian falsificationism - when we observe that Uranus is not on the orbit Newton would predict, we could reject Newton's laws of motion, or we could postulate some additional unobserved physical fact like the existence of a seventh planet called Neptune. Our observation has only forced us to reject the consolidated theory Newton+6-planets, it doesn't tell us which of the 2 to spare. Similarly, when our potential proof finally terminates in a contradiction, all it tells us is that somewhere we went wrong; it doesn't tell us which axiom or theorem we ought to throw away as false.