3
$\begingroup$

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.

Improve this question
$\endgroup$
3

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .