I've always been interested in having a good understanding of Gentzen's proof of the consistency of arithmetic.

Being more precise, he showed that $PRA + WF(\epsilon_0) \vdash Con(PA)$.

I am interested in an exposition of his work that

1) Is transparent on which parts of the consistency proof uses the well-foundness of $\epsilon_0$.

2) Discuss (in mathematical and philosphical way) to what extent this proof deviate from the original Hilbert's Program, and in what extent it fits in a nice way to a more flexible formulation of this programme.

I should also add:

0) Is technically as simple as possible.

Item 0) is because I think this question might be of interest to the curious general mathematician.


1 Answer 1


Pohlers's 1989 book 'Proof Theory, An Introduction' gives a very clean, streamlined approach (based on work by Tait.)

Takeuti's presentation in his 'Proof Theory' is closer to Gentzen's original proof, but is much less readable than Pohlers.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.