[FOM] Gentzen and finitism

[Harvey Friedman]

It is formalizable in SEFA = super exponential function arithmetic.  
This is Q + defining equations for +,dot,exponentiation, and  
superexponentiation, together with the induction scheme for all  
bounded formulas in the language of SEFA. This amounts to a tiny  
fragment of PRA. There are reversals showing that this is best possible.

Harvey Friedmans

On Feb 2, 2010, at 6: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?