It would seem as though the sentence s(E) which expresses the existence of a nontrivial elementary embedding of the universe V into itselfand which can be formalized in the first order language of NBGcould 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 factswhich I am missingthat imply my questions obviously have negative answers and probably should be closed. But I'll take the chance and ask.
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 firstorder language of set theory. Kunen himself formalized his theorem as a secondorder assertion in KellyMorse set theory, but it is possible to formalize it in secondorder GödelBernays set theory. Some mathematicians (as in Kanamori's textbook The Higher Infinite) formalize the result as a scheme of firstorder 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 metamathematical 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.

$\begingroup$ Thanks for clearing up my mistaken notion about the languages in which Kunen's theorem could be formalized. I thought it could be done in NBG but did not realize that second order NBG would be required if the axiom of choice was going to be needed in the proof. When set theorists prove theorems in a second order set theory, they must use some axiomatizable subtheory of that theory since the logical axioms of second order classical logic are not recursively enumerable. $\endgroup$ – Garabed Gulbenkian Apr 15 '13 at 19:01

$\begingroup$ Anyway, if I want to bring Quine's NF into this picture (as well as the axiom of choice) it seems as if I should really be talking about "second order NF". Although such a theory must certainly exist, I never heard of anybody taking any interest in it. $\endgroup$ – Garabed Gulbenkian Apr 15 '13 at 19:12

$\begingroup$ Oh, I guess we are miscommunicating. When I mentioned "secondorder GBC," I just meant the usual GBC, which is usually viewed as a secondorder theory because it allows classes. That is, the Kunen inconsistency is indeed provable in GBC. $\endgroup$ – Joel David Hamkins Apr 15 '13 at 19:30

$\begingroup$ Is GBC the same as NBG and, if so, does the "C" stand for Cohen? $\endgroup$ – Garabed Gulbenkian Apr 16 '13 at 15:30

$\begingroup$ Yes, people write variously NBG or GBC and other things. The "C" stands for the axiom of global choice, which is taken to be part of GBC. Meanwhile, GB has no choice principle, and GB+AC has only the usual axiom of choice. $\endgroup$ – Joel David Hamkins Apr 16 '13 at 16:05