ORDINAL DEFINABILITY IN upper L double struck upper E $L[\mathbb {E}]$ L E
Farmer Schlutzenberg · Journal of Symbolic Logic · 2026
Abstract Let M be a tame mouse modelling upper Z upper F upper C $\mathrm {ZFC}$ Z F C . We show that M satisfies “ upper V equals upper H upper O upper D Subscript x $V=\mathrm {HOD}_x$ V = H O D x for some real x ”, and that the restriction upper E Superscript upper M Baseline backslash exclamation mark up harpoon with barb right backslash exclamation mark omega 1 Superscript upper M Baseline comma upper O upper R Superscript upper M Baseline right parenthesis $\mathbb {E}^M\!\upharpoonright \![\omega _1^M,\mathrm {OR}^M)$ E M \! ↾ \! ω 1 M , O R M ) of the extender sequence upper E Superscript upper M $\mathbb {E}^M$ E M of M to indices above omega 1 Superscript upper M $\omega _1^M$ ω 1 M is definable without parameters over the universe of M . We show that M has universe upper H upper O upper D Superscript upper M Baseline upper X $\mathrm {HOD}^M[X]$