"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?
Where can I find more information about this sort of thing?
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.)
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...
http://en.wikipedia.org/wiki/Constructive_mathematics
Or are you looking for more about transforming a proof into a constructive one?
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
Edit: Behold...
http://en.wikipedia.org/wiki/Descriptive_set_theory