Kunen: no elementary self-embedding of a two-step rank segment

Open

Bagaria.kunen_no_segment_embedding

by Lucas · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementaryembeddingskuneninconsistencylargecardinalssettheory

Kunen's inconsistency theorem in its bounded form (slide 8): assuming the universe satisfies ZF, there is no non-trivial elementary self-embedding of the two-step rank segment below the double successor of any ordinal l — the abstract analogue of V_{l+2}. This is the obstacle that rules out Reinhardt cardinals under the Axiom of Choice, and the boundary within which the choiceless hierarchies of the source live.

Preamble

import Mathlib
import Definitions.Def_Bagaria_arena
import Definitions.Def_Bagaria_reinhardt
import Definitions.Def_Bagaria_berkeley

Formal statement

universe v

namespace Bagaria

open Universe

/-- Kunen's inconsistency in the bounded segment form (slide 8): assuming
the universe satisfies ZF, there is no non-trivial elementary
self-embedding of the two-step rank segment below the double successor of
any ordinal l — the abstract analogue of V_{l+2}. -/
theorem kunen_no_segment_embedding (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
    (l : Ordinal.{v}) :
    ¬ ∃ j : U.segmentOfSuccSucc l → U.segmentOfSuccSucc l,
      j ≠ id ∧
        IsElementaryOf (U.segmentMem (U.succ (U.succ l)))
          (U.segmentMem (U.succ (U.succ l))) j := by
  sorry

end Bagaria

Source

Bagaria (2017), Large Cardinals beyond Choice, AILA XXVI slides, p. 8, Theorem (Kunen); Kunen (1971), On the Question of the Existence of a Nontrivial Elementary Embedding of V into V, J. Symbolic Logic 36

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

The statement says: given an abstract universe U whose membership relation satisfies the semantic first-order ZF axioms, and an ordinal l, there is no function j from the two-step rank segment below the double successor of l to itself that differs from the identity and preserves the satisfaction of every first-order set-theoretic formula under every assignment, where satisfaction is taken with the membership relation inherited from U on that segment. The ZF hypothesis carries no form of Choice; the segment form is stated over ZF alone.

View graph