Nontrivial upper bounds on proof-theoretic ordinals of strong theories: do we have any?

Question

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.

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.