A question about Kunen's inconsistency theorem It would seem as though the sentence s(E) which expresses the existence of a non-trivial
elementary embedding of the universe V into itself-and which can be formalized in the 
first order language of NBG-could also be formalized in the language of Quine's NF. These
two set theories would seem to share the same first order language (since NBG does not really
need separate variables and quantifiers for sets and for proper classes.) I am interested in
this question because I understand that Kunen's proof of the inconsistency of NBG+s(E) depends
upon the axiom of choice (which is taken as one of the axioms of NBG.) Now the axiom of choice
does not hold in NF (or holds at most for Cantorian classes- and V is not a Cantorian class.)
Is it possible that NF+s(E) might be consistent if NF is, and should this be the case, would
the set theory NF+s(E) be of any interest in its own right? I realize there may be some very
simple facts-which I am missing-that imply my questions obviously have negative answers
and probably should be closed. But I'll take the chance and ask.
 A: This is more of a comment than an answer, but it is too long to
fit in a comment box.
There are a number of subtle issues concerning your claim that one
may formalize the Kunen inconsistency as an assertion in the
first-order language of set theory. Kunen himself formalized his
theorem as a second-order assertion in Kelly-Morse set theory, but it is possible to formalize
it in second-order Gödel-Bernays set theory. Some mathematicians (as in
Kanamori's textbook The Higher Infinite) formalize the result as a
scheme of first-order assertions in ZFC, ruling out only definable nontrivial
elementary embeddings $j:V\to V$. But others object that this way
of stating the result is considerably weaker, since one may
actually prove it quite softly, without the axiom of choice. We
discuss all these meta-mathematical issues in our paper J.
D. Hamkins, G. Kirmayer, N.L. Perlmutter, Generalizations of the Kunen inconsistency.
When considering the Kunen inconsistency in NF, therefore, I would
want to know exactly what you take the assertion $s(E)$ to be,
especially in light of the fact that NF is particularly finicky
about the syntactic form of the assertions it treats.
Meanwhile, let me mention that there are a variety of assertions similar to the Kunen inconsistency assertion, which we do not actually know to be inconsistent.


*

*For example, ZFC proves that there is a nontrivial class function $j:V\to V$ with $x\in y\iff j(x)\in j(y)$. For example, one may recursively define $j(y)=\{j(x)\mid x\in y\}\cup\{\emptyset, y\}$.  (See my recent paper Every countable model of set theory embeds into its own constructible universe.)

*If one augments the language of set theory with a new function symbol $j$, then the theory consisting of the usual ZFC axioms (in the ordinary language of set theory), plus the assertions $\forall x[\varphi(x)\iff\varphi(j(x))]$, and nontriviality $\exists x\ j(x)\neq x$ are equiconsistent with ZFC. This is just because if ZFC is consistent, then it has models with nontrivial automorphisms. 

*Stronger versions of the previous theory lead one to the Wholeness axioms of Paul Corazza, which are known to lie just below $I_3$ in large cardinal strength. 
