# Definable well-ordered class relations

Suppose we a working with an axiomatic set theory such as $$\bf ZFC$$. Formulae with 2 free variables define class relations. "Small" class relations can be turned into sets of ordered pairs, the others are proper classes. Some formulae define relations that are well-orders. A "small" such relation can be turned into a well-ordered set that is order-isomorphic to some ordinal $$\alpha\in\bf Ord$$. Proper class relations also be can well-orders, e.g. a formula $$\phi(x,y)$$ saying that $$x$$ and $$y$$ are both ordinals and $$x\in y$$ defines the usual well-order on the class of ordinals $$\bf Ord$$.

Now, we can also write a formula that well-orders all ordinals except $$\bf 0$$ in the usual way, but considers $$\bf 0$$ as larger than all of them. Apparently, it gives us an order type that is "longer" than $$\bf Ord$$, and can be denoted as $$\bf Ord+\bf1$$. In a similar way, formulae having even "longer" order types such as $$\bf Ord+\bf Ord$$, etc. can be written. These order types are not sets existing in the universe, but rather, informal equivalence classes of formulae defining well-ordered class relations under (provable) order isomorphism. But, still, we can think of them as very long "ordinals" that occur when we count beyond all set-sized ordinals and even beyond the proper-class-sized "ordinal" $$\bf Ord$$. I'm interested in how far those "ordinals" can extend, and whether there is some systematic or formal way to study them, or develop ordinal arithmetic on them. Perhaps, a different axiomatic theory, rather than $$\bf ZFC$$, would be more suitable for that?

A good way in my opinion to study this phenomenon is to switch from $$V$$ to transitive set-sized models of $$\mathsf{ZFC}$$ (making appropriate existence assumptions of course). Specifically, suppose $$M$$ is a transitive model of $$\mathsf{ZFC}$$. Then we can talk unproblematically about the supremum $$S_M$$ of the order-types of $$M$$-definable well-orderings; this supremum will always be $$>\mathsf{Ord}^M$$ (which is just $$\mathsf{Ord}\cap M$$ of course) by precisely the example you give.
Especially when $$M$$ is countable (if $$M$$ is uncountable we need to perform some circumlocutions) there is a natural computability-theoretic ordinal to compare with $$S_M$$, namely the supremum $$O_M$$ of the ordinals computable from an isomorphic copy of $$M$$ with domain $$\omega$$. This $$O_M$$ "sees" that $$M$$ is countable, so on the face of things doesn't seem to be connected to $$M$$ very well at all. However, it turns out that this is a rather important thing to consider, so it's natural to compare it to $$S_M$$. We always have $$O_M\ge S_M$$, and for $$M$$ "sufficiently closed" this inequality is strict; however, equality can occur.
If we really want to talk about class relations on $$V$$ rather than "set-ifying" things, we need to look at some class theory. The standard examples are $$\mathsf{NBG}$$ (which is a conservative extension of $$\mathsf{ZFC}$$) and $$\mathsf{MK}$$ (which isn't). The latter is more appropriate for things related to class-length recursions, which suggests that it's the right framework here. There is definitely some work done on class theories and their relation to "long" ordinals; I think Joel David Hamkins has some good papers on the topic.