What are the nontrivial theorems one can prove about natural numbers which need transfinite induction? By "need transfinite induction" I mean one can show that the statement is not provable in arithmetic which only allows induction up to $\omega$. In particular, are there any statements which only state a claim about natural numbers but which require the use of infinite objects in their proof? The statement should not be metamathematical in nature (proof of consistency etc) or involve any ordinals or cardinals (i.e. infinite objects). Goodstein's theorem was mentioned as one such possibility in this MO question

$\begingroup$ Friedman showed in a 1971 paper that any proof of Borel determinacy requires the axiom scheme of replacement. $\endgroup$– Benedict EastaughFeb 4, 2014 at 13:32

$\begingroup$ That periodicity of Laver's tables is unbounded is proved using largecardinal axiom en.wikipedia.org/wiki/Laver_table: it is not a transfinite induction, so it is not exactly an answer to your question, but the only known proof requires transfinite techniques. $\endgroup$– Philippe GaucherFeb 4, 2014 at 13:52

$\begingroup$ Can you say more precisely what you mean by "need transfinite induction"? How exactly do you formalize this "need"? And why do you exclude metamathematical statements, which would otherwise of course be the main source of interesting examples. $\endgroup$– Joel David HamkinsFeb 4, 2014 at 14:22
1 Answer
The Hydra Game is another nice example where ordinals are needed. More generally, ordinals and transfinite induction appear a lot in game theory, and in related subjects like automata theory.
For instance when studying thin trees (infinite trees with a countable number of branches), each thin tree can be mapped to a (countable) ordinal that describes its complexity in some sense, and proving results on thin trees can involve transfinite induction up to $\omega_1$.

$\begingroup$ See also en.wikipedia.org/wiki/Goodstein's_theorem $\endgroup$– usulFeb 6, 2014 at 5:53