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?
Best Answer
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.