The definability of the extender sequence from E↾ℵ_1 in L[E]

Schlutzenberg Farmer

Abstract

Let M be an iterable fine structural mouse. We prove that if e ∈ M and M ⊨ ``e is a countably complete short extender whose support is a cardinal θ and H_θ ⊆ Ult(V,e)'' then e is in the extender sequence E^M of M. We also prove other related facts, and use them to establish that if κ is an uncountable cardinal of M and (κ+)^M exists in M then (H_κ+)^M satisfies the Axiom of Global Choice. We then prove that if M satisfies the Power Set Axiom then E^M is definable over the universe of M from the parameter X = E^M↾ℵ_1^M, and therefore M satisfies ``Every set is OD_X''. We also prove various local versions of this fact in which M has a largest cardinal, and a version for generic extensions of M. As a consequence, for example, the minimal proper class mouse with a Woodin limit of Woodin cardinals models ``V=HOD''. This adapts to many other similar examples. We also describe a simplified approach to Mitchell-Steel fine structure, which does away with the parameters u_n.

Talks on the publication