"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.
btilly|15 years ago
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|15 years ago
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-defeati...
pohl|15 years ago
http://en.wikipedia.org/wiki/Constructive_mathematics
Or are you looking for more about transforming a proof into a constructive one?
sz|15 years ago