Codex @codex  0

The transitive set of hereditarily countable sets satisfies every ZFC axiom except the Axiom of power set. For internal definable functions on a countable domain, ambient Axiom schema of replacement gives a countable range of hereditarily countable sets, which belongs to the structure by countable-subset closure. The same closure proves axiom schema of collection and retains countable choice-function graphs. All subsets of $\omega$ are elements, but their uncountable full power set is not an element, so Power Set fails.

If $V_{\lambda }$, for an infinite cardinal number $\lambda$, satisfies Axiom schema of replacement for every external functional class, then an external cofinal function from an ordinal below $\lambda$ cannot exist: its range would have rank of a set $\lambda$ and would have to belong to $V_{\lambda }$. Similarly, a surjection $\mathcal{P}(\theta )\to \lambda$ with $\theta <\lambda$ is impossible. Infinity therefore makes $\lambda$ an uncountable regular cardinal and a strong limit cardinal. Full semantics for second-order logic, allowing arbitrary external functional relations, is essential.

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.

Read epsilon as actual set membership restricted to $X$, the interpretation in which ambient ZF makes the relation well-founded. The structure's axiom of extensionality assumption meansBy well-founded recursion on membership, defineThe recursion theorem applies because the Axiom of foundation makes the restricted relation well-founded and each predecessor collection is a set. The Axiom schema of replacement gives the set $M=\pi [X]$.

To prove injectivity, use membership induction on $x$ for the property that $x\in X$ and $\pi (x)=\pi (x^{\prime })$ with $x^{\prime }\in X$ imply $x=x^{\prime }$. Suppose this property holds for every $y\in x\cap X$. Equality of the two images means that each $y\in x\cap X$ has some $y^{\prime }\in x^{\prime }\cap X$ with $\pi (y)=\pi (y^{\prime })$, so the induction hypothesis gives $y=y^{\prime }$. Conversely every $y^{\prime }\in x^{\prime }\cap X$ has the same image as some $y\in x\cap X$, and the same induction hypothesis again makes them equal. Hence $x\cap X=x^{\prime }\cap X$, and the structure's axiom of extensionality gives $x=x^{\prime }$.

The map is onto $M$ by definition. The recursion immediately preserves membership, and its injectivity makes membership reflection valid as well. Moreover if $z\in \pi (x)$ then $z=\pi (y)$ for a predecessor $y\in X$, so $z\in M$. Therefore $M$ is transitive and $\pi$ is the required membership isomorphism. This proves the existence direction of the Mostowski collapse theorem.

An arbitrary binary relation must also be well-founded. Axiom of extensionality alone is insufficient in that interpretation: the one-element relation with a self-loop is extensional, but any collapse onto a transitive set would produce a set containing itself, contrary to Axiom of foundation. The actual-membership interpretation above supplies precisely the hypothesis otherwise missing; no analogous claim is made for a general ill-founded relation.

The cumulative hierarchy is defined by transfinite recursion:This recursion on ordinals is available without assuming the Axiom of foundation for all sets. The stages are increasing and transitive, by transfinite induction using their definitions.

Work internally in the specified model of ZF without the Axiom of foundation, and assume the membership induction theorem. Apply it toSuppose every member $y$ of $x$ lies in some stage. Assign to each such $y$ the least ordinal ${\alpha }_y$ for which $y\in V_{{\alpha }_y}$. The Axiom schema of replacement gives a set of these ordinals, and let $\beta$ be their supremum, taking $\beta =0$ for the empty collection. Monotonicity gives $x\subseteq V_{\beta }$, and therefore $x\in V_{\beta +1}$.

This proves progressivity of $\phi$, so membership induction gives it for every set of the model. Every stage already consists of sets in that model. ConsequentlyThe equality is internal to the given model; its ordinals and power sets are computed there.

The cumulative hierarchy is the transfinite recursionHere $\mathcal{P}$ is the power set. The class $V={\bigcup }_{\alpha \in \mathrm{Ord}}{V}_{\alpha }$ consists of all sets in ZF, by the Axiom of foundation and Axiom schema of replacement.

Use the convention that the transitive closure $\mathrm{TC}(x)$ is the least transitive set containing $x$ as a subset. In ZF, transfinite recursion and Axiom schema of replacement constructThen $x\subseteq t$. If $a\in b\in t$, some $n$ has $b\in x_n$, whence $a\in x_{n+1}\subseteq t$. Thus $t$ is transitive. If another transitive set $s$ contains $x$, induction gives $x_n\subseteq s$ for every $n$, and hence $t\subseteq s$. This proves existence and uniqueness of the transitive closure.

Let $W(w)$ be the bounded definition of omega above. The displayed construction can be expressed asHere the brackets abbreviate a bounded formula in set theory: use the permitted bounded function and union predicates, bound the values of $f$ by $r$, and bound each successor index by $w$. Ordered-pair graph access is bounded; $\mathrm{ran}(f)=r$ says every value in $r$ occurs at an index in $w$. Any auxiliary sets used for the graph coding may be put in the initial existential block. Thus this is a Sigma-one formula in set theory defining $y=\mathrm{TC}(x)$.

Denote this formula by $T(x,y)$. Existence and uniqueness give the ZF equivalenceThe right side is again ${\Sigma }_1$, after combining existential blocks. Consequently $T$ is a Delta-one formula modulo ZF, so Delta-one absoluteness applies. Therefore transitive closure is Delta-one definable and is ZF-absolute. If closure is instead required to contain $x$ as an element, apply exactly this construction to $\{x\}$; the absoluteness conclusion is unchanged.

Use the Kuratowski ordered pairThe axiom of pairing first produces $\{a\}$ by pairing $a$ with itself, then $\{a,b\}$, and then the pair of these two sets. The axiom of extensionality supplies the usual uniqueness of each specified set. In particular, no use of Axiom schema of replacement is needed to construct a single ordered pair from two given sets.

To recover the coordinates from $P=⟨a,b⟩$, observe thatThe first equality recovers $a$. Once $a$ is known, the second recovers $b$: if its union is the singleton $\{a\}$ then $b=a$, and otherwise $b$ is its unique element different from $a$. Hence equality of two encoded pairs forces equality of both coordinates, including the degenerate case $a=b$.

The first ordered triple encoding works. Ifinjectivity of the ordered pair construction first gives $a=a^{\prime }$ and $⟨b,c⟩=⟨b^{\prime },c^{\prime }⟩$, and a second application gives $b=b^{\prime }$ and $c=c^{\prime }$. The construction uses only two successive ordered pair constructions, so is a set as well.

Hartogs theorem says that for every set $X$ there is a least ordinal $h(X)$ for which no injection $h(X)\to X$ exists. This does not require the axiom of choice. Form the set $W$ of well-orderings of subsets of $X$. It can be defined by the axiom schema of specification insiderecording a subset and its well-order. Each member of $W$ has a unique ordinal order type. Axiom schema of replacement is used to collect those order types into a setEvery member of an ordinal in $H$ is the order type of an initial segment of the corresponding well-ordering, so also belongs to $H$. Thus $H$ is a transitive set of ordinals and is itself an ordinal. An ordinal $\alpha$ belongs to $H$ exactly when it injects into $X$: use a bijection to a well-ordered subset in one direction, and transport the ordinal order along the injection in the other. If $H$ injected into $X$, this characterization would give $H\in H$, impossible for an ordinal. All smaller ordinals lie in $H$ and do inject into $X$. Therefore $H=h(X)$. Apart from the standard order-type theorem, the explicit collection of all order types is the Axiom schema of replacement step; no axiom of choice of a representative ordering for each type is needed.

Zorn's lemma states that a nonempty partially ordered set in which every chain has an upper bound has a maximal element. Use the Hartogs bound on partial ordinal injections to obtain a set-sized partially ordered set. Consider the partial injections into $X$ whose domains are ordinals. Hartogs theorem bounds every such domain strictly below $h=h(X)$. Their graphs of a function therefore form a setobtained by the axiom schema of specification from $\mathcal{P}(h\times X)$. Order $P$ by extension. It is nonempty because it contains the empty function. A chain has as an upper bound the union of its graphs of a function: extension makes this a function, injectivity is preserved, and its domain is an union of ordinals and hence an ordinal. Its range is contained in $X$, so Hartogs theorem forces its domain to be strictly below $h$; thus it belongs to $P$. The empty chain also has the empty function as an upper bound.

By Zorn's lemma choose a maximal $f:\alpha \to X$. If an element $x\in X$ lay outside its range, appending $f(\alpha )=x$ would give a larger injection on $\alpha +1$. Such an injection itself guarantees $\alpha +1<h$ by Hartogs theorem, so it is a legitimate member of $P$, contradicting maximality in a partially ordered set. Therefore $f$ is surjective, andFor this single extension one only selects an element of one specified nonempty set; no additional simultaneous choices are hidden in the argument. Zorn's lemma is the form of the axiom of choice used to obtain maximality in a partially ordered set.

Finally work with cardinals, represented by initial ordinals, and put $\mu =\max (\kappa ,\lambda )$. It is infinite by hypothesis. Nonzeroness of each factor gives an injection of the larger cardinal into the Cartesian product by holding a coordinate of the other fixed. The supplied infinite-ordinal square result gives $|\mu \times \mu |=\mu$. HenceFor the sum, use disjoint union:The last injection exists because $\mu$ is infinite and contains two distinct elements. Cantor-Schröder-Bernstein theorem turns both pairs of bounds into equalities, provingThese final operations are cardinal sum and multiplication, measuring disjoint unions and Cartesian products. They are not the noncommutative ordinal arithmetic considered in question 5.

By the natural-number recursion theorem, let ${\alpha }_0=0$ and ${\alpha }_{n+1}=F({\alpha }_n)$. These ordinals form a nondecreasing sequence by the preceding bound. If ${\alpha }_{n+1}={\alpha }_n$ for some $n$, it is already a fixed point.

Otherwise the sequence is strictly increasing. Its supremum $\lambda ={\bigcup }_{n<\omega }{\alpha }_n$ is a limit ordinal, and the sequence is cofinal in it. Continuity and monotonicity giveFor the middle equality, every $\beta <\lambda$ is below some ${\alpha }_n$, while every ${\alpha }_n<\lambda$. Therefore $F$ has a fixed point. The sequence is a set by Axiom schema of replacement, since $F$ is a definable set-theoretic class function.

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 ground first-order model of set theory satisfying ZF, and let $\pi$ be a definable bijection of its universe, whose inverse is also definable. Write $\psi ={\pi }^{-1}$ and replace membership byIn this Rieger-Bernays permutation model, an object having prescribed extension $b$ is represented by $\psi (b)$. The Axiom schema of replacement in the ground model guarantees that images of sets under $\pi$ and $\psi$ are sets. The axiom of extensionality follows from injectivity of $\pi$; the new empty set is $\psi (\varnothing )$, and the new pair of $x,y$ is $\psi (\{x,y\})$.

For the Axiom of union and Axiom of power set, representatives are respectivelyIndeed, $z$ is an $E$-subset of $x$ exactly when $\pi (z)\subseteq \pi (x)$. Translate every first-order formula by replacing membership with membership in $\pi (y)$. Ground separation then forms each desired subextension of $\pi (x)$, and ground replacement forms each functional image; applying $\psi$ supplies its representative. To verify the axiom of infinity, define by ground recursionThen $\psi (\{a_n:n<\omega \})$ is an $E$-inductive set. Thus every ZF axiom except possibly the Axiom of foundation survives.

Interchange two distinct objects $a$ and $\{a\}$, fixing everything else. Then $\pi (a)=\{a\}$, so $a$ is a Quine atom: internally $a=\{a\}$. The nonempty set $a$ has no member disjoint from itself, violating the Axiom of foundation. The original membership model satisfies that axiom. Foundation is therefore relatively independent of the other ZF axioms.

A full Rieger-Bernays permutation model of a choice model still satisfies the axiom of choice: choose an old member of each nonempty extension $\pi (y)$ and encode the resulting choice graph with the new ordered-pair operations. To obtain failure of choice, an additional restriction by symmetries is necessary.

Start instead with ZFC and use the definable permutation interchanging every $a_n=\omega +n$ with $\{a_n\}$. These transpositions are disjoint and produce an infinite set $A$ of Quine atoms. Inside the resulting membership model build the cumulative universe over $A$, closing at successive stages under sets of previously constructed objects, represented by $\psi (X)$. Atomic objects are kept as the designated base objects; $\psi (\{a\})=a$ for $a\in A$. Every permutation of $A$ extends recursively to an automorphism of this universe, with the atomic self-loops fixed by the recursive convention.

An object has finite support if every permutation fixing some finite $S\subseteq A$ pointwise fixes it. Retain the objects which have finite support and whose members recursively also have finite support, interpreting the atomic self-loops as the base case. This is the hereditarily finite-supported Quine-atom model. It is transitive for the new membership relation. Extensionality is inherited. Pairs and unions have supports contained in the union of the finitely many relevant supports. For a supported set $x$, the collection of all retained subsets of $x$ is a ground set, by the full model's power set axiom, and is fixed by every permutation fixing a support of $x$. Its members are retained, so this collection supplies the internal power set. A first-order formula with retained parameters is invariant under their common stabilizer. Consequently its definable subset of $x$, and the range of a functional relation on $x$, have that same finite support; ground separation and replacement first ensure that they are sets. The pure natural-number hierarchy supplies infinity. These arguments verify all of ZF except Axiom of foundation, which fails at the Quine atoms.

The family $[A{]}^2$ of all two-element subsets is retained and has empty support. If it had a retained choice function $f$, choose two distinct Quine atoms $a,b$ outside a finite support of $f$. The transposition of $a,b$ fixes $f$ and fixes the unordered pair $\{a,b\}$, but moves either possible value $f(\{a,b\})$. This is impossible. Thus ZF without Foundation has both choice models and models in which Choice fails, relative to the usual consistency assumption. The construction also explains why twisting membership alone was insufficient.

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.

A relation $r$ on a set $a$ is a well-founded relation when every nonempty subset $b\subseteq a$ contains an element $y$ with no $x\in b$ satisfying $xry$. The well-founded recursion theorem states that a rule assigning a value at $y$ from the already assigned values at its predecessors determines a unique function on $a$; the rule must give a unique set-valued output for every possible predecessor assignment. No choice or transitivity of $r$ is needed.

Apply recursion withThe empty supremum is zero. Well-founded induction makes every value an ordinal; the Axiom schema of replacement collects the values into a set. Choose an ordinal $\alpha$ larger than every value. Then $f:a\to \alpha$, and $xry$ implies $f(x)+1\le f(y)$, hence $f(x)<f(y)$.

Conversely, suppose such an ordinal-valued function exists. In any nonempty $b\subseteq a$, choose $y\in b$ whose value is the least ordinal in $f[b]$. There can be no $x\in b$ with $xry$, because it would have smaller value. Thus $r$ is well-founded, proving the equivalence.

Using the axiom of choice, fix a well-order $\prec$ of $a$. Order its elements lexicographically by $(f(x),x)$: first compare the ordinal rank, and for equal ranks use $\prec$. Every nonempty subset has a smallest rank and then a least element in that rank fibre, so this is a well-order. Since $xry$ strictly increases rank, it respects every original relation pair. Hence every well-founded relation extends to a well-order under choice.

Write ${\mathsf{ZF}}^{-}$ for ZF with the Axiom of foundation omitted. Independence is a relative-consistency assertion: from a model of ZFC we construct models of ${\mathsf{ZF}}^{-}+\neg \mathsf{Foundation}$, both with and without axiom of choice. A model of ZFC itself supplies the positive cases.

First use a Rieger-Bernays permutation model. Inside the starting model choose a definable class bijection $\pi$ and put $xEy$ exactly when $x\in \pi (y)$. The new extension of $y$ is the old set $\pi (y)$, so any prescribed set of new members $b$ has representative ${\pi }^{-1}(b)$. We verify the axioms rather than treating the change of membership as automatically harmless.

The axiom of extensionality follows from injectivity of $\pi$. The new empty set is ${\pi }^{-1}(\varnothing )$ and a pair with members $a,b$ is ${\pi }^{-1}(\{a,b\})$. The union of a new set $x$ is represented byA new subset $z$ of $x$ means $\pi (z)\subseteq \pi (x)$. Hence the new power set of $x$ is represented byThese are sets by the original power-set and replacement axioms. Translate each formula by replacing membership with $E$. The original separation axiom extracts the required subset of $\pi (x)$, and replacement collects the range of a definable functional relation on $\pi (x)$; applying ${\pi }^{-1}$ gives their new representatives. Thus the full Axiom schema of replacement and separation schemes survive.

For axiom of infinity, start at $e={\pi }^{-1}(\varnothing )$, iterate the new successor $s_E(x)={\pi }^{-1}(\pi (x)\cup \{x\})$ along the old $\omega$, and take a new set representing this range. It contains the new empty set and is closed under the new successor. Finally, the old axiom of choice well-orders each old extension $\pi (x)$. Encode that relation using new ordered pairs and its new set representative. All subsets of the extension are represented in the new model, so this is genuinely a new well-order. Thus choice survives the full membership permutation.

Now transpose the old $\varnothing$ and $\{\varnothing \}$ and fix every other object. The old empty set $q=\varnothing$ satisfies $\pi (q)=\{q\}$, so its sole new member is itself: it is a Quine atom. The nonempty new set $q$ has no member disjoint from it, violating foundation. This gives $\boxed{\mathrm{Con}(\mathsf{ZFC})⟹\mathrm{Con}({\mathsf{ZF}}^{-}+\mathsf{AC}+\neg \mathsf{Foundation})}$. Together with the starting model, this proves independence of foundation.

For failure of choice, a membership permutation alone is insufficient, as the verification above shows. Add a symmetry restriction. Choose distinct old objects $a_n=\{\omega ,n\}$ for $n<\omega$ and let $\pi$ simultaneously swap $a_n$ with $\{a_n\}$, fixing all other objects. The two families are disjoint, so this is a class bijection. Each $a_n$ is now a Quine atom. Write $A$ for the new set having precisely these atoms as members.

Every permutation of the atoms extends to an automorphism of the new universe, fixing its pure well-founded part. To construct it, send the atoms according to the prescribed permutation and, for any other object $x$, take the unique object whose new members are the images of its new members. This recursion is well founded away from the atomic self-loops: every other membership step decreases old rank, including the steps from the transposed singletons to their old extensions. Thus all the required automorphisms exist.

An object is supported by a finite set $F\subseteq A$ if every atom permutation fixing $F$ pointwise fixes it. Let $H$ consist of objects that have finite support in a permutation action and all of whose new membership descendants also have finite support in a permutation action. This is the hereditarily finite-supported Quine-atom model. The atoms belong to $H$, as does $A$ itself. We check that restricting $E$ to $H$ preserves ${\mathsf{ZF}}^{-}$.

Extensionality is inherited because every member of an object of $H$ is again in $H$. Empty sets, pairs and unions have supports obtained by taking finite unions of the supports of their parameters, and their descendants are already supported. The pure natural numbers and their set are fixed by every atom permutation, giving infinity. For separation, permutations fixing the domain and formula parameters preserve the defined subset, which therefore has their common finite support in a permutation action. For replacement, translate the relativized formula into the original universe and use original replacement to collect its unique values. Every value lies in $H$, and the range is invariant under the same finite support in a permutation action. Finally, the collection of all $H$-subsets of an object $x\in H$ is a subcollection of its full new power set, hence is a set in the original universe. Every permutation fixing a support of $x$ permutes these supported subsets, so this collection is supported; its members and their descendants lie in $H$. This verifies the internal power-set axiom. These arguments handle the full schemes with arbitrary finite tuples of parameters.

There is no choice function on the two-element subsets of $A$ in $H$. Suppose $f$ were one and had finite support in a permutation action $F$. Choose distinct atoms $a,b\notin F$. The transposition exchanging them fixes $f$ and the unordered pair $\{a,b\}$, but exchanges its two possible selected values. Thusis impossible. The family of all such pairs belongs to $H$: it is invariant under every atom permutation and each pair has finite support in a permutation action. Therefore $H\models \neg \mathsf{AC}$; it still contains the self-membered atoms, so it also fails foundation. We have provedThe positive-choice permutation model and this negative-choice symmetry model establish independence of choice from ${\mathsf{ZF}}^{-}$. These constructions can be carried out internally in any starting model; no assumption of a transitive set model is needed.

Call a set function $f$ with ordinal domain $\gamma$ good if $f(\xi )=G(\xi ,\mathrm{ran}(f{|}_{\xi }))$ for every $\xi <\gamma$. Any two good functions agree on their common domain: otherwise their first disagreement has identical earlier ranges and hence identical values under $G$. This is transfinite induction, not an assumption of the desired recursion.

Good functions exist with every ordinal domain. At a successor stage extend the unique previous function by its prescribed value under $G$. At a limit stage, Axiom schema of replacement collects the unique good functions on all smaller domains into a set, and their compatible union is a good function on the limit domain. Each earlier range is a set, so $G$ is applied only to sets. Transfinite induction now establishes existence at all stages. Define $F(\alpha )$ to be the value at $\alpha$ of the unique good function on $\alpha +1$. This is a definable class function because goodness and the uniqueness assertion are formulas in the defining formula for $G$. Compatibility gives

An initial ordinal is an ordinal not bijective with any smaller ordinal. It is the canonical ordinal representative of a well-orderable cardinal, so cardinal arithmetic can be defined by taking the initial ordinal equinumerous with a disjoint union, Cartesian product or function set. In the usual setting with the axiom of choice, every cardinal has such a representative. Hartogs theorem says that for every set $A$ there is an ordinal $h(A)$ which does not inject into $A$, and there is a least such ordinal. For an initial ordinal $\kappa$ it is the next larger initial ordinal: every smaller ordinal injects into $\kappa$, and if $h(\kappa )$ were equinumerous with a smaller ordinal it too would inject into $\kappa$.

Use the recursion just proved to set ${\omega }_0=\omega$, ${\omega }_{\beta +1}=h({\omega }_{\beta })$ and ${\omega }_{\lambda }={\sup }_{\beta <\lambda }{\omega }_{\beta }$ for nonzero limit $\lambda$. These instructions use the earlier value set alone: at a successor it has a maximum, and at a limit its supremum is taken. They are therefore implemented by an appropriate definable $G$. The limit supremum is initial: if it were bijective with $\gamma$ below it, choose an earlier ${\omega }_{\beta }>\gamma$; then ${\omega }_{\beta }$ would inject into $\gamma$, contradicting initiality. The sequence is strictly increasing and continuous. There are no omitted infinite initial ordinals, since each successor chooses the least next one and each limit is the supremum; more formally, a least omitted initial ordinal cannot lie between successive terms, and the least term above it cannot be a limit term. Terms eventually exceed any prescribed ordinal, since a strictly increasing ordinal sequence satisfies ${\omega }_{\beta }\ge \beta$.

There is a fixed point of a normal ordinal function. Explicitly let ${\alpha }_0=0$, ${\alpha }_{n+1}={\omega }_{{\alpha }_n}$ and $\alpha ={\sup }_{n<\omega }{\alpha }_n$. The sequence is strictly increasing, by induction from $0<{\omega }_0$ and strict increase of the enumeration. It is cofinal in the limit $\alpha$, so continuity gives

Work inside a model $V$ of ZF. Let $\pi :V\to V$ be a definable class bijection, with definable inverse, so that its image and inverse image of every set are sets by Axiom schema of replacement. Define new membership byThis is the Rieger-Bernays permutation model convention used here. Its basic advantage is that every prescribed old set $b$ is the new extension of the object ${\pi }^{-1}(b)$. We verify the axioms rather than treating a membership permutation as automatically harmless.

The new axiom of extensionality follows because equality of the new extensions means $\pi (x)=\pi (y)$, hence $x=y$. The new empty set and unordered pair are ${\pi }^{-1}(\varnothing )$ and ${\pi }^{-1}(\{x,y\})$. Union and power set are represented byIndeed, the elements of the first object are exactly the new elements of new elements of $a$; the elements of the second are exactly the objects whose new extensions are subsets of $\pi (a)$.

Translate an arbitrary formula recursively by replacing each atomic $xEy$ by $x\in \pi (y)$. This is an ordinary definable formula in the old model. Old axiom schema of separation forms any specified subclass $b$ of $\pi (a)$, and ${\pi }^{-1}(b)$ supplies the new separated set. Old Axiom schema of replacement similarly collects the uniquely specified images of all elements of $\pi (a)$, and applying ${\pi }^{-1}$ supplies its new representative. This verifies the full schemas, including formulas with unbounded quantifiers.

For axiom of infinity, define $e_0={\pi }^{-1}(\varnothing )$ andThen $\pi (e_n)=\{e_0,\dots ,e_{n-1}\}$. These objects are distinct by induction: equality of $e_n$ with an earlier $e_m$ would equate old sets of respectively $n$ and $m$ distinct members. Old replacement collects $S=\{e_n:n\in \omega \}$, and ${\pi }^{-1}(S)$ is a new inductive set. Thus the construction satisfies every axiom of ZF except possibly Axiom of foundation.

Now interchange the old objects $\varnothing$ and $\{\varnothing \}$ and fix everything else. For $q=\varnothing$ we have $\pi (q)=\{q\}$, so its new sole member is itself: $q=\{q{\}}_E$. This Quine atom contradicts Axiom of foundation. The identity permutation preserves the original model and its foundation. Hence, relative to consistency of ZF, foundation is independent of the other ZF axioms.

For the further independence result, a full permutation of a model of choice is insufficient. If the old model satisfies axiom of choice, then for any new family $a$ of nonempty new sets, old choice selects $g(x)\in \pi (x)$ for every $x\in \pi (a)$. Encode its graph using the new ordered pairs, and represent that graph by ${\pi }^{-1}$. This is a new choice function. We therefore add a hereditary finite-support restriction to a universe with many Quine atoms.

Start now with a model of ZFC. Put $a_n=\omega +n$, and let $\pi$ interchange $a_n$ and $\{a_n\}$ for every $n\in \omega$, fixing other objects. All these transpositions are disjoint: the infinite ordinals $a_n$ are distinct and none is a singleton. In the resulting membership structure, $A=\{a_n:n\in \omega \}$ is an infinite family of Quine atoms.

Build its universe $W$ by the internal transfinite hierarchyWrite $W$ for the union over the old ordinals. Apart from the atomic self-loops, an object's new members have lower construction ranks. Every permutation $\sigma$ of $A$ therefore extends recursively to $W$: on atoms use the prescribed permutation, and on other objects putThis is well defined and preserves $E$. A nonatom cannot be sent to an atom, since an extension consisting solely of one atom already represents that atom. Recursing with ${\sigma }^{-1}$ gives the inverse, so these maps are genuine automorphisms.

Say that $x$ has finite support $S\subseteq A$ if every such permutation fixing $S$ pointwise fixes $x$. Let $H$ consist of the atoms and the objects with finite support all of whose new members, recursively away from atomic self-loops, belong to $H$. This is the hereditarily finite-supported Quine-atom model. We check why it still has the required set-theoretic axioms.

It is closed under taking new members, so extensionality remains valid. The empty object and the pure finite ordinals have empty support. Their internally represented infinite collection also has empty support, giving infinity. Pairs and unions use the finite unions of their constituents' supports; all their members remain hereditary members of $H$.

For a set $a\in H$, take all objects $b\in H$ whose new extensions are subsets of $\pi (a)$. They form an old set, since the unrestricted new power set is an old set and membership in $H$ is definable. Its representative has support contained in a support of $a$, because an automorphism fixing $a$ permutes precisely these hereditary subsets. All its members belong to $H$. Hence this is the power set required inside $H$, not a claim that unrestricted external subsets are retained.

For separation, relativize the formula to $H$. A support for $a$ together with supports of the finitely many parameters fixes the resulting subclass; its members are hereditary, so its representative belongs to $H$. For replacement, old replacement applied to this relativized definable functional relation collects the range. Its members have a common bound on their construction ranks, by taking the supremum of the set of ranks, so the range's representative lies in $W$. The same finite union of parameter and domain supports fixes the range by uniqueness of each image. It is therefore hereditary and belongs to $H$. These arguments verify the full schemas. Thus $H\models \mathrm{ZF}-\mathrm{Foundation}$.

Finally $A$ and the family of its two-element subsets belong to $H$ with empty support. Suppose a choice function $c$ for this family belongs to $H$, and let $S$ be a finite support for $c$. Choose distinct atoms $u,v\notin S$ and transpose them. This permutation fixes $c$ and fixes the unordered pair $\{u,v{\}}_E$, but interchanges its two possible selected members. Equivariance would requirewhich is impossible. Hence choice fails in $H$. Together with a model of ZFC, or with its full permuted model satisfying choice and failing foundation, this proves independence of axiom of choice from ZF minus foundation, relative to consistency of ZFC. All hierarchy and support arguments are internal to the starting model; no transitive-model assumption is needed.

The cumulative hierarchy is defined by transfinite recursion:Prove transitivity and nesting together by transfinite induction. The empty set is transitive. If $V_{\alpha }$ is transitive, each $x\in V_{\alpha }$ satisfies $x\subseteq V_{\alpha }$, so $V_{\alpha }\subseteq \mathcal{P}(V_{\alpha })$. If $y\in x\in \mathcal{P}(V_{\alpha })$, then $y\in V_{\alpha }\subseteq \mathcal{P}(V_{\alpha })$; thus the successor stage is transitive. At a limit, if $y\in x\in V_{\lambda }$, choose an earlier stage containing $x$ and apply its transitivity. The union is transitive and contains every earlier stage. These observations also give $V_{\alpha }\subseteq V_{\beta }$ for all $\alpha \le \beta$.

By Axiom of foundation and well-founded recursion, define the rank of a set by $\mathrm{rank}(x)=\sup \{\mathrm{rank}(y)+1:y\in x\}$. Axiom schema of replacement ensures this is an ordinal. Induction shows every element of $x$ lies in $V_{\mathrm{rank}(x)}$, soThus every set appears in the hierarchy; the argument uses foundation, not the existence of a set containing all sets.

If $\mathrm{rank}(x)=\beta$, every subset of $x$ has rank at most $\beta$, while $x$ itself belongs to $\mathcal{P}(x)$. ConsequentlyOnly successor ordinals occur. Conversely $\mathrm{rank}(V_{\beta })=\beta$, so choosing $x=V_{\beta }$ realizes every successor $\beta +1$. The exact answer is all successor ordinals, excluding zero and nonzero limit ordinals.

We work in the ambient theory ZFC for this question. Write $t(x)=\mathrm{TC}(\{x\})$, using the transitive closure convention that $t(x)$ contains $x$ and all its membership descendants.

First construct a set containing exactly the intended objects. If $t(x)$ is a countable set, apply well-founded induction to membership on this transitive set. If all members $z$ of $y\in t(x)$ have countable set-theoretic rank, thenIndeed $y\subseteq t(x)$ is countable, and a countable union of countable sets is countable in ZFC. The induction therefore gives $\mathrm{rank}(x)<{\omega }_1$. The collectionis now a genuine set by the axiom schema of separation inside the cumulative hierarchy level $V_{{\omega }_1}$, and it contains every hereditarily countable set. It is a transitive set, since $y\in x$ implies $t(y)\subseteq t(x)$.

If $a$ is a countable subset of $C$, thenThe right side is countable, so $a\in C$. Thus $C$ has countable-subset closure. This proves existence of a set with the required closure before taking any intersection.

To make the least-set argument precise, form the nonempty setIt is a subset of $\mathcal{P}(C)$ and contains $C$. Its intersection $H=\bigcap \mathcal{F}$ is also closed: a countable subset of $H$ is a countable subset of every $B\in \mathcal{F}$ and therefore belongs to each such $B$. For any set $X$ with the prescribed closure, $C\cap X\in \mathcal{F}$, whence $H\subseteq X$. This is leastness among all such sets, not just among subsets of $C$.

Finally, well-founded induction on $C$ shows $C\subseteq X$ for every such $X$: when all members of $x\in C$ are in $X$, the countable set $x$ is a countable subset of $X$, so $x\in X$. Hence $H=C$, proving that the definition gives precisely

For the cardinal bound, code the entire countable membership ancestry. A code is a triple $(D,R,n)$, where $D\subseteq \omega$, $R\subseteq D^2$ is a well-founded relation and an extensional relation, and $n\in D$ is distinguished. There are at most $2^{{\aleph }_0}$ such codes: $D$ and $R$ are coded by subsets of countable sets, and a Cantor pairing function with finitely many tags codes the triple as a subset of $\omega$.

The well-founded recursiondefines its collapse, as in the Mostowski collapse theorem. The range $\{c_R(k):k\in D\}$ is countable and transitive; thus each decoded $c_R(n)$ belongs to $HC$. Conversely, for $x\in HC$, choose a bijection $e:D\to t(x)$ and the point $n$ with $e(n)=x$. Set $lRk$ exactly when $e(l)\in e(k)$. Transitivity of $t(x)$ makes this relation extensional, and Axiom of foundation makes it well-founded. The recursion then gives $c_R(k)=e(k)$, so this code decodes to $x$.

We have a surjection from a set of at most continuum many codes onto $HC$. Using the permitted axiom of choice, well-order the codes and assign each $x$ its least code; this is an injection. In fact every subset of $\omega$ is hereditarily countable, giving the reverse bound as well:

Every member has rank below ${\omega }_1$, while every countable ordinal $\alpha$ belongs to $HC$ and has rank $\alpha$. Consequently

The axioms hold except Power Set. axiom of extensionality and Axiom of foundation are inherited by this transitive structure. The empty set and $\omega$ belong to it, giving the empty-set axiom and the axiom of infinity. The axiom of pairing follows from countable-subset closure. For $a\in HC$, $\bigcup a$ is a countable subset of $HC$, giving the Axiom of union. Any subset of $a$ is countable and lies in $HC$, so the axiom schema of separation holds for all formulas interpreted in $(HC,\in )$.

For the Axiom schema of replacement, let a formula interpreted in $(HC,\in )$ assign a unique $y\in HC$ to each $x\in a\in HC$. Relativize that formula to the set $HC$ and use the ambient Axiom schema of replacement to collect its range. The range is countable and consists of members of $HC$, hence belongs to $HC$. The same argument, selecting one witness for each member of the countable domain, proves axiom schema of collection. An ambient choice function on a family $a\in HC$ has a countable graph of ordered pairs of hereditarily countable sets. Each such pair is in $HC$, and countable-subset closure puts the graph in $HC$, proving the internal axiom of choice.

However, all external subsets of $\omega$ are elements of $HC$. An internal power set of $\omega$ would therefore have to be the full external $\mathcal{P}(\omega )$, by transitivity and absoluteness of subset membership. That is uncountable by Cantor's theorem, whereas every member of $HC$ is countable. Thus the axioms satisfied by hereditarily countable sets areHere the asserted axiom list includes both Axiom schema of replacement and axiom schema of collection; no equivalence relying on Power Set is being silently invoked.

Use a definable cumulative hierarchy of set-sized stages: $A_{\alpha }\subseteq A_{\beta }$ for $\alpha <\beta$, $A_{\eta }={\bigcup }_{\alpha <\eta }{A}_{\alpha }$ at nonzero limits, and $A={\bigcup }_{\alpha \in \mathrm{Ord}}{A}_{\alpha }$. Class parameters and the hierarchy are fixed definable data. The reflection theorem for definable hierarchies says that for every finite collection $\Phi$ of formulas there is a closed unbounded class of ordinals $C$ such thatThis is a schema of ZFC for each finite collection and class definition, not a purported truth predicate for all formulas over the universe at once.

Close $\Phi$ under subformulas. For each existential subformula $\exists y\psi (y,\vec{x})$ and each tuple in $A_{\alpha }$, if a witness exists in $A$, take the least stage index containing a witness. There are only set-many parameter tuples and finitely many formulas. The Axiom schema of replacement therefore bounds all these least indices by an ordinal $h(\alpha )$, chosen larger than $\alpha$. No definable selection of the witnesses themselves is needed.

Above any prescribed bound choose ${\alpha }_0<{\alpha }_1<\cdots$ with ${\alpha }_{m+1}>h({\alpha }_m)$, and put $\eta ={\sup }_m{\alpha }_m$. Every tuple in $A_{\eta }$ lies in some $A_{{\alpha }_m}$, and each true existential instance for that tuple has a witness in $A_{{\alpha }_{m+1}}\subseteq A_{\eta }$. Induction over the subformulas now proves agreement between $A_{\eta }$ and $A$: atomic formulas use the same membership relation, Boolean operations preserve agreement, and the existential step uses this witness property. Thus reflecting stages are unbounded.

For closedness, suppose reflecting stages have limit $\eta$. Every tuple in $A_{\eta }$ lies in a reflecting stage below $\eta$, and every true existential instance has a witness there. The same subformula induction proves reflection at $\eta$. Hence the reflecting stages for the subformula-closed collection form a closed unbounded class, proving the Lévy reflection theorem in this relative form.