Nachum Dershowitz has lots of work on termination proofs and many of these make use of ordinal arithmetic. In particular, if you have a computer program that moves from one state to another, and you can label each state with an ordinal, and you know that the ordinal for each new state is strictly less than the ordinal for the previous state, then the program must eventually terminate. Goodstein's Theorem is a special case, showing termination for a highly contrived sequence. But more realistic examples arise when studying termination of rewrite rules.
A basic example is proving termination of the rewrite rules that define symbolic differentiation. Like in the case of Goodstein's theorem you have the same problem that differentiation might take a step forward in decreasing the powers in a monomial, but then takes what looks like a giant step back as applying the Leibniz rule to a product can lead to many more terms. But Floyd came up with a neat labelling by ordinals resulting in a really simple termination proof. See example 8 here (among other examples and papers).
Apparently the idea for this originated with Alan Turing.