What are the difficulties involved in proving that the Kunen inconsistency holds in $NGB$

Question

or (contrariwise) that $NGB$ + "There exists a Reinhardt cardinal" is consistent?

The question is partially in the title. $NGB$ is used for the reasons stated in the Hamkins, Kirmayer, and Perlmutter paper, "Generalizations of the Kunen inconsistency", Annals of Pure and Applied Logic, 163 (2012) pp. 1873-1876 (Section 1, "A few metamathematical preliminaries").

In order that this question should not be deemed overbroad, answers must be limited in scope to specific mathematical difficulties (eg. the Erdos-Hajnal theorem used in in proving the Kunen inconsistency in $NGBC$ or $NBC$ + $Choice$ has no known proof in $NGB$ or is known not to be provable without choice--however, those who would say that the Erdos-Hajnal theorem cannot be proven without choice must show how this fact allows for a non-trivial elementary embedding $j$: $V$ $\rightarrow$ $V$ and the existence of the requisite critical point $\kappa$ in $NGB$). Those who are so inclined might make mention of Rupert McCallum's recent attempt in showing that "the existence of a non-trivial elementary embedding $j$: $V_{\lambda + 2}$ $\rightarrow$ $V_{\lambda + 2}$ for some ordinal $\lambda$...is not consistent with $ZF$" (quote from McCallum's withdrawn short preprint, The Choiceless Cardinals are Inconsistent, arXiv:1712.09768, which is discussed on Joel David Hamlin's blog — I would be especially interested in getting a nice explanation (i.e. analysis) of the gap in this argument and the relavance of the Laver paper which Gabriel Goldberg directed him to).

Though at first glance the answers to these questions might seem "primarily opinion-based", the mathoverflow community should realize the value of informed opinion and (yes) informed speculation regarding this topic, and use this question as an opportunity to provide these 'clues' (think of the proof of the 4-color theorem) to both the mathoverflow community and the mathematical community as a whole.

Answer 1

Here is the strategy behind McCallum's attempted proof that there is no nontrivial elementary embedding $j :V\to V$.

Step 1 is to cite the theorem that if a $j :V\to V$ is consistent, then a $j : V\to V$ is consistent with $V_\lambda\vDash \text{ZFC}$ where $\lambda = \sup_{n < \omega} j^n(\text{crt}(j))$. This is proved by a minor modification of Woodin's technique for forcing choice assuming a supercompact. So it suffices to show this stronger assumption is inconsistent.

Step 2 is to try to reflect the failure of AC given by Kunen's theorem into $V_\lambda$. There is a technique for reflecting certain properties of tame substructures of $V_{\lambda+2}$ to cardinals below $V_\lambda$. This is called inverse limit reflection, originally invented by Laver and recently vastly extended by Scott Cramer. For example, a theorem of Cramer implies that in this situation, and assuming DC, there is some $\bar \lambda < \lambda$ such that there is an elementary $\pi : L(V_{\bar \lambda+1})\to L(V_{\lambda+1})$ and even a $\pi : L(V_{\bar \lambda + 1},V_{\bar \lambda + 1}^\#)\to L(V_{\lambda + 1},V_{\lambda + 1}^\#)$.

[Here is a successful application of this proof strategy. Note that $I_0$ holds at $\bar \lambda$ since $I_0$ at $\lambda$ is a first-order fact in $(V_{\lambda+1},V_{\lambda+1}^\#)$. Thus $V_\lambda$ is a model of ZFC + $I_0$. This is how I proved NBG + DC + $j :V\to V$ implies Con(ZFC + $I_0$).]

McCallum had rediscovered the inverse limit reflection technique, and he thought he could reflect the existence of an $\omega$-Jonsson cardinal into $V_\lambda$ using it. The issue, however, was that the statement that $\lambda$ is $\omega$-Jonsson is a fact about $V_{\lambda+2}$, and inverse limit reflection does not seem to be able to reflect statements about the whole structure $V_{\lambda+2}$ into $V_\lambda$. One can only reflect properties of canonical inner models over $V_{\lambda+1}$, like $L(V_{\lambda+1})$ and $L(V_{\lambda+1},V_{\lambda+1}^\#)$.

So maybe the obstruction to carrying out this proof idea is, very vaguely, that one must first extend inverse limit reflection / inner model theory to "reach" $V_{\lambda+2}$.