In their paper, "Generalizations of the Kunen inconsistency", (_Annals of Pure and Applied Logic_ 163 (2012) 1872-1890), Hamkins, Kirmayer, and Perlmutter write the following (pg. 1888--I quote Theorem 32, Corollary 34(1), and their commentary on the proofs of the theorem and the corollary preceding Theorem 32):

>Theorem 32.  Assume only $ZF$ [$NGB$--my comment] There is no nontrivial elementary embedding $j$:  $V$ $\rightarrow$ $V$ that is definable from parameters.
>
>Corollary 34.  Do not assume $AC$.  For any transitive class $M$, there is no nontrivial elementary embedding $j$:  $M$ $\rightarrow$ $V$, with a critical point, that is definable from parameters in $V$.
>
>The essence of the proof is the classical observation that the concept of being a Reinhardt cardinal, if consistent, cannot be first order expressible, since if $\kappa$ is the least Reinhardt cardinal, witnessed by $j$: $V$ $\rightarrow$ $V$, then by elementarity $j$($\kappa$) would also be the least Reinhardt cardinal, contrary to $\kappa$ $\lt$ $j$($\kappa$).  Indeed, for the same reason, there can be no consistent first-order property $\varphi$($\kappa$) implying that that $\kappa$ is Reinhardt?

also this, from the paragraph below the proof of Theorem 32:

>The proof of Theorem 32 worked by observing that if $j$: $V$ $\rightarrow$ $V$ is definable in $V$, even with parameters, then the concept of being Reinhardt with respect to that definition for some parameter is first order expressible [this seems to imply that there are two tiers of functions in $NGB$--one tier for sets and one tier for proper classes (following Bernays' two separate membership relations-- $\in_{set}$ for sets and $\in_{class}$ for classes?)--my comment].


Question:  What is the second-order formula that expresses for some cardinal $\kappa$, that "$\kappa$ is a Reinhardt cardinal", and is that second-order formula expressible in $NBG$? 


Finally (just to note), I am using the Hamkins, Kirmayer, Prelmutter understanding of $NGB$ ( i.e., $NGB$ without Choice or Global Choice).  Others, (such as Yurii Khomskii, in his slide presentation, "Alternative set theories"--look under title on the Web) hold that Global Choice is a class axiom of $NGB$ (on the other hand, Khomskii holds that Replacement is a set axiom- does that mean that Replacement does not hold for proper classes in $NGB$?)