Ordinal analysis is typically described as characterizing recursive ordinals in a theory $T$, but there is a sense in which it can characterize all $T$-ordinals, even those that are nonrecursive.
Specifically, in such ordinal analysis, we want a canonical
- recursive set of terms
- recursive well-ordering '$≺$' of terms
- assignment formula $φ$ converting terms into ordinals
such that
- T proves that $φ$ acts as a partial order-preserving function
- for every term $t$, $T$ proves that $φ(t)$ exists
- $T + ∀α∈\mathrm{Ord} \, ∃t \, α=φ(t)$ is $Π^1_1$ conservative over $T$. ($\mathrm{Ord}$ is the class of all ordinals.)
Question: What is the strongest natural theory for which such an analysis (with proof) has been carried out? If no one has done this type of analysis, then a (canonical) example (with proof) of such a system for $Π^1_1$-CA0 (or stronger) would work as an answer.
Note: We also want other things from ordinal analysis, as described in "Goals of Ordinal Analysis" section in my paper Ordinal Notation, but the above will do here.
At first, the conditions seem impossible — strong theories such as NBG include existence of many infinite cardinals. However, the conditions deal not with what exists, but what is provable, and proofs are recursive. Modulo canonicity (which, however, is the whole point of ordinal analysis), the construction can be carried out for NBG and many other typical sound finitely-axiomatizable theories. (For theories such as Z2 and ZFC having certain infinite reflection schemas, one would need to pass to a conservative extension to get enough expressiveness for $φ$.) One existence proof (assuming $Π^1_1$ soundness of NBG) uses '≺' that consistently with NBG embeds the rationals ℚ, together with consistency of an appropriate definable surjection (not a class) $\mathbb{N}→\mathrm{Ord}$, and encodes nonrecursive ordinals by nonstandard numbers.
Of course, what we also want is for every canonically definable (in $T$) ordinal (recursive or not) to be encoded by a (standard) term. We do not have that yet for NBG + V=L (or for that matter, a definition of 'canonical'), but we can(?) do this for $Π^1_1$-CA0. Typical ordinal notation systems for $Π^1_1$-CA0 using admissible ordinals and collapsing functions should work if properly formulated. Alternatively, choose a reasonable ordinal notation system $A$ corresponding to the proof ordinal of $Π^1_1$-CA0 that can be built above an arbitrary ordinal. Working in $Π^1_1$-CA0, let $\mathrm{wfp}(A(α))$ be the well-founded part of $A$ built above $α$. Ordinals below $ω_1^{\mathrm{CK}}$ will be denoted using $\mathrm{wfp}(A(0))$, and ordinals between $ω_i^{\mathrm{CK}}$ and $ω_{i+1}^{\mathrm{CK}}$ using $\mathrm{wfp}(A(ω_i^{\mathrm{CK}}))$ and the notations for ordinals used that are $ < ω_i^{\mathrm{CK}}$. However, this analysis is informal; I do not have a proof of the $Π^1_1$ conservation above.
