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.



Reference request on Gentzen's proof of the consistency of PA
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.


