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.

  • $\begingroup$ @TimothyChow is a regular contributor to MO. He might read your question, I suppose. $\endgroup$
    – kodlu
    Jul 16, 2019 at 18:59
  • $\begingroup$ Why the downvote? $\endgroup$ Jul 16, 2019 at 19:20
  • 2
    $\begingroup$ Is there an actual mathematical question somewhere? “Is this thing more infinitary than that thing” certainly isn’t one. $\endgroup$ Jul 16, 2019 at 19:39
  • 3
    $\begingroup$ @ThomasBenjamin It's pretty obvious that over any reasonable base theory T1 implies T1' and T1' implies T2 - "strength" seems to be used here in the simplest possible way. I really think you're making things much more complicated than they actually are. $\endgroup$ Jul 16, 2019 at 23:36
  • 1
    $\begingroup$ @Noah Schweber: It seems that T1 implies T1' and T1' implies T2 over RCA, so the real question which theory of arithmetic is needed to go the other way round? Induction on large countable ordinals implies the existence of fast growing functions, so I would assume that every "reasonable" theory of arithmetic can only prove T1 up to a certain point. If you can prove this and find a good theory that proves T1', which should also be possible, as PA almost proves it, then you have a precise mathematical meaning of "strength". $\endgroup$ Jul 19, 2019 at 16:10

1 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.)

  • $\begingroup$ Thank you for your answer; I will take it under advisement (in general it is helpful but I have some questions about your examples). A couple of quibbles though: you attribute the view that the proof of the consistency of $PA$ is "infinitary" because "its proof must somehow assume 'assume the existence of infinite sets' " to me when in fact it is correctly attributable to Prof. Chow ("The alert reader will notice that the statement of Theorem 1 presupposes the concept of an arbitrary infinite sequence and hence it is not finitary"--this from the paragraph directly below his $\endgroup$ Jul 20, 2019 at 13:55
  • $\begingroup$ (cont.) statement of Theorem 1); second, though you are entirely correct that in his answer to IamMeeoh's (matteo's) question, Prof. Chow does state that the term "ordinal" means "ordinal below $\epsilon_0$", in a later paragraph he states, "My personal opinion is that the usual ways of defining $\epsilon_0$ make it seem mind-bogglingly infinitary, but the above definition [the list notation for ordinals below $\epsilon_0$] makes it clear that any particular ordinal [below $\epsilon_0$, presumably] is just a special type of finite list of finite lists of finite lists of ...of finite lists... $\endgroup$ Jul 20, 2019 at 14:18
  • $\begingroup$ (cont.) ...Not very infinitary at all.". Given that in an earlier paragraph he states that the list-notation for $\omega$ is "((( )))", why can there not be a finite list notation for $\epsilon_0$ (and can it be proven that there is no finite list notation for $\epsilon_0$)? $\endgroup$ Jul 20, 2019 at 14:28
  • $\begingroup$ As regards your example (since the second example seems to be a variation of the first): consider the example of an arithmetic statement $\forall$ $x$$\varphi$($x$) which is not provable in $PA$, but for each individual natural number $n$ the instance $\varphi$($n$) is provable in $PA$; since this seems an example of an $\omega$-rule, if one assumes assumes that this $\omega$-rule in a primitive recursive $\omega$-rule, though the primitive recursive $\omega$-rule cannot be proven in $PA$, is there some reason a primitive recursive $\omega$-rule cannot be deemed 'finitary'? $\endgroup$ Jul 20, 2019 at 14:46
  • $\begingroup$ [Note that 'in' in the statement "if one assumes that this $\omega$- rule in a primitive recursive $\omega$-rule" should be "is"--sorry for the typo.] $\endgroup$ Jul 20, 2019 at 14:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.