For parameters , set-theoretic absoluteness means agreement of the two membership first-order structures:This must hold for every such parameter tuple. Equivalently, formula relativization to a class produces two formulas and whose truth values agree on tuples from . Agreement for parameters only in is not part of the definition. For a proper class in set theory, this notation is understood separately for each fixed first-order formula, rather than as an unrestricted truth predicate for the entire universe.
A syntactically bounded formula in set theory is built from the atomic first-order formulas and using Boolean operations and bounded quantifiers and . These abbreviate and , with different from the bounding variable .
The superscript in the question allows provable equivalence: a ZF-equivalent bounded formula is any first-order formula for which some syntactically bounded formula in set theory satisfiesThus is the class of first-order formulas equivalent over ZF to a syntactic first-order formula. If a convention uses just for syntactically bounded set-theoretic first-order formulas, it is the smaller syntactic class; the subsequent set-theoretic absoluteness proof works for both conventions.
The Von Neumann hierarchy is the following transfinite recursion on the ordinals:Here denotes the full power set. The levels are increasing transitive sets, and the construction is continuous at limit ordinals. Transfinite induction proves these properties: transitivity at a successor follows because a member of a subset of already belongs to ; at a limit it follows from the set union of increasing transitive sets. In ZF, Axiom of foundation and Axiom schema of replacement ensure that every set belongs to some . In terms of the rank of a set, exactly when .
First prove set-theoretic absoluteness for syntactically bounded formulas in set theory by induction on their construction. Atomic equality and membership use the actual equality and membership relations in both transitive classes. Boolean operations preserve agreement.
For the bounded existential step, take and suppose . Its witness is an actual member of . Since is a transitive class, ; the induction hypothesis then gives . The converse uses the same witness in . The bounded universal step follows similarly because both structures quantify over exactly the actual members of , or follows by negation from the existential step. HenceNo ZF axioms are needed for this syntactic statement beyond the ambient meaning of a transitive class. For a ZF-equivalent bounded formula , choose a bounded equivalent . The assumption that both structures model ZF gives and . Combining these with the displayed equivalence proves the asserted set-theoretic absoluteness of .
The essential fact is absoluteness of cardinalhood in limit ranks. Let be limit ordinals and . Being an ordinal is absolute between these transitive sets, so a non-ordinal is a cardinal number in neither structure. For an ordinal , we have .
If is not an ambient cardinal number, there is an ordinal and a bijection . With Kuratowski ordered pairs, its graph has rank of a set at most . Since is a limit ordinal, , so . The assertion that is such a bijection is a bounded formula in set theory and is therefore evaluated correctly by each rank. Conversely, any internal bijection witnessing failure of cardinal number status is an actual one by the same set-theoretic absoluteness. ConsequentlyUnlike arbitrary transitive models, these rank-initial structures contain every sufficiently low-rank witness. That witness availability is what upgrades the usual downward absoluteness of cardinalhood to agreement in both directions.
Use the standard convention that a strongly inaccessible cardinal is uncountable, regular and strong limit. The printed explanatory definition omits uncountability: literally it also admits , for which no finite cardinal is a worldly cardinal. Thus that omission makes the requested conclusion false under the literal abbreviated definition. The proof below applies to the usual, intended strongly inaccessible cardinal convention .
First for every . At successor stages this follows from the strong limit cardinal property, and at limits from the regular cardinal property. Consequently . In particular, for Axiom schema of replacement, a domain has size less than , so its functional image has fewer than elements, so the supremum of the rank of a set over its elements is below by regular cardinal structure. All other axioms, including axiom of choice, have their witnesses at bounded ranks below ; uncountability supplies axiom of infinity.
Enumerate the first-order formulas as . For each finite collection, reflection inside the set structure gives a closed unbounded subset of of agreeing ranks. To see why the witness bounds stay below , there are fewer than parameter tuples at each , and the supremum of their least witness ranks remains below by regular cardinal structure. Closing under these bounds and taking increasing countable limits gives the usual reflection theorem for definable hierarchies argument. The countable intersection of these closed unbounded subsets is still closed unbounded because is regular and uncountable. At each resulting ,The infinite cardinal numbers below also form a closed unbounded subset: they are unbounded because for infinite , and a supremum of increasing cardinal numbers is a cardinal number. Intersect the two closed unbounded subsets. Every member of the intersection is a worldly cardinal, and an unbounded subset of a regular cardinal has size . HenceIn fact this proves the stronger worldly cardinals below an inaccessible cardinal result that these worldly cardinals contain a closed unbounded subset of .
A definable continuous hierarchy is a definable class function on the ordinals, with set-valued levels, such that for andfor nonzero limit ordinals. Its union is a definable class in set theory . Often the definition additionally requires every level to be a transitive set; the following statement also works without that requirement.
The reflection theorem for definable hierarchies says that for any finite collection of first-order formulas, there is a closed unbounded class of ordinals such that, for every and every parameter tuple from ,A useful justification is the witness-closure proof. Close under subformulas. At each level and for each existential subformula, bound the least level containing a witness for each parameter tuple for which a witness exists in . Axiom schema of replacement bounds these indices. Iterating the finitely many bounds through produces a limit level containing all required witnesses. Induction on the first-order formulas, equivalently the finite-formula version of the Tarski-Vaught test, yields agreement. Continuity gives closedness of the reflecting class, and starting above any prescribed ordinal gives unboundedness. This is finite reflection, not a claim that all first-order formulas reflect simultaneously in an arbitrary hierarchy.
Fix the base convention . For a transitive set , the relative constructible hierarchy isHere the definable power set isThe satisfaction for a set structure in this definition is a definable set-theoretic relation, obtained by finite syntax coding and recursion on a first-order formula. The transfinite recursion therefore defines a class in ZF.
Each level is a transitive set. For transitive , every is a subset of definable using the parameter , so ; also using the always-true first-order formula. Thus the levels increase and . Starting instead with is another common indexing convention, but it is not the convention used here. The relative universe need not satisfy axiom of choice: arbitrary need not have an internally available well-order.
Use relative constructible level recognition. The finite coding conditions matter here: merely writing “every set is relatively constructible” inside an arbitrary transitive set does not ensure that its computations are correct.
Let be a single finite conjunction expressing finite relation closure for set-theoretic coding. Concretely require the empty set, pairing, set union, set difference, Cartesian products, and the following uniform relation operations: for each finite ordinal and each set , the set of finite tuples exists; relations on these tuple domains can be complemented, intersected, projected along a coordinate and pulled back along finite coordinate maps; the equality and membership relations restricted to exist. These are finitely many first-order closure assertions with quantified, not an axiom schema. Each operation is specified by its usual elementwise membership equivalence. Transitivity makes the operations correct externally. Finite tuple domains are also correct: every individual finite tuple is already present by pairing and union.
These conditions make satisfaction for a set structure absolute. For a fixed coded first-order formula, compute its truth relations on by induction: equality and membership give the atomic cases, relative complement gives negation, intersection gives logical conjunction, and projection gives existential quantification. All required truth tables exist by and agree with the actual ones. Thus the first-order assertion is absolute whenever belong to a transitive structure satisfying : require that each member of has such a finite formula-and-parameter definition, and that each coded definition contributes a member of . Codes are finite objects; no truth predicate for the ambient universe is being used.
Write for the coded relative constructible stage assertion: is an ordinal and there is a function with domain , with , , at nonzero limit ordinals, and . Under , any such internal code is correct by transfinite induction. Restrictions of a code to shorter domains exist by the relation operations. Define the one-free-variable first-order formulaAll displayed abbreviations expand into first-order formulas of the membership language.
Suppose is transitive, , and . Let be the externally defined set of indices of stage codes in . It contains , is downward closed by restricting codes, and has no largest member by the last conjunct. Thus is a nonzero limit ordinal . Correctness of stage codes gives for , hence by transitivity. Conversely the exhaustion conjunct puts every in some such level. Therefore
For the converse, every with nonzero limit satisfies : each listed operation on parameters from one level is definable at finitely many later levels, still below . Moreover stage histories appear below every limit constructible level. Here is the essential limit step of that lemma. If the histories for are available in , the correct predicate defines their graph of endpoints as a subset of . No endpoint with can belong to , because would then give , contradicting Axiom of foundation. The defined graph therefore has domain exactly . Adjoining its final pair takes finitely many more stages. Together with finite successor extensions, this proves by transfinite induction that every belongs to for some finite .
Thus all histories for belong to . Exhaustion follows from continuity, and supplies a larger represented stage. Hence , proving both directions without assuming ZF for the arbitrary input structure .
A suitable relative condensation lemma fixes the base pointwise. Let be a nonzero limit ordinal, and let be an elementary substructure withThen the Mostowski collapse theorem gives an isomorphism onto a transitive set, andFor the collapse to apply, the restricted membership relation is well-founded because it is actual membership. It is extensional: if two members of differ, an element distinguishing them in can be chosen in by elementary substructure structure. Since is transitive and all its members are in , transfinite induction on their rank of a set shows that fixes every member of , and then .
By the preceding relative constructible level recognition, . Elementary substructure agreement transfers this to , and the collapse isomorphism transfers it to . Thus and for a nonzero limit ordinal .
For the bound, let . The relative constructible hierarchy has ordinal height : at a successor the definable power set adds exactly the previous ordinal height as a new ordinal, and at limits take unions. The order type of is at most , so ; strict increase of ordinal addition in the right argument gives . The requirement is essential to this version: merely having need not make the collapse fix the base.
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 . ThereforeThis proof uses agreement on all reals and on , not an unwarranted assertion that satisfies axiom of choice or computes every higher cardinal number correctly.
Use standard notation for forcing: means that is stronger. A generic filter is nonempty, upward closed and downward directed, and meets every dense subset of a forcing order in the ground model. Names below are forcing names in , with pairs ordered as .
The semantic forcing relation isHere is the evaluation of a forcing name. Countability of supplies such generic filters through every condition by the Rasiowa–Sikorski lemma.
Define the syntactic forcing relation by mutual well-founded recursion on the forcing names for the atomic cases, then induction on the first-order formula. Its membership clause isFor equality, first abbreviateand set exactly when both inclusions hold. Each recursive call lowers the rank of at least one forcing name without raising the other. This makes the mutual recursion well-founded.
For a basis of connectives consisting of logical conjunction, negation and existential quantification, the remaining clauses areThe last line is the existential clause of syntactic forcing; witnesses need only occur densely, rather than be forced by itself with one preselected name. Other connectives are defined by logical abbreviations. The recursion gives a definable relation inside for each fixed first-order formula, with quantification over the class of its names. If has no greatest element, use canonical forcing names , which still evaluate to . It also proves monotonicity: strengthening a condition preserves what it forces. The forcing theorem identifies the two relations and supplies the truth lemma.
This is the forward implication of the atomic membership truth lemma for forcing. Suppose . By the evaluation of a forcing name, choose with and . The assumed equality truth lemma supplies with .
Directedness of the generic filter gives with . For every , monotonicity of the syntactic forcing relation gives , and . Thus itself witnesses the required membership density below . HenceOnly the equality truth lemma stipulated in the source and the recursive membership clause have been used.
Conversely, suppose and . The syntactic forcing relation says thatis dense below a forcing condition . This is a set in by definability of forcing and axiom schema of separation. The dense-below generic meeting lemma gives : augment by all incompatible forcing conditions with to obtain a globally dense ground-model set, and use to exclude the incompatible part.
Choose the witnessing . Since and , upward closure gives . The assumed equality truth lemma gives , while gives . Combining both directions,This completes the atomic membership truth lemma for forcing; no separate assumption of the membership truth lemma was made.
We prove power set in a generic extension by bounding possible subnames in the ground model, rather than presupposing the desired power set in . Let , and let . In formEvery is a forcing name. Its value is a subset of : an active pair has for some , so implies and .
Now take any with , and choose a forcing name with . By axiom schema of separation and definability of the syntactic forcing relation,The atomic membership truth lemma for forcing shows . One inclusion follows immediately from its soundness direction. For the other, if , choose with and . The truth direction supplies forcing ; strengthen within below and to obtain an active pair in representing .
Finally the ground-model forcing nameexists by Axiom schema of replacement and the ground-model power set axiom. Since is nonempty, all contribute their values, andThis set belongs to by the definition of a generic extension. The construction uses all conditions in the outer pairs and therefore does not require a greatest condition in .
For the product forcing order, let and be the coordinate projections of :These are nonempty upward-closed, directed filters in an ordered set. Clearly . If and , choose and . Directedness supplies below both, so . Upward closure of gives . Therefore the projection of a product-generic filter satisfiesNo greatest conditions in the factors are required for this argument.
Let be a dense subset of a forcing order . Then is dense in the product forcing order: below , choose in and retain . The generic filter meets it, so its first projection meets . Together with the filter properties proved above, this givesThe same argument proves that is -generic over , but genericity over the larger generic extension needs the next argument.
We prove mutual genericity for product forcing. Let be a dense subset of , and take a forcing name evaluating to . By the forcing theorem, some forces that is a dense subset of the canonical forcing name for .
In defineThis set is dense in the product forcing order. Given , the incompatible case is immediate. Otherwise first strengthen below . The forced density assertion and the existential clause of syntactic forcing supply a further and a ground-model with . To justify choosing a ground-model , a name forced to lie in can densely be made equal to some by the atomic membership clause; strengthen to that equality and use the forced order comparison. Thus lies below .
The generic filter meets . It cannot meet the first part, because its first projection contains and is directed. Hence there is with and . Soundness of the forcing theorem gives , and the projection gives . Since every such is met,This establishes the stronger property, rather than merely meeting dense ground-model subsets.
A forcing atom is a condition such that any two strengthenings of are compatible forcing conditions:An atomless forcing order has no such condition; equivalently,The meaning of is that there is no common stronger condition. For an arbitrary partial order, an atom need not be a minimal element: the definition concerns compatibility below it. This distinction prevents a minimal-element definition from misclassifying an order with descending but mutually compatible conditions.
The two-argument version of Fn forcing consists of finite partial functions:Thus a stronger condition specifies more values. The empty partial function is the greatest condition. Two conditions are compatible forcing conditions exactly when they agree on their common domain; if they do, their set union is a common strengthening. This is in the three-argument convention for Fn forcing. If or is empty, only the empty condition exists. For infinite and at least two elements in , assigning two different values at a fresh coordinate proves that this is an atomless forcing order.
Suppose, towards a contradiction, that . Then is a ground-model set by axiom schema of separation. It is dense. If , it already lies in . If , atomless forcing order structure gives incompatible forcing conditions . Both cannot belong to the directed filter , so at least one is a strengthening of in .
All compatibility and extension quantifiers range over the same ground-model set , so this density argument is also valid internally in the transitive model . Genericity requires , contradicting the definition of . Therefore a generic filter for an atomless order is new:The assumption is essential: a forcing atom determines a ground-model generic filter. For an atom , the conditions compatible with form a generic filter : two such conditions have strengthenings below , which have a common strengthening by the atom property; every dense set has a member below . In a general partial order, need not be the principal filter above .
Put and let . Conditions from Fn forcing agree on common coordinates because is directed, so is a function. For each , the ground-model setis dense: add a value at that coordinate if necessary. The generic filter meets all these sets, making total.
For distinct , the ground-model setis dense. Choose fresh for both rows of a finite condition and assign and there. Genericity therefore makes the rows pairwise different. The generic coordinate reals for finite-function forcing are , and in the generic extensionThe family is a set in , for example by collecting the ground-model names and evaluating the corresponding name for their indexed family. This argument only needs as the specified ground-model ordinal; it does not silently assume a cardinal preservation by chain-condition forcing result.
The Rasiowa–Sikorski lemma constructs a generic filter over each . Every resulting generic extension remains a countable transitive model of ZFC: there are only countably many ground-model names externally. The order has the same elements and ordering at every stage, and atomless forcing order structure is absolute because all its quantifiers are bounded to . Hence the generic filter for an atomless order is new result gives for every .
The increasing union is transitive and contains . If it satisfied Axiom of power set for , there would be a set withChoose with . The next-stage generic filter belongs to and is an actual subset of . This subset assertion is absolute for the transitive set , so . Transitivity of and then give , a contradiction. Thus the power-set failure in an increasing union of generic extensions occurs already at the fixed ground-model order:The stages form an increasing chain, not an elementary chain, so the elementary chain theorem does not assert ZFC for their union.
Articles by others on the same topic
There are currently no matching articles.