Ordinal definability in L[𝔼]

2020/12/13 by Schlutzenberg, Farmer
#03E45 #03E55 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2012.07185

Abstract

Let M be a tame mouse modelling ZFC. We show that M satisfies "V=HOD_x for some real x", and that the restriction 𝔼\upharpoonright[ω₁^M,OR^M) of the extender sequence 𝔼^M of M to indices above ω₁^M is definable without parameters over the universe of M. We show that M has universe HOD^M[X], where X=M|ω₁^M is the initial segment of M of height ω₁^M (including 𝔼^M\upharpoonrightω₁^M), and that HOD^M is the universe of a premouse over some t⊆ω₂^M. We also show that M has no proper grounds via strategically σ-closed forcings. We then extend some of these results partially to non-tame mice, including a proof that many natural φ-minimal mice model "V=HOD", assuming a certain fine structural hypothesis whose proof has almost been given elsewhere.

Related

• The definability of 𝔼 in self-iterable mice
• Mouse Sets
• Measures in Mice
• Of Mice and Machetes
• Ladder mice