In his expository article, "The Consistency of Arithmetic""The Consistency of Arithmetic" (MSN), Prof. Chow has the following theorems:
Theorem 1. If $a_1$, $a_2$, $a_3$,...$a_1, a_2, a_3,\dotsc$ is a sequence of ordinals and $a_i$ $\ge$ $a_j$$a_i \ge a_j$ whenever $i$ $\lt$ $j$$i \lt j$, then the sequence stabilizes; i.e., there exists $i_0$ $\ge$ 1$i_0 \ge 1$ such that $a_i$ = $a_0$$a_i = a_0$ for all $i$ $\ge$ $i_0$$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)$$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$PA and its relation to Theorem 1 as found in his answerhis answer to IamMeeoh's mathoverflowIamMeeoh's MathOverflow question, "Understanding the countable ordinals up to $\epsilon_0$"Understanding the countable ordinals up to $\epsilon_0$" (56062).
I find that after understanding this proof [of Theorem 1--my1—my comment], the hard thing to wrap my head around is how it can possibly be true that $PA$PA does not prove that there is no infinite descending sequence. My current gut feeling is that $PA$ asPA is weirdly weak, because it cannot even formalize a proof as simple as this one.
...In … In fact, Theorem 2 can almost be proved in $PA$PA. [Note that, in footnote 7 on pg. 26, he writes that $PRA$PRA + Theorem 2 implies that $PA$PA is consistent--myconsistent—my comment.]
How does Prof. Chow justify this? Consider the following, again formfrom pg. 26 of his expository article:
First, we can formulate a theorem--calltheorem—call it $Theorem 1^{'}$--thatTheorem 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 25—my comment]. Then we can mimic the proof of Theorem 1 to construct a $PA$PA proof of Theorem $1^{'}$1′ for $\phi$. The only catch is that we need, as building blocks, P$A $PA proofs of Theorem $1^{'}$1′ for formulas smaller that $H$--but—but we can assume by induction that these are available. Note that this is an inductive procedure for constructing $PA$PA proofs of individual instances of Theorem $1^{'}$1′ and cannot be converted to a $PA$PA proof of Theorem $1^{'}$1′ itself; however, it illustrates that each instance of Theorem $1^{'}$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^{'}$1′ is "intermediate in strength between Theorem 1 and Theorem 2, does the ordering of "strength" in this case refer tomean that (say) Theorem 1 is 'more infinitary' than Theorem $1^{'}$1′ (because "each instance of Theorem $1^{'}$1′ can be proved without assuming the existence of infinite sets"), and Theorem $1^{'}$1′ is 'more infinitary' than Theorem 2 (but then that is exactly the question I asked in the title--sincetitle—since "Theorem 2 can almost be proved in $PA$"PA" it must, in some sense, be 'infinitary', that is, its proof must somehow "assume the existence of infinite sets"--butsets"—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--myquestion—my comment])?
Finally, it might behoove the reader of this question to read Maria HameenHämeen-Antila'sAnttila's paper, Nominalistic Ordinals, Recursion on Higher Types, and FinitismNominalistic 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^{'}$1′, and 2 (and a possible finitary interpretation of Theorems 1, $1^{'}$1′, and 2).
