What does "can almost be proven in PA" mean regarding Theorem 2 of Timothy Chow's expository article, "The Consistency of Arithmetic"?

Question

In his expository article, "The Consistency of Arithmetic" (MSN), Prof. Chow has the following theorems:

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.

Answer 1

I believe you're overthinking what Chow means by "almost provable." We have an arithmetic statement of the form $$(*)\quad\forall x\varphi(x),$$ which while not provable in PA has the property that for each individual natural number $n$ the instance $$(*)_n\quad\varphi(\underline{n})$$ is provable in PA (where "$\underline{n}$" is the numeral corresponding to the natural number $n$). I believe this is what "almost provable" means in this context; perhaps "locally provable" or "instancewise provable" would be better terms, but I think that's all there is to this.

Note that we also have the same phenomenon with respect to consistency: for each natural number $n$, PA proves "there is no PA-proof of "$0=1$" of length $<n$." So PA almost proves Con(PA).

---

You also ask some questions about infinitary content and interpreting ordinals. Here I don't really understand what you're getting at, unfortunately (and this might be the cause of the downvote - I find the entire paragraph beginning "Interesting so far" to be quite confusing, and I'm not at all sure that there's a real mathematical question here).

That said, let me make a couple comments:

• When you ask "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,"" I think you're misreading Chow - earlier in that answer (in the paragraph beginning "finally") he is careful to say that by "ordinal" he means "ordinal smaller than $\epsilon_0$." So his statement that ordinals can be represented as [stuff] isn't meant to apply to $\epsilon_0$, since the term "ordinal" is being used there in a restrictive context.

• As to "infinitary content," I think this part of the question boils down to a confusion around what that means - different authors use the term in different ways. The simplest way to approach this is to identify finitary mathematics with some specific theory - say, PA - and then by fiat everything not provable in this theory is infinitary. You don't seem to adopt this interpretation, per your comment "it must, in some sense, be 'infinitary', that is, its proof must somehow "assume the existence of infinite sets."" Frankly I think this is reasonable, and it seems silly to me to identify finitism with a particular formal theory, but the point is that people can disagree over whether a given piece mathematics is finitary. With this in mind I think this aspect of your question isn't really mathematical, and you'll have to settle for a soft answer - namely, that in some sense when we add Theorem 2 to PA as a new axiom we "get new ordinals." (And of course this is hiding an underlying assumption - that regardless of whether we identify finitistic mathematics with a specific formal theory, we are fixing a notion of "finitistically justifiable" ordinals, namely those $<\epsilon_0$. If one holds that all ordinals $<\Gamma_0$ are "finitistically justifiable" then the above breaks down.)