[FOM] Gentzen and finitism

Robert Black mongre at gmx.de
Tue Feb 2 18:32:21 EST 2010

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?

Robert Black

More information about the FOM mailing list