"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?
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.)
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%9...
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.
"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)?
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".
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.
I believe it is David Hilbert you are thinking of, not Bertrand Russell. He found that Euclid's traditional 5 axioms needed to be 20. See http://en.wikipedia.org/wiki/Hilbert%27s_axioms for more.
Speaking as an almost not-amateur (finishing my PhD this year, and working on getting a faculty job), you're both right.
Logically, there's nothing wrong with proof by contradiction. As long the steps between "Assume P is true" and "therefore FALSE" are valid, you have a valid proof that "P is false".
The issue with proofs by contradiction is psychological, but it's important not to ignore such things when you are doing math. Proofs are written for people to read, and people make mistakes in reading, writing and constructing proofs. The longer and more complex a proof is, the more likely it is that there are mistakes. I can't speak for all fields, but in my field (statistics) proofs by contradiction are acceptable but not in style and constructive proofs are generally considered to be more informative.
Proof by contradiction requires a high degree of precision because the desired result is a false statement. Whereas, for example, proof by construction requires an exactly correct answer.
For example, proving a^2 + b^2 = c^2 by construction requires ending up with the exact correct answer. Ending with a^1.8 + b^2.5 = c^3 isn't good enough. You may not know where the problem in your proof is, but you know there's a problem.
Whereas with contradiction you just get something like 1 == 2, which is clearly false. So did you arrive at that because of the contradiction or a mistake in the proof? Its really impossible to know.
With that said, I must admit that contradition feels like the only way to prove NP/P -- although I'm not a theorist and don't really know the latest techniques, but just from an amateur it seems that contrapositive/construction/direct/etc allow for solutions to this problem.
Where can I find more information about this sort of thing?