The question is: if I assert in ZF that there exists a Reinhardt cardinal, do I really get a theory of higher consistency strength than when I assert in ZFC that there exists an I0 cardinal (the strongest large cardinal not known to be inconsistent with choice, as I understand)? This is implicit in the ordering of things on Cantor's Attic, for example, but I've been unable to find a proof (granted, I don't necessarily have the best nose for where to look!).

One thing that worries me is that when there *is* a ZFC analog of a ZF statement, many equivalent formulations of the ZFC statement may become inequivalent in ZFC. So we don't have much assurance that the usual definition of a Reinhardt cardinal is "correct" in the absence of choice.

I think it should be clear that Con(ZF + Reinhardt) implies Con(ZF + I0). But again, it's not clear that ZF+I0 is equiconsistent with ZFC+I0.

It's apparently not possible to formulate Reinhardt cardinals in a first-order way, so I should really talk about NBG + Reinhardt, or maybe ZF($j$) + Reinhardt, where ZF($j$) has separation and replacement for formulas involving the function symbol $j$.

**EDIT**

Since this question has attracted a bounty from Joseph Van Name, maybe it's appropriate to update it a bit. Now, I'm not actually a set theorist, but it's not even clear to me that Con(ZF + Reinhardt) implies Con(ZFC + an inaccessible). So perhaps the question should really be: what large cardinal strength, if any, can we extract from the theory ZF + Reinhardt?

Infinity: New Research Frontiers(Cambridge 2011, Heller & Woodin eds.), Woodin writes in the article "The Realm of the Infinite", §4.3.2, that "by the results of Woodin (2009), the theory ZF+“There is a weak Reinhardt cardinal”provesthe formal consistency of the theory ZFC+“There is a proper class of strongly (ω+1)-huge cardinals”" (emphasis his). Sadly, the reference "Woodin (2009)" is nowhere to be found! (contd.) $\endgroup$ – Gro-Tsen Apr 22 '16 at 13:30