Axiom of constructibility Created 2026-10-07 Updated 2026-10-14
Every set belongs to some level of the constructible hierarchy. The assertion is , not that each set is definable without parameters. The constructible universe theorem supplies a relative-consistency model of this assertion from ZFC.
An inner model of ZF is a transitive class containing every ordinal, with inherited membership, such that each ZF axiom holds with all quantifiers restricted to . Here transitivity means . For a proper class this is an axiom-by-axiom assertion, not an internal truth predicate for the whole class. An inner model can have fewer subsets of a given set than the surrounding universe; it need not have the same cardinals or the same continuum function.
Inner models prove relative consistency. If a theory proves that a definable class satisfies every axiom of , an inconsistency proof from could be relativized to and become an inconsistency proof from . Thus . This reasoning concerns formal interpretations and needs no assumption that a given model of is externally well-founded.
The central example is the constructible universe. Define
where contains exactly the subsets definable over using parameters from . Satisfaction for a set structure is definable, so this recursion is available in ZF. Induction shows that the levels are transitive and increasing: if , the subset is , so . The ordinal part of is , giving all ordinals in .
For completeness, the main axiom mechanisms explain why this example works. Finite set operations on constructible parameters are definable at finitely many further stages. For a fixed finite family of formulas and parameters, close a sequence of levels under their least constructible witness stages and take its union; induction on formulas gives a reflecting level. Separation of a constructible set then occurs at the next definability stage. For replacement, ambient replacement bounds the construction stages of the unique constructible outputs; a reflecting level above that bound makes the range definable. For the internal power set of , use ambient separation to form , bound the construction stages of its members, and at a sufficiently high level define the family of all subsets of in that level. Thus the internal power set is constructible even though some ambient subsets may not be. Foundation is inherited by transitivity, and infinity comes from and its successor stages.
There is a canonical well-order of : order by first construction stage, then by the least definition code and finite parameter tuple, using the previously constructed well-orders for parameters. Each set in can be well-ordered by the restriction of this set-like class order; hence satisfies AC. Moreover the hierarchy computed inside is the same hierarchy, because definability over a fixed set structure and limit unions are absolute. Thus satisfies . The further cardinal analysis of this hierarchy, encapsulated in the constructible universe theorem, gives GCH. Consequently
This proves the relative consistency of choice, CH and GCH; in particular none can be refuted by ZF if ZF is consistent. The assertions here are internal to : they do not assert CH in the ambient universe.
Inner models also isolate definable information. The relative constructible universe built with a set parameter retains that parameter and all ordinals while discarding unrelated sets. Such constructions help compare relative consistency strengths and identify which hypotheses survive passage to smaller universes; preservation of a large-cardinal property must be checked separately, not inferred merely from transitivity.
There is an important limitation, the constructible-universe obstruction to a uniform inner-model proof of failure of choice. Every inner model of ZF contains the ambient . Indeed by induction: the same set structure has the same definable subsets at a successor stage, and both hierarchies take the same union at a limit. If the ambient universe satisfies , this forces . Thus inner models cannot uniformly produce a model of or from every ZF universe. To prove the opposite independence directions one needs an outer-model or other interpretation technique, such as forcing or the non-well-founded symmetry construction in Question 2.
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.
All assertions of independence below are relative consistency assertions. We construct structures satisfying the other ZF axioms but falsifying the indicated axiom; an ordinary model of ZF supplies the positive side. The convenient ground theory is ZFC, which has the same consistency strength as ZF by the constructible universe theorem.
For the Axiom of union, put and use the hereditarily locally small membership model
It is a transitive class. The condition requires each individual set in the membership ancestry to have size below ; it does not require its entire transitive closure to have size below . Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and witnesses infinity. For , the actual also belongs to : if , then by the strong-limit property, while every subset of and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain , ground replacement, applied to the relativized first-order formula, gives its range . Since and every value is already in , its range is also locally small. Thus every replacement instance holds.
However, belongs to : its members have cardinalities , and their members are smaller still. Its actual union is , of cardinality , which is not in . Transitivity makes any internal union witness equal to this actual union. Hence Union fails while all the other ZF axioms hold.
For the Axiom of power set, use the hereditarily countable sets in the ground choice universe. This is transitive and contains . Pairs, subsets and unions have countable transitive closure. For replacement, a functional image of a countable domain is countable, and the union of countably many countable transitive closures is countable; hence that image is again hereditarily countable. These observations, with inherited extensionality and foundation, verify all the remaining axioms. Every real, viewed as a subset of , belongs to . A power-set witness for would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas is uncountable by Cantor's theorem. Power set fails.
For the Axiom schema of replacement, use with actual membership. This limit-rank structure contains and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below . A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable function
is obtained by successive power-set operations starting with the parameter . Each finite iteration, including its finite history, belongs to the structure. Its range has rank and is not an element of . Thus the replacement instance for this first-order formula fails, although every other ZF axiom holds.
For the axiom of extensionality, take the well-founded cumulative set universe over two distinct urelements, and forget the predicate distinguishing urelements from sets. Each urelement has no members, just as the ordinary empty set has no members, so extensionality fails. Every other axiom survives in this pure membership language. Pairing, union, separation and replacement are witnessed by the corresponding ordinary sets of urelements and sets; foundation follows from their well-founded ranks, and the pure supplies infinity. Here foundation is written with “has a member” as its nonemptiness antecedent, and disjointness means having no common member. Formulations using inequality to one designated empty object are not equivalent after removing extensionality. There is also one necessary adjustment to power set: an urelement is vacuously a subset of every object because it has no members. Thus the power-set witness for is the ordinary set of all usual subsets of its extension, together with both urelements. This is still a set, and contains exactly the objects satisfying the unrestricted subset first-order formula. Consequently the countermodel falsifies Extensionality alone, without silently weakening Power set to sets only.
Finally, the hereditarily finite sets satisfy extensionality, foundation, pairing, union, power set and separation. Every functional image of a finite domain is a finite set of hereditarily finite objects, hence also belongs to , giving all replacement instances. No finite set contains and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.
The diamond theorem in the constructible universe gives , and satisfies ZFC. Apply the preceding construction inside with . It produces a normal splitting Suslin tree.
For completeness, such a tree yields a Suslin line. Order its nodes lexicographically using the two successors at every split, treating a node itself as a position between its two successor subtrees. Each node is thus a cut point between a left and a right subtree. This gives a dense linear order without endpoints. Every nonempty interval contains a whole cone above some node: for comparable endpoints use the successor cone of the descendant endpoint directed toward the other endpoint; for incomparable endpoints use the right-successor cone of the lower endpoint. Disjoint intervals therefore supply pairwise incomparable cone roots, so the order has the countable chain condition for a linear order. A countable collection of nodes has bounded heights; a cone based above that bound contains none of them, so it is not an order-dense subset. Passing to the Dedekind completion using proper cuts, so that no endpoints are added, preserves density, the countable chain condition for a linear order, and nonseparability. For nonseparability, a countable dense set in the completion would give a countable dense set of original nodes by choosing one original node between each distinct pair of its points. This contradicts the preceding height-bound argument. The result is a Suslin line.
Thus the Suslin hypothesis fails in . The constructible universe theorem is a theorem of ZFC, so this is a relative-consistency argument, without an additional assumption that a transitive model exists:
In the generic extension from the preceding construction, a surjection from onto all reals gives . Cantor theorem gives the reverse inequality, so the Continuum hypothesis holds.
For the exact consistency-strength statement, existence of a countable transitive model is stronger than bare consistency of ZFC. One can formalize the forcing proof syntactically, or use the constructible universe theorem: ZFC proves that its constructible universe satisfies ZFC and the Generalized continuum hypothesis. If there is any model of ZFC, its internal constructible universe is therefore a model of ZFC with CH. By the Godel completeness theorem,
This deduction does not silently replace consistency by existence of a transitive model.