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