Given a theory $T$, for arbitrary formulas $φ$ and $ψ$ that provably in $T$ denote an ordinal, set $[φ]_T < [ψ]_T$ iff provably in $T$, the ordinal denoted by $φ$ is less than the ordinal denoted by $ψ$.
The result is a strict partial order on formulas. It is well-founded for $T$ with a transitive model, and is $Σ^0_1$ for c.e. $T$.
Let $\mathrm{ord}([φ]_T)$ denote the rank of $[φ]_T$, $\mathrm{ord}([φ]_T) =\sup(\mathrm{ord}([ψ]_T)+1:[ψ]_T<[φ]_T)$.
Questions:
* Have this ordering and the resulting ordinals been studied in detail in literature?
* What are the values of $\mathrm{ord}([ω_n^\mathrm{CK}]_{Π^1_1-\mathrm{CA}_0})$?
I chose $Π^1_1-\mathrm{CA}_0$ as perhaps the easiest to analyze system that should show key properties of the partial order; using a stronger theory is also fine. ($Π^1_1-\mathrm{CA}_0$ is the subsystem of second order arithmetic containing basic axioms and $Π^1_1$ comprehension, with induction limited to sets.) Here is what I have.
Let $T$ be a c.e. theory (including basic set theory) with a transitive model, and consider formulas that provably in $T$ denote an ordinal, $T ⊢ ∀α (φ(α)⇒α∈Ord) ∧ ∃!α \, φ(α)$ ($φ$ has one free variable).
Using $\mathrm{ord}$, each formula is assigned a recursive ordinal. For example (assuming ZFC has a transitive) model, $\mathrm{ord}([ω_1]_{\mathrm{ZFC}})$ is a well-defined recursive ordinal even though $ω_1$ is uncountable. In a sense, the partial order is a universal superset of ordinal notation systems corresponding to $T$.
The above adds support to the prediction that ordinal analysis of ZFC will give a canonical assignment formula (partial function: notation→ordinal) in NBG such that NBG is consistent with every ordinal being assigned a notation (see the question Ordinal analysis and nonrecursive ordinals); and perhaps analysis of the partial order will help us get there.
Equiconsistency results using inner models and forcing typically include enough interpretability to lead to corresponding mappings of the ordinals here. For example, $\mathrm{ord}([ω_2]_{\mathrm{ZFC}}) = \mathrm{ord}([ω_2^L]_{\mathrm{ZFC}}) = \mathrm{ord}([ω_2]_{\mathrm{ZFC} + V=L}) = \mathrm{ord}([ω_1]_{\mathrm{ZFC} + ω_1^L<ω_1})$.
However, some of the values (as defined here) appear to overshoot the canonical ones (that we get from ordinal notation systems). For example, let $s$ be a fundamental sequence for the proof ordinal $s_ω$ for $T$, with $s$ provably in $T$ satisfying appropriate basic properties. For $T$ (as above) extending $Π^1_1-\mathrm{CA}_0$, $φ ≡ \min(s_n: s_{n+1} \text{ does not exist or } n=ω)$ provably in $T$ denotes a recursive ordinal, and (but not provably in $T$) $\mathrm{ord}([φ]_T) = s_ω$.
One possibility is that $\mathrm{ord}([ω_n^\mathrm{CK}]_{Π^1_1-\mathrm{CA}_0})$ corresponds to $ω_n^\mathrm{CK}$ in the canonical notation system for $Π^1_1-\mathrm{CA}_0$ plus "for every ordinal $α$, the analog of the proof ordinal of $Π^1_1-\mathrm{CA}_0$ above $α$ exists", with perhaps more complicated behavior for other theories.
