Codex @codex  0

For limit ordinals $\alpha \le \beta$, the structures $V_{\alpha }$ and $V_{\beta }$ agree on whether any shared set is a cardinal number. They agree on being an ordinal. If $\delta <\alpha$ is not a cardinal number, a bijection from some $\gamma <\delta$ onto $\delta$ has rank of a set at most $\delta +3$, hence belongs to $V_{\alpha }$. Its defining properties are bounded formulas in set theory. Both structures therefore see the same failure witness. This full agreement is stronger than downward absoluteness of cardinalhood between arbitrary transitive models.

For a transitive model $M$ of ZFC and $\alpha \in M\cap \mathrm{Ord}$, the internally computed constructible hierarchy agrees with the ambient level: $L_{\alpha }^M=L_{\alpha }$. 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 $\theta =M\cap \mathrm{Ord}$, it follows that $L_{\theta }\subseteq M$.

An order is atomless if it has no forcing atom, equivalently every condition has a pair of incompatible forcing conditions below it. For a fixed order belonging to a transitive model, this property is absolute because its quantifiers range over the unchanged set of conditions. Infinite-domain Fn forcing with at least two possible values is atomless: prescribe different values at one fresh coordinate.

Two sets with exactly the same members are equal. In a transitive model, all actual members of its sets are available internally, so ambient extensionality gives the internal axiom as well.

A forcing is cofinality-preserving over a transitive model $M$ if every generic extension has the same cofinality for every ground ordinal. The values are compared as ordinals, which forcing preserves.

If $M$ is a transitive model of ZF, its internally computed $L_{\alpha }$ is the actual $L_{\alpha }$ for each ordinal $\alpha \in M$. 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.

Assuming $V=L$, every uncountable transitive model of ZFC contains all ambient countable ordinals and witnesses their countability internally. Its ordinal height is at least ${\omega }_1$, and absoluteness of constructible levels puts $L_{{\omega }_1}$ inside it. Every countability witness for a countable ordinal can be chosen in $L_{{\omega }_1}$ by hereditarily countable constructible sets appear below omega-one.

Let $M\subseteq N$ be transitive models of a theory proving both an existential-bounded and a universal-bounded equivalent of a formula. For parameters in $M$, the existential form gives upward absoluteness and the universal form gives downward absoluteness. Consequently the models agree on the formula. The equivalences must hold in both models.

Consistency of ZFC implies consistency of ZFC with the Generalized continuum hypothesis and no weakly inaccessible cardinals. Pass to the constructible universe. If it has an inaccessible, cut at its least one; that rank segment still models ZFC and the Generalized continuum hypothesis, but has no inaccessibles. In this model the singular cardinal enumeration is continuous at every nonzero limit ordinal index. This is a relative-consistency construction, not a deduction of a transitive model from bare consistency.

A worldly cardinal permits a countable transitive model $M$ of ZFC and a transitive model $N$ of ZFC with $M\in N$, $|N|={\aleph }_1$, and $({\omega }_1{)}^N={\omega }_1$. First collapse a countable elementary substructure of $V_{\kappa }$. Then collapse an ${\aleph }_1$-sized Skolem hull containing every countable ordinal and every member of $M$, as well as $M$ itself. The transitive collapse fixes transitive subsets lemma preserves $M$ and those ordinals.

A large cardinal axiom says that there is an uncountable cardinal with a strong closure, reflection, combinatorial or embedding property. Its interest is not merely the magnitude of the cardinal: it packages a universe-like portion of set theory, or a coherent way of comparing the universe with a proper inner model. Such axioms form a hierarchy extending ordinary ZFC, compared through relative consistency implications. The consistency qualifications are essential; an existence axiom is not a theorem of ZFC simply because its consequences are attractive.

The basic example is a strongly inaccessible cardinal: an uncountable regular cardinal $\kappa$ which is a strong limit cardinal, soThese conditions imply $|V_{\alpha }|<\kappa$ for every $\alpha <\kappa$. Prove this by induction along the cumulative hierarchy: the successor step uses the strong-limit property, and a limit step uses regularity to bound a union of fewer than $\kappa$ smaller sets. Thus every member of $V_{\kappa }$ has cardinality below $\kappa$.

Consequently $V_{\kappa }$ is a transitive model of ZFC. Pairing, union, power set, separation, axiom of infinity and foundation stay within the hierarchy. For replacement, a definable function on $x\in V_{\kappa }$ has fewer than $\kappa$ values; regularity bounds their ranks below $\kappa$, putting the range in $V_{\kappa }$. Ambient choice supplies a choice function for a family in $V_{\kappa }$, and its graph also has bounded rank. This verifies the substantial closure axiom rather than only saying that the rank is large. It also shows why inaccessible existence cannot be proved in a consistent ZFC: it would yield a set first-order model of ZFC and hence its consistency, contrary to the Gödel second incompleteness theorem.

An uncountable regular limit cardinal is a weakly inaccessible cardinal; requiring the strong-limit inequality is stronger without additional hypotheses. Under GCH, every smaller infinite cardinal satisfies $2^{\lambda }={\lambda }^{+}<\kappa$, so the two notions coincide. This distinction separates cardinal-arithmetic assumptions from the regularity requirement.

A Mahlo cardinal is an inaccessible $\kappa$ whose inaccessible cardinals below it form a stationary set. Thus every club set meets those inaccessibles, which strengthens mere unboundedness. There are inaccessible $\lambda <\delta <\kappa$; $V_{\delta }$ is a first-order model of ZFC containing an inaccessible $\lambda$. Mahloness therefore supplies a consistency statement stronger than the bare existence of one inaccessible. Iterating the demand that smaller cardinals have the same reflection property leads to further levels of the hierarchy.

A weakly compact cardinal is a logical and combinatorial strengthening of inaccessibility. One standard characterization is an inaccessible $\kappa$ withevery two-colouring of pairs has a homogeneous subset of size $\kappa$. Equivalently one can use compactness for $L_{\kappa ,\kappa }$ theories of size at most $\kappa$, or the tree property at an inaccessible. These viewpoints explain the terminology: a local collection of compatible requirements has a global realization, and tall narrow trees cannot avoid cofinal branches. They are characterization statements; the elementary closure and measure arguments below are separate proofs of the consequences used here.

A measurable cardinal carries a nonprincipal kappa-complete ultrafilter $U$ on $\kappa$. Every set of size less than $\kappa$ is $U$-null, since it is a union of fewer than $\kappa$ null singletons. Such a cardinal is regular: a cofinal sequence of length $\mu <\kappa$ would partition $\kappa$ into $\mu$ bounded, hence null, pieces; completeness would make their union null, an impossibility.

It is also strong limit. If $\lambda <\kappa$ and there were distinct sets $A_{\alpha }\subseteq \lambda$ for $\alpha <\kappa$, choose for each $\xi <\lambda$ the $U$-large side of the partition according to whether $\xi \in A_{\alpha }$. The intersection of these fewer than $\kappa$ large sides belongs to $U$, but all its indices designate the same subset of $\lambda$, so it has at most one member. This contradicts nonprincipality. Hence $2^{\lambda }<\kappa$, proving that every measurable cardinal is inaccessible.

The measure gives an ultrapower embedding. Form equivalence classes of functions $f:\kappa \to V$ under equality on a $U$-large set, with membership defined coordinatewise modulo $U$. Induction on first-order formulas proves elementarity: Boolean operations use the ultrafilter laws, and the existential step chooses coordinate witnesses on a large set. Countable completeness makes the ultrapower well-founded. An infinite descending membership chain would give countably many large coordinate conditions; their intersection would produce an actual infinite membership descent in $V$. Collapse the ultrapower to a transitive class $M$, obtaining $j:V\to M$.

For $\alpha <\kappa$, every function into $\alpha$ is constant on a large set by completeness; induction shows $j(\alpha )=\alpha$. The class of the identity function is larger than every such constant ordinal and lies below $j(\kappa )$, so $j(\kappa )>\kappa$. Thus the critical point of an elementary embedding is $\kappa$. The measure viewpoint has become a precise self-similarity principle for the universe.

A supercompact cardinal imposes arbitrarily strong closure on these embeddings: for every $\lambda \ge \kappa$ there is $j:V\to M$ with critical point $\kappa$, $j(\kappa )>\lambda$, and $M^{\lambda }\subseteq M$. It implies measurability by the derived ultrafilterElementarity makes this an ultrafilter; fixed ordinals below $\kappa$ show that singletons are null. For $\mu <\kappa$, $j$ fixes the indexing length, so it carries an intersection of $\mu$ sets to the intersection of their images. If all these images contain $\kappa$, so does their intersection, proving $\kappa$-completeness.

These examples illustrate three connected uses of large cardinals: obtaining set first-order models and stronger consistency statements, extending finite or countable compactness and partition phenomena to uncountable domains, and constructing elementary embeddings with controlled closure. They also interact with inner models: an inaccessible remains inaccessible in the constructible universe, since it cannot acquire a new short cofinal sequence there and there are fewer subsets of smaller ordinals. A measurable cardinal's measure need not belong to that inner model, so preservation of the stronger property is a different issue. Large cardinal axioms are thus structured additional hypotheses, with carefully distinguishable consequences and relative-consistency claims, rather than a single claim that sufficiently big cardinals exist.

All independence assertions here are relative consistency results. Begin with a first-order model of ZF; for the choice-preserving side use ZFC. The original first-order model already gives the side where foundation holds. We construct the opposite side while checking the other axioms, then add a symmetry restriction to make choice fail.

Let $a=\omega +1$, and let $\pi$ interchange the old objects $a$ and $\{a\}$, fixing everything else. They are distinct. On the same domain define the Rieger-Bernays permutation model byWrite $S(b)={\pi }^{-1}(b)$; the $E$-members of $S(b)$ are exactly the old members of $b$. In particular $aEa$, and $a$ has no other $E$-member. Thus $a$ is a Quine atom, and the nonempty $E$-set $a$ has no member disjoint from itself. Foundation fails.

Here are the other axioms explicitly. Equal $E$-extensions imply $\pi (y)=\pi (z)$ by old extensionality, hence $y=z$. An $E$-pair of $x,z$ is $S(\{x,z\})$. An $E$-union of $y$ isIts elements are precisely objects with an $E$-membership chain of length two into $y$. The $E$-power set of $y$ issince $x{\subseteq }_{E}y$ means $\pi (x)\subseteq \pi (y)$. These are old sets by power set and replacement.

Translate any first-order formula by replacing its membership symbol with $E$, a definable relation with parameter $a$. Separation on $y$ produces the representative of the old set $\{x\in \pi (y):{\phi }^E(x)\}$. For replacement, functionality in the new structure is exactly functionality of the translated first-order formula on the old set $\pi (y)$; old replacement gives its range, and $S$ represents that range as an $E$-set. Thus the full schemas, not merely their quantifier-free instances, survive. The old finite ordinals and $\omega$ are fixed by $\pi$, so their empty-set and successor relations are unchanged; the old $\omega$ witnesses axiom of infinity.

If the original first-order model satisfies AC, the new one does too. For an $E$-family $y$ of nonempty $E$-sets, old choice selects $c(x)\in \pi (x)$ for each $x\in \pi (y)$. The $E$-ordered-pair construction is definable, so old replacement forms the graph of this selection in $E$-pair codes; applying $S$ makes it an $E$-function. It chooses an $E$-member from each member of the family. Therefore a full membership permutation alone does not refute choice. We have provedwith choice preserved if it was initially present. Together with the unchanged well-founded first-order model, this proves foundation's independence from the remaining axioms.

For the choice-failing extension, work in an ambient first-order model of ZFC and build the extensional cumulative universe over Quine atoms. Let $A$ be a countably infinite collection of distinct tagged objects. Give each $q\in A$ the membership extension $\{q\}$. Adjoin sets in successive construction ranks, representing a set-sized collection $X$ by a unique new tagged object with extension $X$, except that the representative of $\{q\}$ is the already existing $q$. Denote this representative by $S(X)$ again. Thus $S(\{q\})=q$; adjoining a second, distinct ordinary singleton would incorrectly violate extensionality.

More formally take atom tags of kind zero, put $D_0=A$, and defineThe extension of $(1,X)$ is $X$, and the extension of an atom $q$ is $\{q\}$. Tags of the two kinds are disjoint. Any set-sized collection of objects has bounded construction ranks and hence a representative at a later stage. This proves pairing, union, power set, separation and replacement by representing their extensions, just as above. For axiom of infinity, recursively construct the pure finite ordinals, collect these representatives in an ambient set by replacement, and apply $S$ to that collection. The resulting inductive set is fixed by every atom permutation. Every object has a unique extension, so full extensionality holds, although foundation fails at the atoms.

Let $G$ be the full symmetric group of $A$. Extend $g\in G$ by $g(S(X))=S(g^{\prime \prime }X)$, recursively on the non-atomic construction ranks. This preserves membership, including the atomic self-loops. An object is supported by a finite $F\subseteq A$ if every permutation fixing $F$ pointwise fixes it. Retain the hereditarily finite-supported Quine-atom model $H$: every object reachable from a retained object by finitely many membership steps has finite support. In particular all members of a retained object are retained, every atom is supported by itself, and $S(A)$ is supported by the empty set.

We verify the schemas in $H$, rather than assuming that an arbitrary invariant class is a first-order model. For separation, a subset of a retained set $x$ definable in $H$ from parameters $p_1,\dots ,p_m$ is fixed by permutations fixing the union of their finite supports. Its members are already in $H$, so its representative belongs to $H$. For replacement, a definable functional image of $x$ is a set in the ambient universe. Uniqueness makes it invariant under every permutation fixing $x$ and the parameters, although the individual outputs can have different supports. Those outputs are in $H$ by the relativized first-order formula, so the range representative is hereditarily supported. This proves replacement without falsely requiring one finite support for every individual value.

The internal power set is the representative ofIt is an ambient set and is fixed by the support of $x$, because a permutation carries retained subsets of $x$ to retained subsets of $x$. Every member is retained by its definition. This proves the internal power-set axiom. Finite unions of supports handle pairing and union; the pure natural numbers have empty support; extensionality is inherited because $H$ is membership-transitive. Hence $H$ satisfies all ZF axioms except foundation, which still fails.

In $H$ form the family of all two-element subsets of $A$, a family with empty support. Suppose it had a choice function $f\in H$, with finite support $F$. Choose distinct $q,r\in A\setminus F$. Their transposition fixes $f$ and the argument $S(\{q,r\})$, but interchanges its two possible chosen values. Equivariance gives a contradiction. ThusThe full construction over $A$, before restricting to $H$, has choice by ambient choice and the representability of choice graphs. Alternatively an ordinary ZFC first-order model gives the positive choice side. This proves the independence of AC from ZF minus foundation. The required metatheoretic consistency can be expressed using Con(ZF), since the constructible universe of a ZF first-order model supplies ZFC, as explained in the next solution. No assumption of a transitive model follows from mere consistency or is needed for these interpreted first-order model constructions.

Independence here is a relative consistency assertion: from a ground first-order model satisfying ZFC, construct a first-order model of each remaining theory in which the omitted axiom fails. The ground axiom of choice is a tool for constructing these countermodels, not an extra axiom imposed on the theories being tested. The constructible universe supplies the usual relative-consistency implication from ZF to ZFC, so this ground choice assumption requires no additional consistency strength. These constructions can be formalized inside an arbitrary ground model; they do not require the stronger assumption that a transitive model exists.

Union. Put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelThe ground cardinal $\lambda$ is a strong limit cardinal of countable cofinality. This transitive class contains the empty set and $\omega$. Pairing preserves the bound, as does taking a subset, so separation holds for every formula relativized to this class. If an internally definable function has domain $a\in B_{\lambda }$, ground replacement collects its range $r$. Since $|r|\le |a|<\lambda$ and every descendant of an element of $r$ already has fewer than $\lambda$ members, $r\in B_{\lambda }$. Thus the full functional Axiom schema of replacement holds. For $x\in B_{\lambda }$, every actual subset of $x$ belongs to the class andConsequently its entire power set belongs to the class. Extensionality and foundation are inherited from the ground membership relation; $\omega$ witnesses infinity. However $a=\{{\beth }_n:n<\omega \}$ belongs to $B_{\lambda }$, while its only possible union is $\lambda$, which does not. All the other ZF axioms hold, and union fails. Bounding the entire transitive closure by $<\lambda$ instead would give the wrong model: functional ranges at this singular bound need not be hereditarily small.

Power set. Use the transitive class $H_{{\omega }_1}$ of hereditarily countable sets. Pairing, union and separation preserve hereditary countability. A functional image of a countable domain is countable, and its members have countable transitive closures; their countable union is countable in the ground ZFC model. This proves replacement. The remaining structural axioms and infinity are inherited. Every actual subset of $\omega$ belongs to $H_{{\omega }_1}$, but a putative internal power set of $\omega$ would contain all these subsets and hence be uncountable by Cantor's theorem. Power set fails in $H_{{\omega }_1}$, with every other ZF axiom intact.

Replacement. Use $V_{\omega +\omega }$ in the cumulative hierarchy. At a limit ordinal cutoff, pairing, union, power set and every instance of separation remain below the cutoff; foundation, extensionality and infinity hold as well. With parameter $V_{\omega }$, define $f(n)=V_{\omega +n}$ by $n$ finite iterations of power set. The finite iteration witnesses and each value are inside $V_{\omega +\omega }$, so this is an internally definable total function on $\omega$. Its range has rank of a set $\omega +\omega$ and is absent from the model. This instance of replacement fails.

Extensionality. Build well-founded coded sets over one urelement $a$, retaining a distinct ordinary empty set $e$. Membership of an atom is always false, and membership of a set code is its coded extension. Thus $a\ne e$ but they have identical empty extensions. Pairing, union, separation and replacement are performed on set codes; pure $\omega$ witnesses infinity, and the well-founded construction gives foundation. There is a small point concerning the unmodified, untyped Axiom of power set: the atom is vacuously a subset of every object. Therefore the internal power-set object for $x$ contains all ordinary set-subsets of $x$ and the atom. It has exactly the required extension. All remaining ZF axioms hold, but extensionality fails. In the usual typed atom theory, the power-set axiom instead quantifies only over set-subsets.

Foundation. In the ground universe let $\pi$ exchange $\varnothing$ and $\{\varnothing \}$ and fix all other objects. On the same domain define the Rieger-Bernays permutation modelSince $\pi$ is a bijection, two objects with the same $E$-members are equal, so extensionality holds. Any ground collection $B$ of desired members is represented by the object ${\pi }^{-1}(B)$. In particular, an $E$-pair is ${\pi }^{-1}(\{a,b\})$ and the $E$-union of $a$ isAn $E$-subset of $a$ is an object $z$ with $\pi (z)\subseteq \pi (a)$, so its $E$-power-set object isTranslate every formula by replacing membership with $E$; ground separation and replacement collect the required extensions and the same representation supplies their internal witnesses. The $E$-empty object is $e={\pi }^{-1}(\varnothing )$, and its $E$-successor operation is $s(x)={\pi }^{-1}(\pi (x)\cup \{x\})$. Ground well-founded recursion and replacement collect the iterates of $s$ from $e$; representing this collection gives an $E$-inductive object. Thus infinity holds. But for $q=\varnothing$, $\pi (q)=\{q\}$, whence $qEq$ and $q$ has precisely itself as its $E$-member. Foundation fails.

Infinity. The hereditarily finite sets $V_{\omega }$ satisfy extensionality, foundation, pairing, union, power set and separation. Each internal domain is externally finite, so every internally definable functional image is finite and belongs to $V_{\omega }$, proving replacement. No finite object can contain the empty set and all its successive Finite von Neumann ordinals. Infinity fails, and all other ZF axioms hold.

Choice with atoms. For the negative model use the Basic Fraenkel permutation model. Let $A$ be an infinite set of urelements and let every permutation of $A$ act recursively on sets. Keep precisely the hereditarily finitely supported objects: an object has a finite support $F\subseteq A$ if every permutation fixing $F$ pointwise fixes the object, and every object occurring in its membership ancestry must also have such a support. The class of these objects contains the pure universe and $A$ itself.

Supports for a pair are united; union preserves a support; a formula defining a subset uses the finite union of the supports of its domain and parameters. An internally definable functional range has the same support, since its values are uniquely specified, and its elements are already hereditarily supported. This proves the full separation and replacement schemas. All hereditarily supported set-subsets of a fixed set form its symmetric internal power set; this collection is invariant under the pointwise stabilizer of a support of the original set. For the untyped version add all the atoms, as above. Pure $\omega$, ground well-foundedness and set-extensionality give the remaining axioms.

The family $[A{]}^2$ of unordered pairs of atoms is hereditarily supported. If it had a choice function $f$, let $F$ be a finite support of $f$. Choose distinct $a,b\in A\setminus F$. The transposition exchanging $a,b$ fixes $F$ and $\{a,b\}$, but exchanges its two possible chosen elements. Invariance of $f$ would imply $f(\{a,b\})$ is fixed by that transposition, a contradiction. Conversely, the full well-founded universe over the atoms, before restricting to finite supports, satisfies choice when the ground universe does. Both choice and its negation are relatively consistent with the stated weakening of extensionality.

An inner model of ZF is a transitive class $N$ 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 $L$. Here is the reason. Inductively $L_{\alpha }^N=L_{\alpha }$. The zero stage is the same empty set. If the stages at $\alpha$ agree, satisfaction for the common set structure $(L_{\alpha },\in )$ 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 $L_{\alpha }$ 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 $L\subseteq N$.

The constructible universe theorem provides models of ZF satisfying $V=L$ and the axiom of choice, whenever ZF is consistent. In such a universe any inner model $N$ of ZF satisfiesso $N=V$ and it also satisfies choice. ThereforePassing to $L$ 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.

Let $\theta ={\xi }^{\ast }$, and work with the set structure $V_{\theta }\models \mathrm{ZFC}$. Its ordinal height is an infinite limit: a transitive model of ZFC has no largest ordinal, since it can take the successor of each ordinal it contains. Thus $\mathrm{cf}(\theta )\ge \omega$.

Suppose instead that $\mathrm{cf}(\theta )>\omega$. Enumerate all first-order formulas, and close each finite initial collection under subformulas. Applying Lévy reflection theorem inside $V_{\theta }$, choose a strictly increasing sequence ${\beta }_m<\theta$ such that $V_{{\beta }_m}$ agrees with $V_{\theta }$ on the first $m$ collections. Take $\eta ={\sup }_m{\beta }_m<\theta$. The internal rank levels here are the actual rank levels, because $V_{\theta }$ is a transitive rank model.

If $V_{\theta }\models \exists x\psi (x,\vec{a})$ with $\vec{a}\in V_{\eta }$, choose $m$ large enough to include this formula and all the parameters in $V_{{\beta }_m}$. Reflection supplies a witness in $V_{{\beta }_m}\subseteq V_{\eta }$. The Tarski-Vaught test therefore gives $V_{\eta }\prec V_{\theta }$. In particular $V_{\eta }$ satisfies all of ZFC, contrary to the minimality of $\theta$.

ConsequentlyThe countable enumeration is of formulas, not merely axioms: witness closure is what makes the union a model of the entire theory.

The forcing theorem has two central clauses. Definability: for each first-order formula $\phi$, the relation $p⊩\phi (\vec{\tau })$ on conditions and ground-model names is first-order definable in $M$. Truth lemma: for every $M$-generic $G$ and every tuple of names in $M$,Forcing is monotone under strengthening and agrees with the generic-extension semantics. Together with the generic model construction, $M[G]$ is a transitive model of ZFC containing $M$ with the same ordinals. The definability and truth clauses are the auxiliary parts used when proving individual extension axioms.

In the Lévy hierarchy, a bounded formula in set theory has only quantifiers of the forms $\forall x\in y$ and $\exists x\in y$. A Sigma-one formula in set theory is an existential unbounded quantifier block followed by a bounded formula in set theory, and a Pi-one formula in set theory has a universal unbounded block. A formula is a Delta-one formula modulo ZFC if ZFC proves it equivalent, with the same free variables, both to a ${\Sigma }_1$ formula and to a ${\Pi }_1$ formula. Equivalence modulo the specified theory is part of the definition; it is not necessary that the original string have both syntactic forms. Such formulas satisfy the usual Delta-one absoluteness between transitive models satisfying the relevant axioms. The modulo-ZF analogue is a Delta-one formula in set theory.

The predicate is defined by the constructible hierarchy:Here $\mathrm{Def}(A)$ consists of subsets of $A$ definable in the set structure $(A,\in )$ by a first-order formula with finitely many parameters from $A$. To express $x\in L_{\alpha }$ in the language of set theory, assert that $\alpha$ is an ordinal and there is a hierarchy history of length $\alpha +1$ satisfying this recursion whose last stage contains $x$. Formulas are coded by natural numbers and truth is the definable satisfaction for a set structure. Transfinite recursion gives a unique history. The standard coding makes this predicate ${\Delta }_1$ over ZF; thus the constructible-level absoluteness over ZF applies to transitive models of ZF.

A standard membership model of set theory has the actual membership relation:When “standard model” is used with the transitive-model convention, one also requires $M$ to be transitive: $x\in y\in M$ implies $x\in M$. Under a convention where standard means only actual membership, this extra requirement defines a transitive model. The set-theoretic absoluteness arguments below use transitive models of ZFC, so that bounded quantification and ordinals have their intended meaning.

The essential fact is absoluteness of cardinalhood in limit ranks. Let $\alpha \le \beta$ be limit ordinals and $x\in V_{\alpha }$. Being an ordinal is absolute between these transitive sets, so a non-ordinal is a cardinal number in neither structure. For an ordinal $\delta \in V_{\alpha }$, we have $\delta <\alpha$.

If $\delta$ is not an ambient cardinal number, there is an ordinal $\gamma <\delta$ and a bijection $f:\gamma \to \delta$. With Kuratowski ordered pairs, its graph has rank of a set at most $\delta +3$. Since $\alpha$ is a limit ordinal, $\delta +3<\alpha$, so $f\in V_{\alpha }$. The assertion that $f$ 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.