The definable power set consists of the subsets of definable over the first-order structure by a first-order formula with parameters from . Satisfaction for a set structure makes this a definable operation in ZF. Iterating it produces the constructible hierarchy and the relative constructible hierarchy; their unions are the constructible universe and the relative constructible universe.
A useful finite conjunction of closure assertions requires empty set, pairing, set union, set difference, Cartesian products, all finite tuple domains , and the following operations on their relations: relative complements, intersections, coordinate projections and pullbacks along finite coordinate maps, together with equality and membership restricted to . The arities and maps are quantified objects, so these requirements form finitely many first-order formulas, not an infinite schema. In a transitive set, individual finite tuples exist by pairing and union, making the tuple-domain assertions correct externally. Atomic truth relations, Boolean operations and projection then compute the truth table of each coded first-order formula correctly by finite induction. Thus satisfaction for a set structure and the relation are absolute for shared arguments. Every nonzero limit level of the relative constructible hierarchy is closed under these operations, since each result can be defined at finitely many subsequent stages.
The constructible hierarchy is defined byfor limit ordinals . Its union is the constructible universe .
The equality can fail even at . Inside the constructible universe, is countable, so its definable power set is countable. The constructible power set of is uncountable there by the Cantor theorem. A real outside remains a constructible subset of , hence belongs to . The cardinal comparison must be made inside , since its reals can be externally countable.
For a transitive model of ZFC and , the internally computed constructible hierarchy agrees with the ambient level: . Satisfaction for a fixed set structure is computed from the same finite formulas and the same domain in both universes. Transfinite recursion then proves agreement at successors and limits. If , it follows that .
If is a transitive model of ZF, its internally computed is the actual for each ordinal . At a successor stage use absoluteness of satisfaction for the same set structure, formula codes and parameters; at a limit stage take the union of the already identical earlier stages. Choice is not required.
The constructible universe is the inner model obtained by iterating the definable power set. It satisfies ZFC and the Generalized continuum hypothesis.
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.
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.
To separate a subset of a constructible set by a formula interpreted in the constructible universe, apply the reflection theorem for definable hierarchies to the formula and its subformulas. At a sufficiently large reflecting level containing the parameters, the desired subset is definable and belongs to the next constructible hierarchy level. The reflection proof uses least witness stages and ambient Axiom schema of replacement, so does not presuppose Axiom schema of separation within the constructible universe.
ZFC proves that the constructible universe is an inner model of ZFC and satisfies the Generalized continuum hypothesis. Relativizing to yields the corresponding relative-consistency implication.
The constructible universe satisfies the diamond principle. Together with antichain sealing by diamond, this supplies a Suslin tree in .
This statement says that the first uncountable ordinal of an inner model is a countable ordinal in the ambient universe. It can hold together with the Generalized continuum hypothesis: start with constructibility and use a finite-function collapse to countable size on . The GCH preservation by a finite-function collapse calculation gives the relative consistency result already from the consistency of ZFC.
Inside the constructible universe, every hereditarily countable set appears in a countable level of the constructible hierarchy. Take a countable elementary substructure of a sufficiently large containing its transitive closure pointwise. The condensation lemma for the constructible universe identifies the collapse with for countable , and the collapse fixes the original set. Conversely, a countable-indexed level is countable inside the constructible universe.
For , its constructible power set isUnlike the single-stage definable power set , it includes subsets of appearing arbitrarily late in the constructible hierarchy.
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.
An inner model of ZF containing all ambient subsets of computes the same countable ordinals as the ambient universe. Every ambient countably infinite ordinal has a well-order code coded by a subset of , hence that code belongs to ; finite ordinals are already shared. The Mostowski collapse theorem inside recovers the actual ordinal and its countability witness. Conversely any countability witness in remains one outside. If also contains the full power set of as a set, its Continuum hypothesis would give an ambient bijection from onto that same power set. Thus an ambient failure of this well-orderable formulation of the Continuum hypothesis is preserved in such an inner model. No internal axiom of choice is required for this argument.
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.
If is a nonzero limit ordinal and with , the Mostowski collapse theorem sends to for some nonzero limit and fixes pointwise. The base is fixed by transitivity and inclusion of all its members. Transfer the relative constructible level recognition formula first by elementarity and then through the collapse isomorphism to identify its image. If , ordinal heights are and , giving the bound. Having only does not guarantee this base-fixing version.
For transitive sets with , a single first-order formula recognises the nonzero limit levels . Require finite relation closure for set-theoretic coding, transitivity of , that every element belongs to a coded relative constructible stage, and that every represented stage index has a larger represented index. Correct history codes have downward-closed indices with no maximum, hence form a nonzero limit ordinal . The exhaustion assertion and transitivity then give . Conversely every limit level has the required closure, correct histories cofinal in its index, and exhaustion. This formulation does not assume ZF for an arbitrary input and does not replace finite coding closure with an unjustified internal constructibility assertion.
This first-order formula asserts the existence of a history function on starting at , applying definable power set at successors and unions at nonzero limit ordinals, and ending at . In a transitive set satisfying finite relation closure for set-theoretic coding, each history is correct by transfinite induction, so . Relation operations produce restrictions to shorter histories. Since stage histories appear below every limit constructible level, every history of length for belongs to when is a nonzero limit ordinal. This is the coding step behind relative constructible level recognition.
For a transitive set , let be the history function on in the relative constructible hierarchy. By transfinite induction, for some finite , possibly depending on . The base and successor steps follow by forming finite ordered pairs and adjoining the next entry, using . These operations require finitely many subsequent definable power sets.
At a nonzero limit ordinal , the inductive bounds put every earlier in , since . This level satisfies finite relation closure for set-theoretic coding, independently of the availability of history functions. Consequently its coded relative constructible stage predicate computes the endpoints correctly. Finite pairing closure and the earlier histories show thatcontains exactly the pairs for . There are no extra indices: if and , increasing levels would give , contradicting Axiom of foundation. Thus is a definable subset of and belongs to . Extracting its domain and adjoining uses finitely many further operations, proving the induction step. Every nonzero limit therefore contains all with , as required by relative constructible level recognition.
Assume a transitive model satisfies . In , encode a bijection by one set , using a fixed pairing of with . Then decodes and contains every real of . The two models consequently have the same , and any bijection between and the real numbers in would also be one in . Thus .
A condensation sentence is a fixed first-order sentence such that every transitive set satisfying is for a limit ordinal . It combines a sufficiently strong finite fragment of set theory, the assertion that every set is constructible, and the absence of a largest ordinal.
A well-order code is a binary relation for which is a well-order. Its representation is the unique countable ordinal isomorphic to .
A level is a coding level when is a limit ordinal, the representation of every well-order code in is below , and every ordinal below has a well-order code in .
Articles by others on the same topic
There are currently no matching articles.