[FOM] Gentzen and finitism

[William Tait]

On Feb 3, 2010, at 1:14 PM, Harvey Friedman wrote:

> [Grntzen's Hauptsatz] 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,

Could you give a reference or some details?

Let
Exp_0- =  exponentiation
Exp_{n+1}x0  = 1, Exp_{n+1}x(y+1) = Exp_n(Exp_{n+1}xy)y

I assume that Exp_1 is your superexponention.  Does your result generalize: If we add Exp_k for all k<n, can we derive recursion on omega^n?

Bill