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 and use the hereditarily locally small membership model
The ground cardinal is a strong limit cardinal of countable cofinality. This transitive class contains the empty set and . 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 , ground replacement collects its range . Since and every descendant of an element of already has fewer than members, . Thus the full functional Axiom schema of replacement holds. For , every actual subset of belongs to the class and
Consequently its entire power set belongs to the class. Extensionality and foundation are inherited from the ground membership relation; witnesses infinity. However belongs to , while its only possible union is , which does not. All the other ZF axioms hold, and union fails. Bounding the entire transitive closure by instead would give the wrong model: functional ranges at this singular bound need not be hereditarily small.
Power set. Use the transitive class 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 belongs to , but a putative internal power set of would contain all these subsets and hence be uncountable by Cantor's theorem. Power set fails in , with every other ZF axiom intact.
Replacement. Use 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 , define by finite iterations of power set. The finite iteration witnesses and each value are inside , so this is an internally definable total function on . Its range has rank of a set and is absent from the model. This instance of replacement fails.
Extensionality. Build well-founded coded sets over one urelement , retaining a distinct ordinary empty set . Membership of an atom is always false, and membership of a set code is its coded extension. Thus but they have identical empty extensions. Pairing, union, separation and replacement are performed on set codes; pure 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 contains all ordinary set-subsets of 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 exchange and and fix all other objects. On the same domain define the Rieger-Bernays permutation model
Since is a bijection, two objects with the same -members are equal, so extensionality holds. Any ground collection of desired members is represented by the object . In particular, an -pair is and the -union of is
An -subset of is an object with , so its -power-set object is
Translate every formula by replacing membership with ; ground separation and replacement collect the required extensions and the same representation supplies their internal witnesses. The -empty object is , and its -successor operation is . Ground well-founded recursion and replacement collect the iterates of from ; representing this collection gives an -inductive object. Thus infinity holds. But for , , whence and has precisely itself as its -member. Foundation fails.
Infinity. The hereditarily finite sets 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 , 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 be an infinite set of urelements and let every permutation of act recursively on sets. Keep precisely the hereditarily finitely supported objects: an object has a finite support if every permutation fixing 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 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 , ground well-foundedness and set-extensionality give the remaining axioms.
The family of unordered pairs of atoms is hereditarily supported. If it had a choice function , let be a finite support of . Choose distinct . The transposition exchanging fixes and , but exchanges its two possible chosen elements. Invariance of would imply 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 and use the hereditarily locally small membership model
The transitive class inherits extensionality and foundation. Definable subsets of its sets remain in it. If , a functional image of has size at most ; every member of that image is already hereditary, so the image belongs to . This verifies replacement, even though its values can have unbounded ranks. Also by the strong limit cardinal property, and each subset of is locally small. This verifies the Axiom of power set. Pairing and infinity follow similarly. But
since while . This is failure of sumset without failure of replacement or power set.
For the Axiom of power set, use the hereditarily countable sets . 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 is hereditarily countable, but the full power set is uncountable by Cantor's theorem and cannot be a member of . 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 . A limit rank contains the empty set and is closed under pairs, unions, subsets and power sets; it contains , and foundation and extensionality are inherited. Fix the parameter . The definable map
is internally described by a finite sequence of power-set iterations. Each finite sequence belongs to , so the definition is genuinely functional there. Its range has rank 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 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 no members. The two different objects 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 vacuously for every . 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, , 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 is finite. Hence infinity fails.
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 and use the hereditarily locally small membership model
It is a transitive class. The condition requires each individual set in the membership ancestry to have size below ; it does not require its entire transitive closure to have size below . Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and witnesses infinity. For , the actual also belongs to : if , then by the strong-limit property, while every subset of and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain , ground replacement, applied to the relativized first-order formula, gives its range . Since and every value is already in , its range is also locally small. Thus every replacement instance holds.
However, belongs to : its members have cardinalities , and their members are smaller still. Its actual union is , of cardinality , which is not in . 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 in the ground choice universe. This is transitive and contains . 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 , belongs to . A power-set witness for would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas is uncountable by Cantor's theorem. Power set fails.
For the Axiom schema of replacement, use with actual membership. This limit-rank structure contains and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below . A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable function
is obtained by successive power-set operations starting with the parameter . Each finite iteration, including its finite history, belongs to the structure. Its range has rank and is not an element of . 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 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 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 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 , giving all replacement instances. No finite set contains and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.
One can take . Finite induction gives for every finite : every subset of a finite level is definable using its finitely many elements as parameters. Hence , the set of hereditarily finite sets.
Now reason inside the constructible universe , a model of ZFC. The set is countable there, and there are countably many first-order formulas and finite parameter tuples. Thus is countable in . But the constructible power set is uncountable in by the Cantor theorem. Choose
This is constructible and a subset of , so and . Therefore
All comparisons were made inside ; this avoids assuming that the constructible reals are uncountable in the ambient universe. The witness remains valid externally because the two structures use the same , the same , and the same constructible level. Thus constructible sets of low rank can appear at later stages.
The epsilon-recursion theorem says that for every definable operation assigning a set to each set and each function with domain , there is a unique class function such that
for every set .
For uniqueness, suppose and both satisfy the recursion. If they agree on every , then their restrictions to agree and hence
The epsilon induction principle therefore gives .
For existence, call a function coherent on a transitive set when
The same epsilon-induction argument shows that any two coherent functions agree on the intersection of their transitive domains. Assuming coherent functions have been constructed below every member of , their compatible union defines all values below ; adjoining the value prescribed by extends the construction to . Epsilon induction establishes this construction for every . The compatible local functions therefore unite to the required class function .
A relation on is well-founded when every nonempty subset of has an element with no -predecessor in that subset. It is extensional when
The Mostowski collapse theorem states that every well-founded extensional relation is isomorphic to membership on a unique transitive set . Define recursively
Well-founded recursion makes well defined. Epsilon-style induction along , together with extensionality, shows that is injective. By definition,
so is an isomorphism from onto , where . If , then for some , so ; hence is transitive. If another collapse has transitive range, induction gives , proving uniqueness.
Finally, suppose is finite. Its collapse is a finite transitive set, so every member of is hereditarily finite. Therefore every well-founded extensional relation on collapses to a transitive subset of .
Conversely, let be infinite. Choose the initial infinite ordinal equinumerous with . The successor ordinal has the same cardinality as . Pulling its membership relation back along a bijection gives a well-founded extensional relation on whose collapse is . But is not hereditarily finite, so . Consequently,
The collection of hereditarily finite sets is
where and . Every is finite, and the axiom of infinity together with replacement and union makes a set. Hence this collection is not a proper class.
It is transitive: if , then , so every belongs to . It is also -closed. If and
then , so .