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?