The definability of E in self-iterable mice [Die Definierbarkeit von E in selbstiterierbaren Mäusen]

Schlutzenberg, Farmer

Abstract

Let M be a fine structural mouse and let F ∈ M be such that M ⊨``F is a total extender'' and (M || lh(F), F) is a premouse. We show that it follows that F ∈ E^M, where E^M is the extender sequence of M. We also prove generalizations of this fact. Let M be a premouse with no largest cardinal and let σ be a sufficient iteration strategy for M. We prove that if M knows enough of σ↾M then E^M is definable over the universe ⌊M⌋ of M, so if also ⌊M⌋ ⊨ ZFC then ⌊M⌋ ⊨``V=HOD''. We show that this result applies in particular to M = M_nt | λ, where M_nt is the least non-tame mouse and λ is any limit cardinal of M_nt. We also show that there is no iterable bicephalus (N,E,F) for which E is type 2 and F is type 1 or 3. As a corollary, we deduce a uniqueness property for maximal L[E] constructions computed in iterable background universes.