What well-orders are definable over $V$? Let $V$ be a (the) universe of sets, and $On^V$ denote the ordinals of $V$.
It is well known that there are formulae that seem to define orderings `longer than' $On^V$. For example:
$\alpha < \beta$ iff either:
(a) $\alpha$ is a limit ordinal and $\beta$ is a successor ordinal. 
(b) $\alpha$ and $\beta$ are both limits and $\alpha < \beta$.
(c) $\alpha$ and $\beta$ are both successors and $\alpha < \beta$.
Prima facie such a formula defines a (non-set-like) well-order of twice the `length' of $On^{V}$. There's more interesting definable well-orderings of this kind (the mouse ordering is a good example).
My question: Putting aside foundational worries (we can work over a $V_\kappa$ or $H_\kappa$ if people feel queasy), what is the limit on the `length' of the well-orders that can be defined this way?
My guess is that it's going to be the least non-recursive ordinal above $On^V$. So, for example, in the case of $V_\omega$, the upper bound of ordinals definable in $ZFC -$ Infinity will be $\omega_1^{ck}$. The reason for this being that one can't take the supremum of objects one doesn't have -- we're only looking at what orderings are definable over a fixed model. However, it might be lower, or I might have missed something, I'm not sure.
 A: This is perhaps surprisingly subtle. The short version is that this ordinal is at least sometimes, and I suspect always, much smaller than the relevant analogue of $\omega_1^{CK}$.

First, suppose $A$ is a countable structure in a finite language (e.g. a countable well-founded model of $\mathsf{ZFC}$). There are various ordinals associated to $A$ (sadly there's no standard notation here, so I'm making it up as I go along):

*

*$\omega_1^{CK}(A)$ is the least ordinal not Muchnik reducible to $A$; that is, the least ordinal such that there is some copy of $A$ not computing any copy of that ordinal.


*$\omega_1^{def}(A)$ is the least ordinal which is not interpretable in $A$ with parameters; that is, the least $\alpha$ for which there are no formulas $\varphi,\psi$ with parameters from $A$ such that $\varphi$ defines an equivalence relation on $A$ and $\psi$ defines a well-ordering of the $\varphi$-equivalence classes of ordertype $\alpha$. If we take $A$ to be a countable well-founded model of $\mathsf{ZFC}$, this is the ordinal you're asking about.


*$\omega_1^{ad}(A)$ is the smallest ordinal $\alpha$ such that there is a transitive set $X$ of height $\alpha$ such that $X\models\mathsf{KP+Inf}$ and there is some structure $y\in X$ which is isomorphic to $A$. (The "ad" is short for "admissible.")
These are each reasonable notions of "$A$'s version of $\omega_1^{CK}$;" the first two are pretty obviously motivated, while the third is motivated by a technical theorem of Sacks. It turns out that we always have $\omega_1^{CK}(A)=\omega_1^{ad}(A)$, basically as a consequence of Sacks' theorem, but in general $\omega_1^{def}(A)$ could be surprisingly small. In particular:

$(*)\quad$ Any "sufficiently closed" countable well-founded model $A$ of $\mathsf{ZFC}$ will have $\omega_1^{CK}(A)>\omega_1^{def}(A)$.

Indeed, I suspect that no countable well-founded model $A$ of $\mathsf{ZFC}$ has $\omega_1^{CK}(A)=\omega_1^{def}(A)$; however, I haven't been able to prove this. The stumbling block is that I haven't been able to find any plausible proxy for "sufficiently closed;" in particular the theory of $A$ itself (does $A=L^A$? does $A$ have lots of large cardinals?) doesn't seem to be relevant.

What about uncountable models of $\mathsf{ZFC}$?
Well, the definitions of $\omega_1^{def}(A)$ and $\omega_1^{ad}(A)$ lift immediately to uncountable structures, and in fact there's a snappier and easier-to-prove analogue of $(*)$ in this context:

$(**)\quad$ Suppose $A$ is a well-founded model of $\mathsf{ZFC}$ and $A^\omega\subseteq A$. Then $\omega_1^{def}(A)<\omega_1^{ad}(A)$.


*

*See this MO answer of mine for the proof. The original statement $(*)$ can then be (stated precisely and) proved by thinking a bit more carefully about the proof of $(**)$.

And we can go further: it turns out that we can also lift the definition of $\omega_1^{CK}(A)$ to uncountable structures $A$. To do this we replace Muchnik reducibility with generic Muchnik reducibility. Given two structures $A,B$ of arbitrary cardinality, we roughly say that $A$ is generically Muchnik reducible to $B$ if $A$ is Muchnik reducible to $B$ in any generic extension where $\vert A\vert+\vert B\vert\le\aleph_0$. By Shoenfield absoluteness this is a pretty well-behaved notion; in particular, if we let $\omega_1^{CK*}(-)$ be the "generic Muchnik" version of $\omega_1^{CK}(-)$, we get that $\omega_1^{CK*}(A)=\omega_1^{ad}(A)$ for every structure $A$ whatsoever. So even for uncountable models we have:

For at least some, and I suspect for all, transitive models $A$ of $\mathsf{ZFC}$ we have $\omega_1^{def}(A)<\omega_1^{CK*}(A)$.

(Meanwhile, if you're familiar with some higher recursion theory note as a caveat that the $\alpha$-recursion analogue of $\omega_1^{CK}(-)$ is actually surprisingly small in this context - see here.)
