Motivated by Consistency of Analysis (second order arithmetic) and Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?, I have the following question:

Are there any examples of strong theories for which we have nontrivial upper bounds on the proof-theoretic ordinal, but do not know the exact value yet?

By "strong theory," I mean a theory $T$ such that for no theory $T'$ extending $T$ do we know the exact proof-theoretic ordinal of $T'$. Let me explain why I am making this restriction: the easiest way to have a nontrivial upper bound on the proof-theoretic ordinal of a theory is to have it be a subtheory of an already-analyzed theory. Such theories, however, may still have unknown proof-theoretic ordinals by virtue of being strange: e.g., I'm sure there are some fragments of $ATR_0$ which are vaguely interesting, but for which finding the proof-theoretic ordinal would require some serious new work.

This is not what I'm looking for. Basically, what I understand of the process of finding proof-theoretic ordinals is that we "work from below," and try to build up a system of notations which exhaust the $T$-provably-well-founded recursive ordinals. I'm curious if there are any techniques for "working from above," other than actually computing the proof-theoretic ordinal of some stronger theory.


1 Answer 1


I think the short answer is no, and I'm not sure there really could be: I don't think we "know" any ordinals above the ordinal of $\Pi^1_2-CA$ but below $\omega_1^{CK}$. Theoretically someone could write down a large notation for, say, $\Pi^1_3-CA$ and then discover it was too big, but in practice the hard part seems to be writing down notations that are sufficiently large. And we don't seem to have a source for those other than getting the ordinals of yet stronger theories.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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