[FOM] Gentzen and finitism
friedman at math.ohio-state.edu
Wed Feb 3 14:14:41 EST 2010
It 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.
On Feb 2, 2010, at 6:32 PM, Robert Black wrote:
Gentzen's proof of the consistency of PA requires (over PRA) induction
up to epsilon_0. But what about Gentzen's "Hauptsatz", i.e. the cut
elimination theorem for pure first-order logic? It's obviously
constructive, but involves a rather complicated double induction. Does
it go through in PRA?
If not, PRA plus induction up to what?
More information about the FOM