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.] 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.

Here is an example from operator theory that qualifies (at leat partially): the ABLV theorem.

A version of it reads as follows:

ABLV Theorem. Let $T$ be a bounded linear operator on a Banach space $E$ and assume that $T$ is power bounded in the sense that $\sup_{n \in \mathbb{N}} \|T^n\| < \infty$.

Suppose that the spectrum $\sigma(T)$ of $T$ intersects the complex unit circle $\mathbb{T}$ at most in a countable set, and that the dual operator $T'$ on $E'$ does not have any eigenvalues on $\mathbb{T}$. Then $T^nx \to 0$ as $n \to \infty$ for each $x \in E$.

The theorem is from 1988, and it is called ABLV theorem because it was proved independently by the following pairs of authors:

[1] Wolfgang Arendt & Charles Batty: "Tauberian Theorems and Stability of One-Parameter Semigroups", Transactions of the AMS, 1988.

[2] Yu. I. Lyubich & Vu Quôc Phóng: "Asymptotic stability of linear differential equations in Banach spaces", Studia Mathematica, 1988.

(Actually, both papers focussed on a $C_0$-semigroup version of it; see the remarks at the end of this post.)

I'll try to outline the main idea of the proof in [1] as Wolfgang Arendt once explained it to me: one needs to (a) use a Tauberian theorem for vector-valued Laplace transforms and (b) successively remove points from $\sigma(T) \cap \mathbb{T}$ by an induction procedure until the spectrum does not intersect the unit circle any longer.

The point about the second step is that, since the spectrum is closed, removing points from it can only work if these points are isolated in the spectrum - so just enumerating the countable set $\sigma(T) \cap \mathbb{T}$ and succesively removing each point doesn't do the job. Instead, one uses transfinite induction over countable ordinals:

In a non-empty compact countable set - such as $\sigma(T) \cap \mathbb{T}$ - there always exists at least one isolated point, so you can successively remove such isolated points $\omega$-many times (unless there are only finitely many spectral values, in which case the spectrum is empty after finitely many steps). Afterwards you're again left with a countable compact set, and repeat.

Remarks.

• Of course, things are actually not quite as simple as I described them (for instance, points that are isolated in $\sigma(T) \cap \mathbb{T}$ need not be isolated in $\sigma(T)$ - so here you can already see that you cannot simply "remove" them from spectrum). Still, this somehow seems to be the intuitive idea behind it.

• Arendt revisits this theorem and explicitly focusses the discussion on transfinite induction over countable sets in the following paper:

  [3] W. Arendt: "Countable Spectrum, Transfinite Induction and Stability", Operator Theory: Advances and Applications, 2015.

  In [3, Section 5] there is also a discussion of the uniqueness of trigonometric series that dates back to Cantor and that uses transfinite induction over countable sets, too. So this is another answer to the question of the OP.

• In fact, the ABLV theorem is typically stated and proved for $C_0$-semigroups rather than for single operators (for instance, [2] deals solely with the $C_0$-semigroup case). The single operator version stated above can be found in [1, Theorem 5.1].

• Why is the ABLV theorem only a partial answer? Well, there is also [2], of course - where the authors used a different technique to arrive at the same result. (By the way, in the popular $C_0$-semigroup book of Engel and Nagel, the ABLV theorem is proved by employing the technique from [2].)

I'm sure I don't quite understand this question, since my impression is that transfinite induction and ordinals are needed all the time, and often lengths are countable in practical cases.

Nevertheless, I can't resist mentioning one of my favorite results in symbolic dynamics, namely a theorem from "Structural aspects of tilings" by Ballier-Durand-Jeandel. It is one where I do not know a nice way to remove the use of countable ordinals. By basic topology, every $\mathbb{Z}^2$-subshift (closed shift-invariant subset of $A^{\mathbb{Z}^2}$ for $A$ finite set) is either finite, countably infinite or has the cardinality of the continuum. They prove an interesting result about the countable case.

Some definitions first. If $A$ is a finite set, we say $X \subset A^{\mathbb{Z}^2}$ is a subshift of finite type or SFT if there exists a clopen set $C \subset A^{\mathbb{Z}^2}$ such that $$ X = \{x \in A^{\mathbb{Z}^2} \;|\; \forall \vec v \in \mathbb{Z}^2: \sigma^{\vec v}(x) \notin C \} $$ where $\sigma^{\vec v}(x)_{\vec u} = x_{\vec v + \vec u}$ is the shift action. (It's the same as saying it's defined by finitely many forbidden patterns.) An SFT is countably infinite if it has countably infinitely many configurations. We call elements $x \in X$ configurations. A configuration $x \in X$ is singly-periodic if the point stabilizer $\{\vec v \in \mathbb{Z}^2 \;|\; \sigma^{\vec v}(x) = x\} \leq \mathbb{Z}^2$ is nontrivial but not of finite index.

Let $X \subset A^{\mathbb{Z}^2}$ be a subshift of finite type which is countably infinite. Then $X$ contains a singly-periodic configuration.

The proof is quite interesting and I'll outline it as I remember it; there's lots of steps so this may be too quick to follow, but at least one sees from the summary that you really talk about ordinals and their successor relation on top of the Cantor-Bendixson argument. You can find the details in the Ballier-Durand-Jeandel paper.

First, you define the Cantor-Bendixson derivatives $X^{(\gamma)}$ for all ordinals $\gamma$ in the usual way. Since $X$ is countable and compact you have $X^{(\gamma)} = \emptyset$ for some $\gamma$ (or you find a perfect subset contradicting countability), and since the topology is second-countable, this happens for a countable ordinal $\gamma$.

Now let us analyze $\gamma$. It must be a successor ordinal, since otherwise $\emptyset$ is an intersection of nonempty sets contradicting compactness. So $\gamma = \beta + 1$ for some $\beta$. Since $X^{(\beta)}$ has empty Cantor-Bendixson derivative, it has to be finite. But it is classical that a finite subshift is a subshift of finite type, and it is also classical that SFTs have the "compactness" property that an SFT cannot be the intersection of a strictly descending chain of subshifts (it's a "finitely-generated group cannot be a strictly increasing union of subgroups" style argument). From this we deduce that also $\beta = \alpha + 1$ must be a successor ordinal. Clearly $X^{(\alpha)}$ is countably infinite.

Next, we analyze $X^{(\alpha)}$ (there we will find our singly-periodic configurations). It is known that a $\mathbb{Z}^2$-subshift is finite if and only if every configuration in it has finite-index stabilizer, so some configuration $X^{(\alpha)}$ has infinite-index stabilizer. Let $x$ be such a configuration, and let $V \leq \mathbb{Z}^2$ be its stabilizer.

It now suffices to show that we cannot have $|V| = 1$: Suppose for a contradiction that we had. Observe that all $\sigma^{\vec v}(x)$ are distinct, so any limit point of such shifts is in $X^{(\beta)}$. Then for every $\epsilon > 0$, every shift $\sigma^{\vec v}(x)$ with $|\vec v|$ large enough is at distance at most $\epsilon$ from the SFT $X^{(\beta)}$.

Since $X^{(\beta)}$ is finite, it has finite-index pointwise stabilizer, generated by some non-collinear $\vec u_1, \vec u_2 \in \mathbb{Z}^2$. Since all limit points of $x$ have to be in $X^{(\beta)}$, we must have $x_{\vec v} = x_{\vec v + \vec u_1} = x_{\vec v + \vec u_2}$ for all $|\vec v|$ large enough (again otherwise we have infinitely many distinct shifts $\sigma^{\vec v}(x)$ and we can extract a limit point which is not fixed by $\sigma^{\vec u_1}$ and $\sigma^{\vec u_2}$, thus is not in $X^{\beta}$).

We conclude that if $x$ does not have finite-index stabilizer, then $x$ is periodic apart from a finite "period-breaker" area, and since $X$ is an SFT, it is easy to see that it is uncountable, since we can glue these period-breakers all around $x$ and we will not see a problem with the defining clopen set $C$, as such a set will only look at the local picture. (I'm being very quick here, here you perhaps need to work a bit and draw a picture, or read the paper.)

So $x$ has infinite stabilizer which is not of finite index, i.e. $x$ is singly periodic. Square.

(There are some characterizations also for the other cardinalities. A $\mathbb{Z}^2$-subshift is finite if and only if every configuration has finite-index stabilizer. In another paper called "Structuring multi-dimensional subshifts", Ballier and Jeandel also give a characterization of uncountable SFTs, but I'll skip that.)