Can $Ord$ have nontrivial second-order elementary self-embeddings?

Question

I forgot to mention originally: this was motivated by this old MSE question.

It's not hard to show in $\mathsf{ZFC}$ that there are nontrivial elementary embeddings from $(Ord; \in)$ to itself - or rather, it's not hard to write down specific formulas which $\mathsf{ZFC}$ proves define such maps. When we add common algebraic operations, things get messier but the picture seems to stay the same - e.g. the result continues to hold for $Ord$ equipped with ordinal addition, multiplication, and exponentiation in addition to $\in$. It seems like any "reasonably simple" expansion of $Ord$ has $\mathsf{ZFC}$-provable nontrivial elementary self-embeddings.

I'm interested in a particular precisiation of this intuition. Specifically, the following seems very close to the Kunen inconsistency but I can't quite get it there:

Is it consistent that there is a nontrivial second-order elementary self-embedding $f:(Ord;\in)\rightarrow (Ord;\in)$?

Note that the second-order quantifiers in this case range over subclasses of $Ord$ or its finite Cartesian powers, not just subsets (= bounded subclasses). So we really have to ask this within an appropriate class theory. Given that that may be a bit annoying to consider, here's a "set-ified" version of that question:

Is it consistent with $\mathsf{ZFC}$ that there is an inaccessible $\kappa$ and a second-order nontrivial elementary embedding $f:(\kappa;\in)\rightarrow(\kappa;\in)$?

(Here correspondingly the second-order quantifiers range over the $\mathcal{P}(\kappa^{n})$s for $n\in\omega$ as appropriate, so everything is nicely captured by $V_{\kappa+2}$: $f$ itself, or an equivalent coding thereof, lives in $V_{\kappa+1}$, the evaluation of each second-order formula over $V_{\kappa}$ is determined by $V_{\kappa+1}$, and $V_{\kappa+2}$ can express "is a second-order elementary embedding" directly.)

The difficulty I run into in getting a negative answer here by invoking the Kunen inconsistency is that even using second-order logic there doesn't seem to be a way to code $V$ into $Ord$ (or $V_\kappa$ into $\kappa$). Of course if $V$ is "sufficiently canonical" we can do this, e.g. the existence of such an $f$ (or such a $\kappa$ and $f$) clearly contradicts $\mathsf{V=L}$, but I don't see an argument for the general case.

Answer 1

Answering this question would either require refuting choiceless large cardinals or getting close to refuting Woodin's HOD Conjecture.

First, if choiceless cardinals are consistent, one cannot rule out the existence of a second-order elementary embedding. Corollary 4.8 in Usuba's "A note on Lowenheim-Skolem cardinals" states that if there is a proper class of Lowenheim-Skolem cardinals, one can force the Axiom of Choice by a homogeneous definable class forcing. (He doesn't say homogeneous, but it will be.) Therefore assume there is a $j : V\to V$ and there is a proper class of Lowenheim-Skolem cardinals. Let $\mathbb P$ be Usuba's forcing, and let $G\subseteq \mathbb P$ be a generic filter. Then $j\restriction \text{Ord}$ is second-order elementary in $V[G]$: if $\varphi(\vec v)$ is a second-order formula and $V[G]\vDash \varphi(\vec \alpha)$, then by homogeneity, $1_\mathbb P\Vdash \varphi(\vec \alpha)$, and so by the definability of $\mathbb P$ and the elementarity of $j$, $1_\mathbb P\Vdash \varphi(j(\vec\alpha))$, and hence $V[G]\vDash \varphi(j(\vec\alpha))$.

Second, assuming the HOD Conjecture and the existence of an extendible cardinal, one can rule out the existence of a nontrivial second-order elementary embedding of the ordinals. This follows from Theorem 3.47 of Woodin's paper "In search of Ultimate L." The reason is that any second-order elementary embedding $j : \text{Ord}\to\text{Ord}$ extends to an elementary embedding from the structure $(\text{HOD},T)$ to $(\text{HOD},T)$ where $T$ is the $\Sigma_2$ theory of $V$ with ordinal parameters. It is a prominent open question whether such an elementary embedding can ever exist. It is also open whether there can be an elementary embedding from $\text{HOD}$ to $\text{HOD}$ in the context of the HOD Conjecture.

So if strong choiceless large cardinals are consistent, so is a second-order embedding, while if the HOD Conjecture is true, second-order embeddings are ruled out by more compelling large cardinal axioms. The question is therefore just one aspect of one of the most important questions in set theory/large cardinals: to what extent can arbitrary sets be approximated by ordinal definable ones?