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 i

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...