In a typically lucid and helpful page of notes for students, [A beginner’s guide to countable ordinals](https://www.dpmms.cam.ac.uk/~wtg10/ordinals.html), Tim Gowers explains how the countable ordinals can be “constructed rigorously in a way that requires more or less no knowledge of set theory”, and this is enough for many applications. He gives some illustrations but then eventually adds 



> 
> Now comes the moment to admit that my 'applications' of countable ordinals were, in a sense, a con. The application to Borel sets wasn't really solving a problem — it was just classifying the Borel sets in quite an interesting way. As for the other two results — that continuous functions on $[0,1]$ are bounded and that open games are determined — it is downright silly to use ordinals for their proofs and very easy to remove them. This is almost always true of proofs that use countable ordinals. Though there are probably several counterexamples to this assertion, I myself know of only one theorem proved with countable ordinals for which a neater ordinal-free proof has not been discovered, and even there I am convinced that it exists.
> 
> 
> 


So here's the obvious question: are there nice counterexamples to Gowers's general claim? How does this claim stand w.r.t. proof theory (where I'd have thought that ordinals kinda matter!)? More generally, what theorems (outside set theory) are there for which a proof using countable ordinals is the most illuminating/most elegant/most informative? 



What's the use of countable ordinals? (prompted by a remark of Tim Gowers)
So, we know from reverse mathematics that nearly all "bread-and-butter" theorems are, suitably encoded, provable in proof-theoretically weak subsystems of second order arithmetic. If a theorem is provable in a system whose proof theoretic ordinal is $\alpha$, then in some sense ordinals larger than $\alpha$ need not come into its proof.


Goodstein's theorem, mentioned in the comments, cannot be proven in PA, so in some way the ordinals up to $\epsilon\_0$ are "needed" in its proof. But induction up to $\epsilon\_0$ can be expressed in a very non-ordinal way: the consistency of PA + all true $\Pi\_1$ sentences implies Goodstein's theorem, so I am not sure there is any satisfying way to formulate the claim that ordinals are "needed" in its proof, in Gowers's sense of "needed" (i.e., we have to teach someone about ordinals before they have any chance of understanding any proof of the theorem).


It sure seems like you need to use ordinals to prove the Cantor-Bendixson theorem (every closed set of reals is the union of a countable set and a perfect set), and indeed the proof-theoretic ordinal needed for reverse mathing it is relatively high, namely $\Gamma\_0$. [I take this back! An ordinal-free proof is given in William's answer [here](https://math.stackexchange.com/questions/270856/cantor-bendixson-theorem-proof).] The graph minor theorem "needs" even larger ordinals, in the sense that it cannot be proven in systems whose proof-theoretic ordinal is less then (I believe) the small Veblen ordinal.


