[FOM] Gentzen and finitism

[William Tait]

On Feb 2, 2010, at 5:32 PM, Robert Black wrote:

> Gentzen's proof of the consistency of PA requires (over PRA) induction 
> up to epsilon_0. But what about Gentzen's "Hauptsatz", i.e. the cut 
> elimination theorem for pure first-order logic? It's obviously 
> constructive, but involves a rather complicated double induction. Does 
> it go through in PRA?
> If not, PRA plus induction up to what?

The double induction is on omega, so it is obtained by recursion on omega^2, which is reducible to primitive recursion. So PRA suffices.

Bill