Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the theorem without transfinite induction. Some time ago I came across this old usenet post where Torkel Franzen writes

Goodstein's theorem does not necessarily require transfinite induction for its proof, but it's not provable in elementary arithmetic. It can be proved by ordinary induction on a statement involving quantification over sets...

What is the proof/statement Franzen is referring to?

Inexhaustibilitybook? Sounds like this is a concrete way to see that $ACA_0$ with $\Sigma^1_1$-induction is not conservative over $PA$. – François G. Dorais♦ Jun 24 '13 at 18:26