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 .
Articles by others on the same topic
There are currently no matching articles.