Theorem 1. If $a_1, a_2, a_3,\dotsc$ is a sequence of ordinals and $a_i \ge a_j$ whenever $i \lt j$, then the sequence stabilizes; i.e., there exists $i_0 \ge 1$ such that $a_i = a_0$ for all $i \ge i_0$.
Theorem 2. If $M$ is a Turing machine that, given $i$ as input, outputs an ordinal $M(i)$, and $M(i) \ge M(i+1)$, then the sequence stabilizes.
Note that Theorem 2 "is a weak corollary of Theorem 1". Further note what Prof. Chow writes about PA and its relation to Theorem 1 as found in his answer to IamMeeoh's MathOverflow question, "Understanding the countable ordinals up to $\epsilon_0$" (56062).
I find that after understanding this proof [of Theorem 1—my comment], the hard thing to wrap my head around is how it can possibly be true that PA does not prove that there is no infinite descending sequence. My current gut feeling is that PA is weirdly weak, because it cannot even formalize a proof as simple as this one.
As regards Theorem 2, he writes (on pg. 22 of his expository article):
… In fact, Theorem 2 can almost be proved in PA. [Note that, in footnote 7 on pg. 26, he writes that PRA + Theorem 2 implies that PA is consistent—my comment.]
How does Prof. Chow justify this? Consider the following, again from pg. 26 of his expository article:
First, we can formulate a theorem—call it Theorem 1′—that is intermediate in strength between Theorem 1 and Theorem 2, which restricts Theorem 1 to weakly decreasing sequences of ordinals that are definable by a first-order formula $\phi$. To prove this version of the theorem, suppose we have a formula $\phi$ that defines a weakly decreasing sequence of ordinals and asserts that they all have height at least $H$ [see Prof. Chow's definition of height and his system of ordinal notations below $\epsilon_0$ on pg. 25—my comment]. Then we can mimic the proof of Theorem 1 to construct a PA proof of Theorem 1′ for $\phi$. The only catch is that we need, as building blocks, PA proofs of Theorem 1′ for formulas smaller that $H$—but we can assume by induction that these are available. Note that this is an inductive procedure for constructing PA proofs of individual instances of Theorem 1′ and cannot be converted to a PA proof of Theorem 1′ itself; however, it illustrates that each instance of Theorem 1′ can be proved without assuming the existence of infinite sets.
Interesting so far … but there are questions (for example, the question I asked in the title still to me is not answered by the quote of Prof. Chow's quoted above). Why? Well, according to Prof. Chow, Theorem 1 "presupposes the concept of an arbitrary infinite set and hence is not finitary". Since Theorem 1′ is "intermediate in strength between Theorem 1 and Theorem 2, does the ordering of "strength" in this case mean that (say) Theorem 1 is 'more infinitary' than Theorem 1′ (because "each instance of Theorem 1′ can be proved without assuming the existence of infinite sets"), and Theorem 1′ is 'more infinitary' than Theorem 2 (but then that is exactly the question I asked in the title—since "Theorem 2 can almost be proved in PA" it must, in some sense, be 'infinitary', that is, its proof must somehow "assume the existence of infinite sets"—but how? … also, given Prof. Chow's "list" notation of "ordinals below $\epsilon_0$", how can that be extended to include $\epsilon_0$ as a "special type of finite list of finite lists of finite lists of … of finite lists" [this from his answer to IamMeeoh's mathoverflow question—my comment])?
Finally, it might behoove the reader of this question to read Maria Hämeen-Anttila's paper, Nominalistic Ordinals, Recursion on Higher Types, and Finitism, Bulletin of Symbolic Logic, 25 (1): 101-124 (2019) (MSN), because it provides the historical context in which to understand Prof. Chow's expository article, his list system of notation (which would be an example of a nominalistic representation of transfinite ordinals) and his Theorems 1, 1′, and 2 (and a possible finitary interpretation of Theorems 1, 1′, and 2).
Any help in this matter would be greatly appreciated. Thanks in advance.