There is a tension between (1) interpreting proper class talk in set theory as talk about first-order formulas and satisfaction; and (2) taking it to be an interesting and non-trivial result that there is no (non-trivial) elementary embedding from V into V and/or taking it to be an open question whether there can be such an e.e. in the absence of choice. Basically, there is a very simple proof that there can be no definable e.e. from V into V (see Suzuki (1999)). 


This tension was recently highlighted by [Hamkins, Kirmayer, and Perlmutter](http://jdh.hamkins.org/generalizationsofkuneninconsistency/) (2012) (and pointed out [here](https://mathoverflow.net/questions/123068/kunens-inconsistency-result) and [here](https://mathoverflow.net/questions/127484/a-question-about-kunens-inconsistency-theorem)). There, the resolution was to give up on (1), since accepting it "does not convey the full power of the [Kunen's] theorem" (p. 1873). But this is perhaps the only place I've seen this issue addressed. For instance, Kanamori seems to hold both (1) and (2) in The Higher Infinite: "By “class” in the ZFC context is meant definable class,... $x \in M$ is merely [a] facon de parler" (p. 33); and "[t]he following unresolved question [i.e. whether there could be an e.e. from V into V in the absence of choice] is therefore of foundational interest" (p. 324). 


**My question is:** how do other set theorists prefer to resolve this tension? 


Hamkins, J., Kirmayer, G., Perlmutter, N. (2012) ``Generalizations of the Kunen inconsistency". Annals of Pure and Applied Logic, 163, 1872–1890.


Suzuki, A. (1999) No elementary embedding from V into V is definable from parameters. Journal of Symbolic Logic 64, 1591-1594.



The Kunen inconsistency and definable classes
My perspective on this issue is that there are a variety of ways to take the claim of the Kunen inconsistency, and we needn't pick a particular one as the only right one. Rather, we gain a fuller perspective of the result by understanding the full robust context including all of the interpretations.


* Kunen proved his result in Kelly-Morse set theory, in large part in order that he could formalize what it means for a class function $j:V\to V$ to be (fully) elementary. In KM, we can prove that that there is a satisfaction class, a truth predicate for first-order truth, and with this class (which is definable) one can express the elementarity of $j$ as a single second-order assertion.
* Meanwhile, using the observation (Gaifman) that any cofinal $\Sigma\_1$-elementary embedding is $\Sigma\_n$-elementary for any meta-theoretic natural number $n$, we can formalize the result in GBC as the claim that no class $j$ is a nontrivial cofinal $\Sigma\_1$-elementary embedding. Thus, this kind of elementarity of $j$ becomes expressible as a first-order assertion about $j$.
* We don't actually need full GBC, since for example global choice is not used, but only the usual AC for sets, and so this argument can be formalized in GB+AC.
* But actually, we don't need the full second-order part of GB, but only the ability to refer to the class $j$. So we can formalize the argument in $\text{ZFC}(j)$, the theory using ZFC where the axioms of replacement is allowed to use formulas in which the class $j$ appears. (But we only insist on elementarity of $j$ in the language without $j$.) This theory is used and suffices to show, for example, that the supremum of the critical sequence $\lambda=\sup\_n\kappa\_n$ exists.
* If one intends to rule out only definable class embeddings $j$, that is, ones which are classes in the ZFC sense of being first-order definable from set parameters, then as you mentioned, there is an easy argument ruling them out, and this argument does not use AC. I do not know any set theorist, however, who takes this result as an answer to the question of whether one can prove the Kunen inconsistency in ZF. Rather, this example reveals the issues of formalization, and shows us that it may be important to take more care in our formal treatment of the result.
* Meanwhile, a purely first-order version of the Kunen inconsistency is formalizable in ZFC, with no talk of classes of any kind, as the claim that there is no nontrivial $j:V\_{\lambda+2}\to V\_{\lambda+2}$ for any $\lambda$. This version still uses AC, and it is open in ZF. It avoids the set/class issues underlying your question by noting that the Kunen inconsistency proof establishes more by restricting to $V\_{\lambda+2}$. This set version of the result implies the full result in any set theory capable of showing that a purported class $j$ must have a closure point $\lambda$.
* The wholeness axiom gets around the issue of the previous point by stating the theory ZFC + "$j:V\to V$ is nontrivial and elementary in the language with a function symbol for $j$. Elementarity is expressed by the scheme $\forall x[\varphi(x)\iff \varphi(j(x))]$.
* Various weakenings and strengthenings of the wholeness axiom are realized by making further claims about $j$, such as whether it has a critical point, whether it moves an ordinal, etc. Also, one can make claims about the extent to which $j$ may appear in the ZFC axioms. Officially, $j$ is allowed in the separation axiom but not in replacement, and so models of WA are not able to prove the supremum of the critical sequence exists.
* If one uses merely the model-theoretic concept of embedding, one would be considering $j:V\to V$ for which $x\in y\iff j(x)\in j(y)$. But now the point is that ZFC proves that there are nontrivial embeddings. For example, we can inductively define $j(y)=\{j(x)\mid x\in y\}\cup\{\{\emptyset,y\}\}$, and prove that this is a nontrivial embedding $j:V\to V$. (See my paper [Every countable model of set theory embeds into its own constructible universe](http://jdh.hamkins.org/every-model-embeds-into-own-constructible-universe/), to appear in the JML, for more information.)


I prefer to understand the Kunen inconsistency in the rich context of all these results, rather than pick just one perspective and say that that perspective is the right one.


