[FOM] Gentzen and finitism

[rgheck]

On 02/05/2010 10:52 PM, William Tait wrote:
> 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?
>
>    
The positive side of this is theorem V.5.17 in Hajek and Pudlak. I think 
the reverse may follow from results close to that, namely, that this is 
the most of what you need for the proof of Con(Q). So I\Delta_0 + 
Superexp |- Con(Q) (V.5.19), but I\Delta_0 + Exp does not.

> 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.
>
>    
I think that's right. Superexp is iterated exponentiation, i.e., 
superexp(3) = 2^2^2.

rh