[FOM] Gentzen and finitism
williamtait at mac.com
Wed Feb 3 13:52:56 EST 2010
On Feb 2, 2010, at 5: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?
The double induction is on omega, so it is obtained by recursion on omega^2, which is reducible to primitive recursion. So PRA suffices.
More information about the FOM