2014/11/29 by Farmer Schlutzenberg, Schlutzenberg, Farmer · 2 citations
Biochemistry, Genetics and Molecular Biology · Computer Science · Mathematics · #03E45 #03E55 #Advanced Topology and Set Theory #Amino Acid Enzymes and Metabolism #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO)
paper · pdf · doi:10.48550/arxiv.1412.0085
openalex publication_date 2014/11/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Let M be a fine structural mouse and let F∈ M be such that M\models``F is a total extender'' and (M||lh(F),F) is a premouse. We show that it follows that F∈𝔼M, where 𝔼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 Σ\upharpoonright M then 𝔼M is definable over the universe \lfloor M\rfloor of M, so if also \lfloor M\rfloor\modelsZFC then \lfloor M\rfloor\models``V=HOD''. We show that this result applies in particular to M=Mnt|λ, where Mnt is the least non-tame mouse and λ is any limit cardinal of Mnt. 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[𝔼] constructions computed in iterable background universes.