An inner model of a universe of ZF is a transitive class containing every ordinal and satisfying the required set-theoretic axioms with the inherited membership relation. Transitivity means that every member of a member of belongs to . Requiring all ordinals distinguishes an inner model from a transitive set first-order model such as : a set first-order model has bounded ordinal height. One may specify an inner model of ZF, ZFC or a stronger theory; choice is not built into the term unless specified.
The fundamental example is the constructible universe. Form the constructible hierarchy
Here definable power set means subsets definable over the set structure by first-order formulas with finitely many parameters from that level. Each level is transitive, the levels increase, and , by induction. Thus is transitive and contains all ordinals.
The construction supplies a definable well-order: order objects first by their earliest construction stage, then by a least first-order formula code and a finite tuple of parameters in the already constructed level's well-order. Recursively extend the earlier well-order at each successor stage and unite compatible orders at limits. First-order formula codes and finite tuples of well-ordered parameters are well-orderable. This yields a canonical global ordering definable within ; its restrictions to sets will give choice once the ZF axioms are checked.
For that check, a useful reflection argument is explicit. Given finitely many first-order formulas and a starting level, pass to a higher level containing witnesses for their existential subformulas on all parameter tuples from the current level, choosing least witnesses in the canonical order. There are set-many tuples, so ambient replacement bounds their witness stages. Repeat for steps and take the union level . Every relevant witness with parameters in that level appears at a later step. Induction on first-order formulas, with this witness property for the existential case, proves that reflects the chosen finite list of first-order formulas of .
Separation on a constructible set is then definability over a sufficiently large reflecting level, so its subset appears at the next level. For replacement, reflect the first-order formula specifying a functional image and its required existence statements. All inputs belong to a level containing the domain as a set; all their unique outputs then lie in one reflecting level. The image is definable there and hence is constructible. For power set, the ambient set of constructible subsets of has bounded construction stages by replacement in the ambient universe. At a level containing them all, this internal collection is definable by the bounded condition , and therefore is itself in . Pairing, union and axiom of infinity follow directly from definability over sufficiently large levels, while extensionality and foundation follow from transitivity. Thus , and its canonical ordering gives .
This proves the important relative-consistency application
One does not conclude that choice is true in the original universe. Instead the inner model supplies a possibly smaller universe in which choice holds.
Constructibility also supplies GCH. Here is the cardinal-counting argument, making clear the role of the condensation lemma for the constructible universe. Work inside . If is constructible, take a large limit containing and an elementary hull of of size . Its transitive collapse is by condensation. The collapse fixes every ordinal below , and hence fixes and . Since the hull has size , . Therefore every constructible subset of appears below .
The condensation fact expresses the rigidity of this definability construction: first-order formula codes, finite parameter tuples and satisfaction in set-sized lower levels are preserved by the collapse. Inducting over the hull's ordinal indices identifies each collapsed lower level with the corresponding -level; elementarity supplies every definable subset coded by parameters in that collapsed lower level. Taking unions identifies the entire collapsed hull with a level .
Induction on construction stages gives : each successor has only countably many first-order formula schemes with finite parameter tuples, and limits take unions. Hence for infinite . The preceding containment gives in , and Cantor's theorem gives the reverse inequality. Consequently
All these cardinal computations are internal to ; they need not equal the ambient cardinal computations.
Inner models are also useful for analyzing stronger axioms. If is inaccessible in , it remains an uncountable regular cardinal in , because a shorter cofinal sequence in would already be one in . For each ordinal , its constructible subsets are fewer than even in the internal cardinal comparison: in , has size below , so its constructible part cannot have an -well-order of length at least . Thus it remains strong limit. Accordingly supplies relative-consistency information compatible with inaccessibles and GCH. Stronger embedding or measure properties require extra analysis, since the witnessing objects may disappear upon passing to an inner model.
There is a useful limitation: no uniform inner-model construction can refute choice from every starting ZF universe. Every inner model of ZF contains the ambient . Indeed, induction gives : the same set-sized level has the same satisfaction relation for definitions, and limit stages take the same unions. If the starting universe already satisfies , any inner model containing all ordinals must therefore be the whole universe, where choice holds. To obtain a choice-failing first-order model uniformly one needs a different method, such as the symmetry restriction in the preceding solution. Inner-model arguments establish consistency and preservation through carefully controlled smaller universes; they do not freely manufacture arbitrary desired axiom failures.
An inner model of ZF is a transitive class containing all ordinals and satisfying ZF with the inherited membership relation. The “all ordinals” requirement is important: an arbitrary transitive set model or a rank segment is not an inner model in this sense.
Every such inner model contains the ambient constructible universe . Here is the reason. Inductively . The zero stage is the same empty set. If the stages at agree, satisfaction for the common set structure is absolute: atomic first-order formulas agree, Boolean operations agree, and quantified variables range over the identical set. The codes of finite first-order formulas are also the same because a transitive model of ZF has the actual natural numbers. Consequently definability with parameters from produces exactly the same subsets in both models, so their successor constructible stages agree. At a limit ordinal both constructions take the union of the same earlier stages. This proves agreement at every stage and hence .
The constructible universe theorem provides models of ZF satisfying and the axiom of choice, whenever ZF is consistent. In such a universe any inner model of ZF satisfies
so and it also satisfies choice. Therefore
Passing to proves the consistency of choice, but the same downward method cannot prove its negation from an arbitrary starting model: it has no possible output when the starting universe is constructible. This is the precise obstruction intended in an inner-model independence argument. It is not a claim that every inner model of every choice universe satisfies choice; symmetric submodels of suitable forcing extensions can fail choice, and that method first changes the ambient universe.
An inner model of ZFC is a transitive class containing every ordinal and satisfying all its axioms. Write this class as with its inherited membership relation. Satisfaction is interpreted by restricting all quantifiers to . In a first-order formulation this is a schema for a definable class, possibly with fixed parameters. The class may equal the whole universe. Transitivity means ; containing all ordinals rules out treating an arbitrary transitive set model as an inner model.
First express inaccessibility by universally excluding witnesses to its failure. Besides being an ordinal greater than , require that for every there is no function from cofinal in , and no injection from into . The first condition gives regular cardinalhood; the second says that is a strong limit cardinal. Under the axiom of choice these are exactly the conditions for a strongly inaccessible cardinal.
These are Pi-one formulas modulo ZF: the only unbounded quantifiers universally range over possible functions. Being a function of the specified domain, having bounded or cofinal range in , and being an injection whose values are subsets of can all be written with bounded formulas in set theory, without using a power-set object as an unbounded existential witness. Consequently inaccessibility is downward absolute to a transitive inner model of ZFC.
Now suppose is Mahlo in . It is inaccessible in the constructible universe , and every -inaccessible ordinal below it is also inaccessible in . Let be any set that regards as a club set in . Closure and unboundedness are absolute properties of this fixed set of ordinals, so is also a club set in . By Mahloness in , it contains an ordinal that is inaccessible in , hence in . Every -club therefore meets the -inaccessible ordinals below . Thus Mahloness is downward absolute to the constructible universe:
The assumed beth number equality means in the ambient universe. Put with , using the relative constructible hierarchy defined above.
The base is transitive because every member of a member of is a finite ordinal, hence itself a subset of . Moreover and , and is an inner model of ZF. The latter standard fact follows from the hierarchy and reflection: bounded-rank witnesses give pairing and union; reflection gives separation and replacement; ambient replacement bounds the stages of all relatively constructible subsets of any fixed set, giving power set. It does not require axiom of choice inside . Since no new subsets of can appear in an inner class,
Since inner models with all reals preserve omega-one, it suffices to check that their real-code argument applies to . Every ambient countably infinite ordinal has a well-order code on , coded by a subset of in . Finite ordinals and are already shared. This code belongs to , is well-founded there, and its Mostowski collapse theorem interpretation inside is the same ordinal as outside. Hence the ordinal is countable in . Conversely, any countability witness in remains a witness in the ambient universe. Thus .
If satisfied the Continuum hypothesis in its usual well-orderable formulation, it would contain a bijection from onto its power set of . The same bijection would exist externally from onto , contradicting . Therefore
This proof uses agreement on all reals and on , not an unwarranted assertion that satisfies axiom of choice or computes every higher cardinal number correctly.
An inner model is projectively well-ordered when some projective relation well-orders the real numbers of . The ordinal is the least ordinal that regards as uncountable; equivalently, it is the supremum of the order types of the well-order codes in .
Assume for contradiction that is uncountable in the ambient universe. Use the projective well-order of the reals of to choose, for each , the least -real coding a well-order of type . Standard closure properties of the projective hierarchy make the resulting set projective. It is uncountable because it contains one distinct code for every .
The set has no perfect subset. Indeed, a perfect subset is closed and therefore analytic. The boundedness theorem for well-order codes bounds the ranks of its members below one countable ordinal . Since contains at most one code of each rank, would then be countable, whereas every nonempty perfect set of reals is uncountable.
If every projective set is determined, projective determinacy holds and gives the perfect set property to every projective set. Applying it to the uncountable projective set yields a perfect subset, a contradiction. Therefore
This is projective determinacy collapses the inner-model omega-one.
An inner model is projectively well-ordered when there is a projective relation that well-orders the real numbers belonging to .
For a transitive set , use , and unions at nonzero limit ordinals. The successor operation is the definable power set. Each level is transitive and the levels increase; moreover . Their union is , an inner model of ZF. The initial-set convention differs from a hierarchy using a predicate, or one starting at . Axiom of choice need not hold for an arbitrary base without an internally available well-order.
Relative constructible universe Created 2026-10-03 Updated 2026-10-05
For a transitive set , the relative constructible universe is the union of the relative constructible hierarchy, starting at , applying the definable power set at successors and taking unions at limit ordinals. It is the smallest inner model of ZF containing and all its members. For an arbitrary set , take the base to be the transitive closure of , so that . Axiom of choice need not hold for an arbitrary base; the construction uses initial parameters rather than a predicate relativization.
Shepherdson's wall 2026-10-14
The obstruction to proving the consistency of nonconstructibility by a uniform inner model construction is that, inside a universe satisfying , every transitive inner model containing all ordinals has as its own constructible universe and therefore is the entire ambient universe. The absoluteness of constructible levels proves this by induction over successor definability and limit unions. Thus a construction valid in every model of ZF cannot always produce such an inner model satisfying , and in particular cannot always produce one violating axiom of choice.