math.LO
The definability of the extender sequence mathbb E from mathbb E upharpoonright aleph 1 in L mathbb E . Let M be an iterable fine structural mouse. We prove that if E in M and M models E is a countably complete short extender whose support is a cardinal theta and mathcal H theta subseteq mathrm Ult (V,E) '' then E is in the extender sequence mathbb E M of M . We also prove other related facts, and use them to establish that if kappa is an uncountable cardinal of M and ( kappa ) M exists in M then ( mathcal H kappa ) M satisfies the Axiom of Global Choice. We then prove that if M satisfies the Power Set Axiom then mathbb E M is definable over the universe of M from the parameter X mathbb E M upharpoonright aleph 1 M , and therefore M satisfies Every set is mathrm 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 mathrm 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 .