[FOM] Gentzen and finitism
William Tait
williamtait at mac.com
Fri Feb 5 22:52:00 EST 2010
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