[FOM] Gentzen and finitism

[Sam Buss]

The reversals for the Hauptsatz (cut-elimination) are based on showing
superexponential lower bounds on the size of cut-free proofs.   These lower
bounds were originally found by Statman [S] and Orevkov [O].  These are
indeed based on the function Exp_1(x,y), namely a stack of exponentials of
height y.  

More references and a newly obtained sharpened lower bound on the size of
cut elimination can be found in my recent preprint online [B].

The functions Exp_k grow much faster than Exp_1, but still form only a small
fragment of PRA.

[S] R. Statman, Lower bounds on Herbrand's theorem, Proceedings of the
American Mathematical Society, 75 (1979), pp. 104-107.

[O] V. P. Orevkov, Lower bounds for lengthening of proofs after
cut-elimination, Journal of Soviet Mathematics, 20 (1982), pp. 2337-2350.
Original Russian version in Zap. Nauchn. Sem. L.O.M.I. Steklov 88 (1979)
137-162.

[B] Sharpened lower bounds for cut-elimination, preprint,
http://www.math.ucsd.edu/~sbuss/ResearchWeb/lowerbdscutElim/.  

Sam

-----Original Message-----
From: William Tait [mailto:williamtait at mac.com] 
Sent: Friday, February 05, 2010 7:52 PM
To: Foundations of Mathematics
Cc: William Tait
Subject: Re: [FOM] Gentzen and finitism


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