In their paper, "Generalizations of the Kunen inconsistency", (_Annals of Pure and Applied Logic_ **163** (2012) 1872-1890, doi:[10.1016/j.apal.2012.06.001](https://doi.org/10.1016/j.apal.2012.06.001), arXiv:[1106.1951](https://arxiv.org/abs/1106.1951)), 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$ [_Corollary 34(1) is the $NGB$ version of this ( see pg. 1874)--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" ([pdf](https://www.math.uni-hamburg.de/home/khomskii/ALST/slides.pdf))) 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$?)