Non-Standard Models of Arithmetic 10

Prev TOC Next

JB: So, last time you sketched the proof of the Paris–Harrington theorem. Your description is packed with interesting ideas, which will take me a long time to absorb. Someday I should ask some questions about them. But for now I’d like to revert to an earlier theme: how questions about the universe of sets cast their shadows down on the world of Peano arithmetic.

It seems a certain class of logical principles let us construct fast-growing functions : functions that grow faster than any function we could construct without assuming these principles. And these logical principles are also connected to large countable ordinals. For example, there’s a simple theory of arithmetic called PRA, for ‘primitive recursive arithmetic’, that’s only powerful enough to define primitive recursive functions. There are various tricks for coding up countable ordinals as natural numbers and defining the operations of ordinal arithmetic using these code numbers, but PRA is only strong enough to do this up to So, we say it has proof-theoretic ordinal Corresponding to this limitation (in some way I don’t fully understand, but can intuit), there are functions that grow too fast to be described by PRA, like the Ackermann function.

There’s a whole hierarchy of more powerful theories of arithmetic with larger proof-theoretic ordinals, nicely listed here;

• Wikipedia, Ordinal analysis.

Presumably theories with larger proof-theoretic ordinals can define faster-growing functions. What’s the precise connection? I know that you can use countable ordinals to index fast-growing functions, via the fast-growing hierarchy, so there’s an obvious conjecture to be made here.

Anyway, the time we reach PA the proof-theoretic ordinal is ε₀. There are still functions that grow too fast for PA, like Goodstein’s function:

• Andrés Caicedo, Goodstein’s function.

What does ‘too fast for PA’ mean? I mean it’s a partial recursive function that PA can’t prove is total.

I know Goodstein’s function is somehow related to Goodstein’s theorem, and you seemed to say that’s in turn related to the Paris–Harrington theorem. So I’m wondering: is the Paris–Harrington principle provable in some theory of arithmetic that has proof-theoretic ordinal a bit bigger than ?

If so, what is this ordinal?

Here’s another way to express my puzzlement. The Paris-Harrington principle is connected to a fast-growing function. Wikipedia says:

The smallest number N that satisfies the strengthened finite Ramsey theorem is a computable function […], but grows extremely fast. In particular it is not primitive recursive, but it is also far larger than standard examples of non-primitive recursive functions such as the Ackermann function. Its growth is so large that Peano arithmetic cannot prove it is defined everywhere, although Peano arithmetic easily proves that the Ackermann function is well defined.

What ordinal indexes the growth rate of this function, via the fast-growing hierarchy?

MW: Let me first ask you about your phrasing: “Presumably theories with larger proof-theoretic ordinals can define faster-growing functions.” By “define”, do you mean, “has a formula for, and can prove that the formula defines a total function”? I’d use “define” to mean just the first clause. I’d like to keep separate what we can prove from what we can express.

JB: I was being vague, mainly because I don’t really know what I’m talking about. But okay, let’s say I meant “has a formula for, and can prove that the formula defines a total function”. That sounds like what I should have said.

MW: I think it’s also time to mention the Church-Kleene ordinal ω₁^CK, which looks down from a lofty height on all the proof-theoretic ordinals. Past ω₁^CK, it seems we don’t even have a decent way to talk about the ordinals (formally in L(PA)), let alone prove things about them. (Or so I’ve read.)

I don’t know proof theory nearly as well as model theory. That’s something I hope to remedy as this series continues. Let me say a few things I’m fairly confident about, plus some guesses.

Things can get finicky, especially low down among the ordinals—many of the different choices seem to “wash out” by the time we get to ε₀. You mention PRA, the theory of primitive recursive functions. This theory has no quantifiers! Instead, it has a function symbol for every primitive recursive function. I’d rather think about IΣ₁, which is like Peano arithmetic, except we have the induction axioms only for Σ₁ formulas. (Recall that a formula is Σ₁ if it consists of an existential quantifier in front of a formula with only bounded quantifiers.) A modeler of PA would find this an attractive theory: Σ₁ formulas are upwards absolute between end extensions.

Now, IΣ₁ and PRA both have the same proof-theoretic ordinal: ω^ω. Does this mean they’re “basically the same”? My guess is yes, at least in the sense of “mutual interpretability” (like PA and ZF¬∞). Maybe they’re even synonymous! (Or what Ketland called “definitionally equivalent”.)

But what, exactly, is the meaning of “proof-theoretic ordinal”? (Let’s stick with theories in the language of PA.) This could mean: the smallest recursive ordinal α for which the theory cannot prove the validity of transfinite induction up to α (and hence can prove it up to any β<α). (That’s the definition in the Wikipedia article on Ordinal analysis.) Or it could mean: the smallest α for which transfinite induction up to α (plus some very basic stuff) proves the consistency of the theory. (That’s the definition in Rathgen’s Art of Ordinal Analysis, a paper you’ve cited in the past. For “very basic stuff”, Rathgen chooses ERA=Elementary Recursive Arithmetic, a subsystem of PRA.) I imagine you prove the equivalence of these two definitions—whenever they are equivalent—using arguments patterned after Gentzen’s proofs for ε₀.

Then we have the various function scales: the Hardy, Wainer (aka fast-growing), and slow-growing hierarchies. You might want to say that the proof-theoretic ordinal is the smallest α for which the theory cannot prove that Hardy’s h_α is total (and hence it can prove that h_β is total for any β<α). I’ve seen that definition in various places; here’s a stack-exchange question about it.

Here’s a puzzle for you (for me too): glance at the definition of the Ackermann function. Say the two-place version. As the Wikipedia article notes, the value for A(m, n) depends values of A(m*, n*) with (m*, n*) preceding (m, n) in the lexicographic ordering—looks like a job for transfinite induction up to ω²!  Yet the Ackermann function outpaces every primitive recursive function, and as we’ve read, PRA handles induction up to any ordinal less than ω^ω!

Things are more clear-cut for ε₀. First off, Con(PA), induction up to ε₀, the Paris-Harrington principle, the generalized Goodstein theorem, a version of the Hydra theorem, and the Kanamori-McAloon principle (don’t ask) are all equivalent over PA. The Hardy and Wainer (aka fast-growing) hierarchies “catch up” to each other, so it doesn’t matter which we use to define sub-ε₀ growth rate. The Buchholz-Wainer theorem says that a function is provably recursive if and only if it appears in the Wainer (or Hardy) hierarchy somewhere before level ε₀.

So to answer your question about growth rates: the Paris-Harrington function (like the Goodstein function) belongs to level  ε₀ of the fast-growing hierarchy (also the Hardy hierarchy). OK, what about the proof-theoretic ordinal of the theory you get by adding any of these to PA? I’m not so sure. It should be the “next” proof-theoretic ordinal after ε₀, but I’m pretty sure that’s not ε₀+1: once you’ve got transfinite induction up to ε₀, it’s no sweat to push it a bit further. My first guess would be ω^ε₀, except that’s equal to ε₀! Maybe ω^ε₀+1? Maybe ε₁?

It might be fun/useful to think through these matters out loud sometime.

JB: In my readings I got the impression that the two definitions of proof-theoretic are not equivalent. I thought that the “smallest α for which transfinite induction up to α (together with some basic stuff) proves the consistency of the theory” definition was a naive one inspired by Gentzen’s proof of the consistency of PA using induction up to ε₀. I thought the “smallest α for which the theory cannot prove the validity of transfinite induction up to α” definition was the one that people actually use these days.

For example, people say that ZFC has a proof-theoretic ordinal, some countable ordinal below the Church-Kleene ordinal that’s so large nobody has figured out how to talk about it. But I’ve never seen anyone claim that you could prove the consistency of ZFC using transfinite induction up to some whopping big countable ordinal (together with some other basic stuff). If this is true I’d be very interested!

I’ll ask on mathoverflow.

MW: My impressions track yours pretty closely. Although I don’t know that any one definition has driven all others off the field. As long as there are thesis topics to assign and papers to write, people will investigate all conceivable definitions, and try to suss out how they relate.

I mentioned my favorite definition above, which coincidentally is the one Noah Schweber mentions in his answer to your mathoverflow question:

The computational proof-theoretic ordinal |T|_comp of T is the supremum of the computable ordinals α such that there is some notation n for α which T proves is well-founded.

As he points out, the “consistency” definition has some rather serious problems. Pohler’s Proof Theory says:

…it is tempting to regard the order type of the shortest primitive recursive well-ordering which is needed in a consistency proof for a theory T as characteristic for T. That this idea is malicious was later detected by Georg Kreisel…

who cooked up a way to make the “consistency” ordinal ω for any “reasonable” theory. (Noah Schweber says “pathological” and “appropriate” instead of Pohler’s “malicious” and “reasonable”. His “pathological” example is the same one that Pohler describes.)

By the way, you seem skeptical that one could prove the consistency of ZF using induction up to some countable ordinal (on top of some basic stuff). I can’t say I have an intuition on this, one way or the other. Asserting the consistency of any recursively axiomatizable theory is, after all, a purely combinatorial (i.e., syntactic) claim. Con(ZF) is but a small pale shadow, cast down into the finite realm by the magic mountain of V.

I’m mostly curious about how the computational proof-theoretic ordinals relate to the growth-rate hierarchies. Maybe we’ll revisit this when I’ve spent more time boning up on proof theory.

JB: Yes, let’s move on to Enayat! I suspect we’ll loop back to these themes at various points.

Prev TOC Next