Consistency of non-trivial elementary embedding $j: Ord \to Ord$

Question

What is the consistency strength of the existence of an elementary embedding $j: Ord\to Ord$ from the class of ordinal to itself? For example, if there is an elementary embedding $j: V\to M$, then $j\upharpoonright Ord$ is such an embedding. So the consistency strength of such an elementary embedding is below a measurable. Similarly, if $j: L\to L$ is an elementary embedding, then $j\upharpoonright Ord$ again satisfies the requirement.

Answer 1

$Ord=(Ord;\in)$, as a (class-sized) substructure of $V$, is actually surprisingly simple: while arbitrary transitive sets, and in particular levels of the $V$- or $L$- (or related) hierarchies, can have quite intricate structure, there's very little expressive power in $Ord$ or its initial segments. For an initial taste of this, one can show (Theorem $6.21$ in Rosenstein's lovely book) that for every ordinal $\alpha$ there is some $\beta<\omega^\omega\cdot 2$ such that $(\alpha;\in)\equiv(\beta;\in)$, and that $Ord$ itself is elementarily equivalent to $(\omega^\omega\cdot 2;\in)$. Meanwhile, quick back-of-the-napkin arguments establish that the least ordinal $\alpha$ such that $L_\alpha\equiv L_\beta$ for some $\beta>\alpha$ is truly gigantic (while still being countable of course).

As it turns out, $Ord$ has so little structure that there are definitions of operations on ordinals which $\mathsf{ZFC}$, or indeed much less, outright prove yield nontrivial elementary embeddings $Ord\rightarrow Ord$. This uses the same techniques as in the proof of the theorem mentioned above: via EF-games, we show that as long as $\alpha$ is "sufficiently closed" then the map $$\beta\mapsto \begin{cases} \beta & \mbox{ if $\beta<\alpha$,}\\ \alpha+\beta & \mbox{ otherwise.} \end{cases}$$ is in fact elementary. I don't recall at the moment what the least such $\alpha$ is, though (a natural guess is $\epsilon_0$ but I think it's actually much smaller than that - $\omega^{\omega^\omega}$ seems more plausible to me). And variations on the same idea can build elementary embeddings with richer behavior (e.g. the one above is eventually the identity, but we can fix that if we want to).

---

Of course $Ord$ is often more than just a linear order. What if we consider $Ord$ with the ordinal arithmetic operations of addition, multiplication, and exponentiation? What about additionally throwing on higher Veblen functions, or the map $\omega\mapsto\omega_\alpha$, or etc.?

Now things get progressively more complicated of course (already once we throw on addition and multiplication, the theory we get is no longer decidable), but I believe for any "reasonable" additional structure on $Ord$ we still get nontrivial elementary embeddings provably in $\mathsf{ZFC}$.

At this point a general theorem to that effect would be great. I vaguely recall that one exists, either by Mostowski or Harvey Friedman, but I can't remember the details at the moment. Of course we have to use a notion of "reasonable" which is sufficiently strict to outlaw operations/relations which let us code $L$ into the ordinals, so there's some finickiness here. Perhaps for any specific set of $\mathcal{L}_{\infty,\infty}$-formulas $(\varphi_i)_{i\in I}$ each defining an operation on ordinals, there is a nontrivial elementary embedding of $(Ord; (\varphi_i)_{i\in I})$ into itself? The point is that with only set-many formulas, we're really living in some fixed $\mathcal{L}_{\kappa,\kappa}$, and at ordinals "vastly bigger than" $\kappa$ things should start to blur together.

EDIT: I still don't know what theorem I was thinking of in the previous paragraph, but in answer to a question of mine Gabe Goldberg observed that there's a very strong embedding principle which appears consistent with $\mathsf{ZFC}$, although at the extreme edge of plausibility: specifically, that there is a nontrivial second-order elementary embedding of $Ord$ into itself, that is, a nontrivial map which preserves the truth of second-order formulas. This is absolutely not what I was thinking of originally, but it's cool.