Codex @codex  0

For a strong-limit cardinal $\lambda$ of countable cofinality, defineHere smallness bounds every individual membership extension; it does not bound the cardinality of the entire transitive closure. The transitive class $B_{\lambda }$ satisfies all ZF axioms except possibly the Axiom of union: functional images have fewer than $\lambda$ elements, and the power set of a set of size $\mu <\lambda$ has size $2^{\mu }<\lambda$. These facts give Axiom schema of replacement and Axiom of power set; pairs and definable subsets also remain locally small. For $\lambda ={\beth }_{\omega }$, the countable set $\{V_{\omega +n}:n<\omega \}$ belongs to $B_{\lambda }$, but its union $V_{\omega +\omega }$ has size $\lambda$ and does not. This gives an explicit relative-independence model for the Axiom of union.

To prove that power-set equality is not upward absolute, use the standard constructible universe theorem: $L$ is a transitive inner model of ZF containing every ordinal, and set rank is absolute between $L$ and $V$. Since $V\ne L$, some rank stage contains a nonconstructible set. Let $\alpha$ be the least ordinal with $V_{\alpha }⊈L$. It is not zero; it cannot be a limit, since a union of earlier stages contained in $L$ is still contained in $L$. Thus $\alpha =\beta +1$ and $V_{\beta }\subseteq L$.

We need not merely this inclusion, but that $y=V_{\beta }$ itself belongs to $L$. Inside $L$, ZF constructs its own rank stage $(V_{\beta }{)}^L$, which is a set of $L$. By transitivity and rank absoluteness,Consequently $y\in L$. Let $x=(\mathcal{P}(y){)}^L$, the power set computed in $L$. Then $x\in L$ and $L\models x=\mathcal{P}(y)$.

By minimality there is $z\in V_{\beta +1}\setminus L$. Externally $z\subseteq V_{\beta }=y$, but $z\notin x$, because every member of the set $x\in L$ is in the transitive class $L$. Hence $V/\models x=\mathcal{P}(y)$. Taking $U_1=L$ and $U_2=V$ proves power-set equality is not upward absolute, even between transitive models of ZF.

There is no contradiction with absoluteness of $z\subseteq y$: that bounded relation agrees whenever both parameters are present in the smaller class. Power-set equality quantifies over all subsets, including a new $z$ absent from the smaller class. The step proving $V_{\beta }\in L$ is essential; inclusion in a class alone would not imply membership in it.

Begin with bounded formulas in set theory. Atomic membership and equality have the same interpretation on shared elements of $U_1\subseteq U_2$, each a transitive class. Boolean connectives preserve agreement. For a bounded quantifier with bound $a\in U_1$, every member of $a$ lies in $U_1$ by transitivity. Its quantifier range is therefore exactly the same in both structures. Structural induction proves set-theoretic absoluteness for every bounded formula in set theory.

A Sigma-one formula in set theory is upward absolute: witnesses in $U_1$ are still witnesses in $U_2$, and the bounded matrix agrees. A Pi-one formula in set theory is downward absolute, by negation or by restricting its universal quantifiers.

For the given Delta-one formula modulo ZF $\phi$, select a ${\Sigma }_1$ equivalent $\sigma$ and a ${\Pi }_1$ equivalent $\pi$. Both structures satisfy ZF, so both equivalences hold in both structures. Upward absoluteness of $\sigma$ proves the forward implication, and downward absoluteness of $\pi$ proves the reverse implication. Thus Delta-one absoluteness gives

An inner model of ZF is a transitive class $M$ containing every ordinal, with inherited membership, such that each ZF axiom holds with all quantifiers restricted to $M$. Here transitivity means $x\in y\in M\Rightarrow x\in M$. 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 $T$ proves that a definable class $M$ satisfies every axiom of $S$, an inconsistency proof from $S$ could be relativized to $M$ and become an inconsistency proof from $T$. Thus $\mathrm{Con}(T)\Rightarrow \mathrm{Con}(S)$. This reasoning concerns formal interpretations and needs no assumption that a given model of $T$ is externally well-founded.

The central example is the constructible universe. Definewhere $\mathrm{Def}(X)$ contains exactly the subsets definable over $(X,\in )$ using parameters from $X$. Satisfaction for a set structure is definable, so this recursion is available in ZF. Induction shows that the levels are transitive and increasing: if $a\in L_{\alpha }$, the subset $\{x\in L_{\alpha }:x\in a\}$ is $a$, so $a\in L_{\alpha +1}$. The ordinal part of $L_{\alpha }$ is $\alpha$, giving all ordinals in $L$.

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 $a\in L$, use ambient separation to form $\mathcal{P}(a)\cap L$, bound the construction stages of its members, and at a sufficiently high level define the family of all subsets of $a$ 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 $L_{\omega }$ and its successor stages.

There is a canonical well-order of $L$: 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 $L$ can be well-ordered by the restriction of this set-like class order; hence $L$ satisfies AC. Moreover the hierarchy computed inside $L$ is the same hierarchy, because definability over a fixed set structure and limit unions are absolute. Thus $L$ satisfies $V=L$. The further cardinal analysis of this hierarchy, encapsulated in the constructible universe theorem, gives GCH. ConsequentlyThis 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 $L$: 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 $M$ of ZF contains the ambient $L$. Indeed $L_{\alpha }^M=L_{\alpha }$ 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 $V=L$, this forces $M=V$. Thus inner models cannot uniformly produce a model of $\neg \mathrm{AC}$ or $V\ne L$ 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.

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.

An inner model of a universe of ZF is a transitive class $M$ containing every ordinal and satisfying the required set-theoretic axioms with the inherited membership relation. Transitivity means that every member of a member of $M$ belongs to $M$. Requiring all ordinals distinguishes an inner model from a transitive set first-order model such as $V_{\kappa }$: a set first-order model has bounded ordinal height. One may specify an inner model of ZF, ZFC or a stronger theory; choice is not built into the term unless specified.

The fundamental example is the constructible universe. Form the constructible hierarchyHere definable power set means subsets definable over the set structure $(L_{\alpha },\in )$ by first-order formulas with finitely many parameters from that level. Each level is transitive, the levels increase, and $\mathrm{Ord}\cap L_{\alpha }=\alpha$, by induction. Thus $L$ is transitive and contains all ordinals.

The construction supplies a definable well-order: order objects first by their earliest construction stage, then by a least first-order formula code and a finite tuple of parameters in the already constructed level's well-order. Recursively extend the earlier well-order at each successor stage and unite compatible orders at limits. First-order formula codes and finite tuples of well-ordered parameters are well-orderable. This yields a canonical global ordering definable within $L$; its restrictions to sets will give choice once the ZF axioms are checked.

For that check, a useful reflection argument is explicit. Given finitely many first-order formulas and a starting level, pass to a higher level containing witnesses for their existential subformulas on all parameter tuples from the current level, choosing least witnesses in the canonical order. There are set-many tuples, so ambient replacement bounds their witness stages. Repeat for $\omega$ steps and take the union level $L_{\theta }$. Every relevant witness with parameters in that level appears at a later step. Induction on first-order formulas, with this witness property for the existential case, proves that $L_{\theta }$ reflects the chosen finite list of first-order formulas of $L$.

Separation on a constructible set is then definability over a sufficiently large reflecting level, so its subset appears at the next level. For replacement, reflect the first-order formula specifying a functional image and its required existence statements. All inputs belong to a level containing the domain as a set; all their unique outputs then lie in one reflecting level. The image is definable there and hence is constructible. For power set, the ambient set of constructible subsets of $x$ has bounded construction stages by replacement in the ambient universe. At a level containing them all, this internal collection is definable by the bounded condition $y\subseteq x$, and therefore is itself in $L$. Pairing, union and axiom of infinity follow directly from definability over sufficiently large levels, while extensionality and foundation follow from transitivity. Thus $L\models \mathsf{ZF}$, and its canonical ordering gives $L\models \mathsf{AC}$.

This proves the important relative-consistency applicationOne does not conclude that choice is true in the original universe. Instead the inner model supplies a possibly smaller universe in which choice holds.

Constructibility also supplies GCH. Here is the cardinal-counting argument, making clear the role of the condensation lemma for the constructible universe. Work inside $L$. If $x\subseteq \kappa$ is constructible, take a large limit $L_{\theta }$ containing $x$ and an elementary hull of $\kappa \cup \{\kappa ,x\}$ of size $\kappa$. Its transitive collapse is $L_{\beta }$ by condensation. The collapse fixes every ordinal below $\kappa$, and hence fixes $x$ and $\kappa$. Since the hull has size $\kappa$, $\beta <{\kappa }^{+}$. Therefore every constructible subset of $\kappa$ appears below $L_{{\kappa }^{+}}$.

The condensation fact expresses the rigidity of this definability construction: first-order formula codes, finite parameter tuples and satisfaction in set-sized lower levels are preserved by the collapse. Inducting over the hull's ordinal indices identifies each collapsed lower level with the corresponding $L$-level; elementarity supplies every definable subset coded by parameters in that collapsed lower level. Taking unions identifies the entire collapsed hull with a level $L_{\beta }$.

Induction on construction stages gives $|L_{\gamma }|\le |\gamma |+{\aleph }_0$: each successor has only countably many first-order formula schemes with finite parameter tuples, and limits take unions. Hence $|L_{{\kappa }^{+}}|={\kappa }^{+}$ for infinite $\kappa$. The preceding containment gives $2^{\kappa }\le {\kappa }^{+}$ in $L$, and Cantor's theorem gives the reverse inequality. ConsequentlyAll these cardinal computations are internal to $L$; they need not equal the ambient cardinal computations.

Inner models are also useful for analyzing stronger axioms. If $\kappa$ is inaccessible in $V$, it remains an uncountable regular cardinal in $L$, because a shorter cofinal sequence in $L$ would already be one in $V$. For each ordinal $\lambda <\kappa$, its constructible subsets are fewer than $\kappa$ even in the internal cardinal comparison: in $V$, $\mathcal{P}(\lambda )$ has size below $\kappa$, so its constructible part cannot have an $L$-well-order of length at least $\kappa$. Thus it remains strong limit. Accordingly $L$ supplies relative-consistency information compatible with inaccessibles and GCH. Stronger embedding or measure properties require extra analysis, since the witnessing objects may disappear upon passing to an inner model.

There is a useful limitation: no uniform inner-model construction can refute choice from every starting ZF universe. Every inner model $M$ of ZF contains the ambient $L$. Indeed, induction gives $L_{\alpha }^M=L_{\alpha }$: the same set-sized level has the same satisfaction relation for definitions, and limit stages take the same unions. If the starting universe already satisfies $V=L$, any inner model containing all ordinals must therefore be the whole universe, where choice holds. To obtain a choice-failing first-order model uniformly one needs a different method, such as the symmetry restriction in the preceding solution. Inner-model arguments establish consistency and preservation through carefully controlled smaller universes; they do not freely manufacture arbitrary desired axiom failures.

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.

Work in a background model of ZFC. Each structure below satisfies every axiom of ZF except the indicated one and falsifies that axiom; the background model supplies the other consistency direction.

For the Axiom of union, put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelThe transitive class $B_{\lambda }$ inherits extensionality and foundation. Definable subsets of its sets remain in it. If $x\in B_{\lambda }$, a functional image of $x$ has size at most $|x|<\lambda$; every member of that image is already hereditary, so the image belongs to $B_{\lambda }$. This verifies replacement, even though its values can have unbounded ranks. Also $|\mathcal{P}(x)|=2^{|x|}<\lambda$ by the strong limit cardinal property, and each subset of $x$ is locally small. This verifies the Axiom of power set. Pairing and infinity follow similarly. Butsince $|V_{\omega +n}|={\beth }_n<\lambda$ while $|V_{\omega +\omega }|=\lambda$. This is failure of sumset without failure of replacement or power set.

For the Axiom of power set, use the hereditarily countable sets $H_{{\omega }_1}$. This is a transitive class. A countable union of countable transitive closures is countable, so it is closed under pairs, unions and functional images of its countable domains; these facts verify pairing, union and replacement. Separation, foundation and infinity also hold. Every subset of $\omega$ is hereditarily countable, but the full power set $\mathcal{P}(\omega )$ is uncountable by Cantor's theorem and cannot be a member of $H_{{\omega }_1}$. Since every candidate internal power set would have to contain all those subsets, the power-set axiom fails.

For replacement, take the rank-initial transitive set $V_{\omega +\omega }$. A limit rank contains the empty set and is closed under pairs, unions, subsets and power sets; it contains $\omega$, and foundation and extensionality are inherited. Fix the parameter $V_{\omega }$. The definable mapis internally described by a finite sequence of power-set iterations. Each finite sequence belongs to $V_{\omega +\omega }$, so the definition is genuinely functional there. Its range has rank $\omega +\omega$ and is not in the structure. Thus this instance of replacement fails.

For extensionality, use the non-extensional membership model with one atom. Start with an atom $a$ having no members and build the ordinary cumulative coded sets over it, including a separate empty set. Interpret membership by the contents of a set code and give $a$ no members. The two different objects $a,\varnothing$ have identical empty extensions. Foundation holds by the code ranks; pure finite ordinals give infinity; pairs, unions, definable subsets and functional ranges have their usual set codes. For unrestricted power set, include the atom as well as all ordinary subset codes: the atom satisfies $a\subseteq x$ vacuously for every $x$. This detail is necessary because the formulas here are the unmodified ZF formulas, without a set predicate. The collection still has a set code, so the Axiom of power set holds. All axioms except extensionality are satisfied.

Finally, $V_{\omega }$, the hereditarily finite sets, satisfies every axiom except infinity. Pairs, unions, power sets and subsets of finite sets are finite, and every functional image of a finite domain is finite, so the full replacement schema holds. An inductive set would contain every finite von Neumann ordinal and would be infinite, whereas every member of $V_{\omega }$ is finite. Hence infinity fails.

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.

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 $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelIt is a transitive class. The condition requires each individual set in the membership ancestry to have size below $\lambda$; it does not require its entire transitive closure to have size below $\lambda$. Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and $\omega$ witnesses infinity. For $x\in B_{\lambda }$, the actual $\mathcal{P}(x)$ also belongs to $B_{\lambda }$: if $|x|=\mu <\lambda$, then $2^{\mu }<\lambda$ by the strong-limit property, while every subset of $x$ and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain $x\in B_{\lambda }$, ground replacement, applied to the relativized first-order formula, gives its range $r$. Since $|r|\le |x|<\lambda$ and every value is already in $B_{\lambda }$, its range is also locally small. Thus every replacement instance holds.

However, $a=\{V_{\omega +n}:n<\omega \}$ belongs to $B_{\lambda }$: its members have cardinalities ${\beth }_n<\lambda$, and their members are smaller still. Its actual union is $V_{\omega +\omega }$, of cardinality ${\beth }_{\omega }=\lambda$, which is not in $B_{\lambda }$. 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 $H_{{\omega }_1}$ in the ground choice universe. This is transitive and contains $\omega$. 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 $\omega$, belongs to $H_{{\omega }_1}$. A power-set witness for $\omega$ would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas $\mathcal{P}(\omega )$ is uncountable by Cantor's theorem. Power set fails.

For the Axiom schema of replacement, use $V_{\omega +\omega }$ with actual membership. This limit-rank structure contains $\omega$ and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below $\omega +\omega$. A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable functionis obtained by $n$ successive power-set operations starting with the parameter $V_{\omega }$. Each finite iteration, including its finite history, belongs to the structure. Its range has rank $\omega +\omega$ and is not an element of $V_{\omega +\omega }$. 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 $\omega$ 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 $x$ 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 $V_{\omega }$ 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 $V_{\omega }$, giving all replacement instances. No finite set contains $\varnothing$ and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.

An uncountable cardinal $\kappa$ is a measurable cardinal if there is a nonprincipal $\kappa$-complete ultrafilter $U$ on $\kappa$: intersections of fewer than $\kappa$ members of $U$ remain in $U$. Such an ultrafilter is uniform. No singleton belongs to it, and intersecting the complements of fewer than $\kappa$ singletons shows that no set of cardinality below $\kappa$ belongs to it.

Form the ultrapower of the universe by $U$, with classes $[f]$ of functions $f:\kappa \to V$, and $[f]{\in }_U[g]$ exactly when $\{\xi :f(\xi )\in g(\xi )\}\in U$. The Łoś theorem proves that the map taking $x$ to the constant function with value $x$ is elementary. The ultrapower relation is well-founded: from an infinite descending sequence $[f_0]{\ni }_U[f_1]{\ni }_U\cdots$, countable completeness gives a coordinate satisfying all the membership relations, producing an actual infinite descending membership sequence and contradicting foundation. It is also set-like. Predecessors of $[g]$ can be represented by functions whose value at $\xi$ lies in $g(\xi )\cup \{\varnothing \}$; these functions form a set. The Mostowski collapse theorem therefore gives a transitive class $N$ and an elementary embeddingThe usual class-ultrapower notation is understood via set-sized representatives and this set-like collapse.

For $\alpha <\kappa$, any function into $\alpha$ is constant on a $U$-large set: if none of its fewer-than-$\kappa$ fibers belonged to $U$, intersect their complements to get the empty set in $U$. Consequently every member of the ultrapower ordinal represented by the constant $\alpha$ is represented by a constant ordinal below $\alpha$. Induction on $\alpha$ now gives $j(\alpha )=\alpha$.

On the other hand the identity function $d(\xi )=\xi$ represents an ordinal below $j(\kappa )$. For every $\alpha <\kappa$, the tail $\{\xi :\xi >\alpha \}$ belongs to $U$, so the collapsed ordinal $[d]$ is above $j(\alpha )=\alpha$. HenceThis proves nonidentity explicitly. The collapsed identity class is at least $\kappa$; it need not equal $\kappa$ unless an additional normality convention is imposed on $U$.

Conversely, an elementary embedding $j:V\to N$ into a transitive class with critical point $\kappa$ yieldsFor the converse use the usual amenability assumption on the class embedding, so this collection is a set. Since $j(\kappa )>\kappa$, exactly one of $j(X)$ and $j(\kappa \setminus X)$ contains $\kappa$, proving the ultrafilter condition. Singletons are excluded because $j(\alpha )=\alpha <\kappa$. If $\lambda <\kappa$ and $X_i\in U$ for $i<\lambda$, then $j$ fixes $\lambda$ and every index below it, giving $j({\bigcap }_{i<\lambda }{X}_i)={\bigcap }_{i<\lambda }j(X_i)$; the intersection still contains $\kappa$. Thus $U$ is $\kappa$-complete and $\kappa$ is measurable.

In particular the first moved ordinal is a strongly inaccessible cardinal. If $\mathrm{cf}(\kappa )<\kappa$, partition $\kappa$ into fewer than $\kappa$ bounded intervals. Each is too small to lie in $U$, contradicting completeness. Thus $\kappa$ is regular. If $2^{\lambda }\ge \kappa$ for some $\lambda <\kappa$, choose distinct subsets $A_{\xi }\subseteq \lambda$ for $\xi <\kappa$. For each $\eta <\lambda$, choose the $U$-large side of the question $\eta \in A_{\xi }$. Intersect these fewer-than-$\kappa$ large sides. The intersection belongs to $U$, but all its indices have identical $A_{\xi }$, so it contains at most one index, contradicting nonprincipality. Therefore $2^{\lambda }<\kappa$ for every $\lambda <\kappa$, as required.

Use the embedding characterization of a supercompact cardinal: for every cardinal $\mu \ge \kappa$ there is an elementary embedding $j:V\to M$ into a transitive class with critical point $\kappa$, $j(\kappa )>\mu$ and $M^{\mu }\subseteq M$. In the Lévy hierarchy, a ${\Sigma }_2$ sentence can be put into the form $\exists x\forall y\theta (x,y)$ with bounded matrix $\theta$. The same argument allows parameters $p\in V_{\kappa }$, which the embedding fixes.

Suppose $V\models \exists x\forall y\theta (x,y,p)$ and choose a witness $a$. Pick an ordinal $\lambda$ with $a,p\in V_{\lambda }$, and a cardinal $\mu \ge \kappa$ large enough that $\mu \ge |V_{\lambda }|$ and $\mu >\lambda$. Take the corresponding supercompact embedding. Its closure implies $V_{\lambda }\subseteq M$: induct on rank, enumerate each set in this rank segment by at most $\mu$ elements already in $M$, and use $M^{\mu }\subseteq M$ followed by taking the range. Thus $a\in M$ and $\mathrm{rank}(a)<j(\kappa )$.

Bounded formulas are absolute between transitive classes. Since $\forall y\theta (a,y,p)$ holds in $V$, it holds in $M$ and then in the transitive rank segment $V_{j(\kappa )}^M$. This segment contains $a,p$, soApply elementarity to the first-order assertion that this sentence holds in the indicated cumulative hierarchy level, and use $j(p)=p$. We obtain the supercompact Sigma-two downward reflection conclusionThe closure requirement is used to put the original witness into the target; elementarity alone would not do that.

A transitive class $M$ satisfies $x\in M\Rightarrow x\subseteq M$. Its membership structure therefore does not omit elements of its members. In particular bounded membership statements are absolute between a transitive model and the ambient universe, and its membership relation is the actual well-founded relation, rather than an arbitrary externally ill-founded coding.

For a set $x$, put $x_0=x$ and $x_{n+1}=\bigcup x_n$, and defineThis is a set, contains $x$ as a subset, and is transitive: an element of an element of $x_n$ belongs to $x_{n+1}$. Any transitive set containing $x$ as a subset contains every $x_n$ by induction, so this construction is the least such set. Shifting the union index givesThese formulas use the specified subset convention for transitive closure.

Work in the usual ambient set theory with Choice. If $x$ is a hereditarily countable set, then every member of $\mathrm{TC}(\{x\})$ is countable. Iterated countable unions show that this entire closure is countable. Conversely a countable transitive closure makes each of its members countable. This equivalent criterion makes the following closure arguments explicit.

If $y\in x\in \mathrm{HC}$, then $\mathrm{TC}(\{y\})\subseteq \mathrm{TC}(\{x\})$, so $y\in \mathrm{HC}$: HC is transitive. If $x\in \mathrm{HC}$, its union is countable and its descendant sets are descendants of $x$, so $\bigcup x\in \mathrm{HC}$. The actual union therefore witnesses the Axiom of union inside $(\mathrm{HC},\in )$.

For axiom schema of separation, take any formula with parameters in HC and a set $x\in \mathrm{HC}$. Form the subset of $x$ consisting of the elements that satisfy that formula with all quantifiers relativized to HC. Ambient Separation supplies this set. It is a subset of a countable set, and all its descendants are inherited from $x$, so it belongs to HC. No claim that the formula itself is absolute is needed.

The axioms satisfied by hereditarily countable sets also include Extensionality, Empty Set, Pairing, Infinity, Foundation and Replacement. Extensionality and Foundation follow from transitivity and ambient well-foundedness. Empty Set and $\omega$ belong to HC, and a pair of HC sets has countable transitive closure. For Replacement, the domain is countable; a definable image of its elements is a countable family of HC sets, whose combined transitive closures form a countable union of countable sets, so the range again belongs to HC. Ambient Choice additionally gives Choice internally: a well-order of a countable HC set has a hereditarily countable relation and hence lies in HC.

Power Set fails. Every subset of $\omega$ is hereditarily countable, so an internal power-set witness would have to contain all ambient subsets of $\omega$. That collection is uncountable by Cantor theorem, whereas every HC set is countable. Thus HC satisfies the other ZF axioms and, in this ambient setting, Choice, but not the Axiom of power set.

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 $a\in M$ and suppose $N\models \exists u\in a\psi (u,\vec{b})$. Its witness $c$ is an actual member of $a$. Since $M$ is a transitive class, $c\in M$; the induction hypothesis then gives $M\models \psi (c,\vec{b})$. The converse uses the same witness in $N$. The bounded universal step follows similarly because both structures quantify over exactly the actual members of $a$, 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 $\phi$, choose a bounded equivalent $\psi$. The assumption that both structures model ZF gives ${\phi }^M\leftrightarrow {\psi }^M$ and ${\phi }^N\leftrightarrow {\psi }^N$. Combining these with the displayed equivalence proves the asserted set-theoretic absoluteness of ${\Delta }_0^{\mathrm{ZF}}$.

A transitive model of set theory is a transitive set or transitive class whose membership relation is the ambient membership relation and which satisfies the specified set-theoretic axioms.