Return to Answer

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 soundness of PA 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.

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.

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 system PA + Con(PA) is strong enough to prove 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.

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 soundness of PA 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.

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 system PA + Con(PA) is strong enough to prove 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$. 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.

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 system PA + Con(PA) is strong enough to prove 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.