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