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.