On the consistency of ZF with an elementary embedding from Vλ+2 into Vλ+2

According to a theorem due to Kenneth Kunen, under ZFC, there is no ordinal Formula: see text and nontrivial elementary embedding Formula: see text. His proof relied on the Axiom of Choice (AC), and no proof from ZF alone is has been discovered. Formula: see text is the assertion, introduced by Hugh Woodin, that Formula: see text is an ordinal and there is an elementary embedding Formula: see text with critical point Formula: see text. And Formula: see text asserts that Formula: see text holds for some Formula: see text. The axiom Formula: see text is one of the strongest large cardinals not known to be inconsistent with AC. It is usually studied assuming ZFC in the full universe Formula: see text (in which case Formula: see text must be a limit ordinal), but we assume only ZF. We prove, assuming ZF Formula: see text Formula: see text Formula: see text “Formula: see text is an even ordinal”, that there is a proper class transitive inner model Formula: see text containing Formula: see text and satisfying ZF Formula: see text Formula: see text Formula: see text “there is an elementary embedding Formula: see text”; in fact we will have Formula: see text ⊆Formula: see text, where Formula: see text witnesses Formula: see text in Formula: see text. This result was first proved by the author under the added assumption that Formula: see text exists; Gabe Goldberg noticed that this extra assumption was unnecessary. If also Formula: see text is a limit ordinal and Formula: see text-DC holds in Formula: see text, then the model Formula: see text will also satisfy Formula: see text-DC. We show that ZFC Formula: see text “Formula: see text is even” Formula: see text Formula: see text implies Formula: see text exists for every Formula: see text, but if consistent, this theory does not imply Formula: see text exists.