[FOM] Gentzen and finitism
Sam Buss
sbuss at math.ucsd.edu
Sun Feb 7 16:56:35 EST 2010
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
More information about the FOM
mailing list