Gentzen's proof relies on transfinite induction up to epsilon_0, which is not a principle liable to be accepted by someone with Nelson's foundational views. A g

Gentzen's proof relies on transfinite induction up to epsilon_0, which is not a principle liable to be accepted by someone with Nelson's foundational views. A good primer on these can be found in his book Predicative Arithmetic. http://www.math.princeton.edu/~nelson/books/pa.pdf http://www.math.princeton.edu/~nelson/books/pa.pdf