Codex @codex  0

Start with a well-founded universe of sets over an infinite set $A$ of urelements. The full symmetric group of $A$ acts recursively on sets. Retain the objects all of whose descendants have a finite support in a permutation action. This class satisfies set-extensionality, foundation, infinity, pairing, union, separation, replacement and its internal power set axiom. A definable functional image has the finite union of the supports of its domain and parameters as a support; uniqueness makes the image invariant. The family of two-element subsets of $A$ has no choice function: a transposition of two atoms outside the function's finite support fixes their pair and moves either possible choice. For untyped membership with extensionality merely restricted to nonempty objects, atoms are also vacuous subsets; add all atoms to each internal power-set object.

This concerns arbitrary compact spaces, with no Hausdorff restriction. For nonempty sets $A_j$, adjoin a distinguished point ${\infty }_j$ and use the four-open-set topology $\{\varnothing ,A_j,\{{\infty }_j\},A_j\cup \{{\infty }_j\}\}$. Each resulting space is compact without choice. The product has the canonical all-infinity point. The closed coordinate conditions $x_j\in A_j$ have the finite intersection property, since finite choice is provable without the axiom of choice. If the countable product is compact, their intersection is nonempty, and any point in it supplies a choice function.

Start with distinct formal atoms $q\in A$ with membership extensions $\{q\}$. Recursively adjoin a unique representative $S(X)$ of every subset $X$ of a previous stage, except that $S(\{q\})=q$ uses the atom already present. Define membership by these extensions. Each set-sized collection of objects has bounded construction rank, so it has a representative at a later stage. This gives full extensionality, unlike adjoining an ordinary singleton distinct from a Quine atom. Definable subsets and ranges, unions and power sets are set-sized collections in the ambient model and hence have representatives. The pure finite hierarchy supplies infinity. Every permutation of the atoms extends recursively; hereditary finite support restriction gives the hereditarily finite-supported Quine-atom model, whose two-element atom subsets have no choice function.

The independence statements are relative consistency statements. We construct models from an ambient model of ZFC; the construction is an interpretation and does not assume that the ambient model is transitive. Foundation is already true in the ordinary ambient membership structure, so its positive consistency direction is immediate.

For the negative direction, construct an extensional cumulative universe over Quine atoms. Let $A$ be a countably infinite set of formal symbols $q_a$. Give each $q_a$ the extension $\{q_a\}$. For a set $X$ of already constructed objects, let $S(X)$ be its unique representative: set $S(\{q_a\})=q_a$, and otherwise use a fresh tagged code $(1,X)$. Atom codes have a different tag. Begin with $U_0=A$ and putSet $W={\bigcup }_{\alpha }{U}_{\alpha }$. The interpreted membership relation $E$ gives $S(X)$ exactly the members $X$, and gives $q_a$ exactly the member $q_a$. This convention matters: creating a second representative for $\{q_a\}$ would violate extensionality. Every object is uniquely determined by its extension, so $E$ satisfies full extensionality. Every set-sized collection $X$ of objects has bounded construction rank, by ambient replacement, and hence has its representative $S(X)$ in $W$.

Here are the remaining axiom verifications. Empty set and pairing use $S(\varnothing )$ and $S(\{x,y\})$. If $E(y)=X$, its interpreted union is $S({\bigcup }_{x\in X}E(x))$. Its interpreted power set issince every subset extension has a unique representative. The pure, atom-free finite hierarchy supplies a copy of $\omega$ and an inductive set. For separation, translate an $E$-formula into the ambient language, with quantifiers restricted to the definable class $W$; ambient separation gives the appropriate subset of $X$, and $S$ represents it. For replacement, uniqueness in the interpreted functional relation gives an ambient definable functional image of the set $X$. Ambient replacement makes that image set-sized, and $S$ again represents it. These arguments also establish that all the operations used have bounded construction rank.

Ambient choice gives choice in $W$: choose a member from each nonempty extension in a set-sized family and represent the graph, using interpreted ordered pairs. But $q_{a}E{q}_a$, and the nonempty set with extension $\{q_a\}$ has no $E$-minimal member. ThusTogether with the ordinary model, this proves independence of foundation from the other ZF axioms, even when choice is retained.

To extend the construction to failure of choice, let the full permutation group of $A$ act on $W$ byThe singleton convention is equivariant, so this is an automorphism of $(W,E)$. An object has finite support if some finite $F\subseteq A$ has the property that every permutation fixing $F$ pointwise fixes the object. Retain objects all of whose membership descendants have finite support, stopping the hereditary recursion at the atomic self-loops. This gives the hereditarily finite-supported Quine-atom model $\mathcal{H}$; each $q_a$ belongs to it, with support $\{q_a\}$.

Extensionality persists because every retained object's members are retained. Empty set, pairing, infinity and union preserve hereditary finite support. For separation on a retained set $x$, the union of finite supports for $x$ and the formula's parameters supports the separated extension: permutations fixing those supports preserve satisfaction in $\mathcal{H}$. All its members are retained, so its representative is retained. For replacement, the same support fixes the functional range, because an automorphism must take the unique output at an input to the unique output at its transported input. Ambient replacement bounds that range; all its members are in $\mathcal{H}$, so its representative belongs to $\mathcal{H}$. Finally, the collection of all retained subset representatives of $x$ is an ambient set, contained in the full interpreted power set of $x$. A support of $x$ permutes this collection onto itself, and its members are retained. Its representative is therefore the internal power set in $\mathcal{H}$. This verifies every ZF axiom except foundation; foundation still fails at each $q_a$.

The atom set $A$ and the family $[A{]}^2$ of its two-element subsets have empty support and are retained. Suppose a choice function $f$ on $[A{]}^2$ were retained, with finite support $F$. Choose distinct $q_a,q_b$ outside $F$ and transpose them. The transposition fixes $f$ and fixes the unordered pair $\{q_a,q_b\}$, but moves whichever of its two members $f$ selects. Equivariance would require that selected member to be fixed, a contradiction. HenceThe full universe $W$ gives the corresponding positive-choice model. Choice is therefore independent of ZF without foundation. Unlike a permutation model with ordinary urelements, this model retains full pure-set extensionality: the atomic objects are self-membered sets, not empty objects exempted from extensionality.

The constructible-universe interpretation gives $\mathrm{Con}(\mathrm{ZF})\Rightarrow \mathrm{Con}(\mathrm{ZFC})$. Thus the consistency assumptions in both displayed conclusions can equivalently be taken to be $\mathrm{Con}(\mathrm{ZF})$; no additional consistency strength is being used.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

All consistency assertions here are relative: begin with a model of ZFC, obtainable from a model of ZF by its constructible universe as proved below. First use the Rieger-Bernays permutation model. Let $\pi$ exchange the old empty set with its old singleton and fix every other object, and defineAn old set $b$ is the extension, in the new relation, of ${\pi }^{-1}(b)$. This immediately verifies extensionality and gives explicit representatives for the new empty set, pairs, unions and power sets: the old extensions required are respectively $\varnothing$, $\{a,b\}$, ${\bigcup }_{u\in \pi (a)}\pi (u)$, and $\{{\pi }^{-1}(c):c\subseteq \pi (a)\}$. Translate any formula by replacing membership by $E$; old separation and replacement then give the desired new subsets and functional ranges, whose representatives are obtained by ${\pi }^{-1}$.

For infinity, recursively form the new empty object $e={\pi }^{-1}(\varnothing )$ and successors $s(x)={\pi }^{-1}(\pi (x)\cup \{x\})$. The old replacement axiom collects the sequence $e,s(e),s^2(e),\dots$; the representative of its range is a new inductive set. The old object $q=\varnothing$ has new extension $\pi (q)=\{q\}$, so $qEq$ and its singleton witnesses failure of the Axiom of foundation. Choice survives this full permutation construction: old choice applied to a family of nonempty new extensions selects its members, and new ordered pairs and a representative of their old set give the new choice function. Thus $\mathsf{ZF}-\mathsf{Foundation}+\mathsf{AC}+\neg \mathsf{Foundation}$ is relatively consistent. A well-founded starting model gives the opposite possibility for foundation.

To make choice fail, a symmetry restriction is essential. Here is an explicit pure-set construction with many Quine atoms. Take a countably infinite set $A$ of distinct tagged objects $a_n$. Give $a_n$ the extension $\{a_n\}$. For every subset $S$ of objects already constructed, introduce an object $c(S)$ with extension $S$, except that $c(\{a_n\})$ is defined to be $a_n$ itself. Use a disjoint tag for all other codes $c(S)$, so identical extensions have identical codes and distinct extensions have distinct codes. Iterate this operation transfinitely, taking unions at limits. Each level is an old set, and its subsets are an old set, so this is a definable class construction. Every non-atomic membership edge decreases construction rank. Atomic edges are just the prescribed self-loops. Consequently the resulting structure is extensional, has the required pairs, unions and power sets, and the old replacement axiom bounds ranks of definable functional ranges. Its pure finite ranks supply infinity.

Every permutation of $A$ extends recursively by $c(S)\mapsto c(\sigma S)$. An object is finitely supported if some finite $F\subset A$ has the property that every permutation fixing $F$ pointwise fixes that object. Retain objects all of whose members, and members' members, are finitely supported, with recursion stopping at the atomic self-loops. Call this class $N$, the hereditarily finite-supported Quine-atom model.

We must verify its set axioms, not merely declare it a symmetric model. Empty set, pairs and unions have supports given by finite unions of the supports of their arguments. For separation, a formula with finitely supported parameters and domain $a$ is invariant under permutations fixing the union of those supports; its selected extension is therefore supported, and all its elements already lie in $N$. For power set, take all codes $c(S)$ with $S\subseteq \mathrm{ext}(a)$ and $c(S)\in N$. They form an old set, by separation from the bounded code level. Permutations fixing a support of $a$ permute this entire collection, so its code is supported and belongs to $N$. For replacement, translate the relativized formula to the original universe and use old replacement to collect its unique values. Equivariance gives this range a support from the parameters and domain, and every range element lies in $N$. Infinity uses the pure natural-number construction, fixed by every atom permutation. This proves $N\models \mathsf{ZF}-\mathsf{Foundation}$.

The set $A$ and the collection of its two-element subsets have empty support and belong to $N$. Suppose the latter had a choice function $f\in N$, with finite support $F$. Choose distinct $a,b\in A\setminus F$. The transposition of $a,b$ fixes $F$, hence $f$, and fixes the unordered pair $\{a,b\}$. But it swaps whichever member $f(\{a,b\})$ selects, a contradiction. ThereforeTogether with the full permutation model satisfying choice, this proves independence of choice from ZF without foundation, using the same replacement of atoms by self-membered pure sets. The negated-choice model also fails foundation; this suffices for independence over the foundation-free base.

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 restricted axiom of choice ${\mathsf{AC}}_X(Y)$ says that for every $X$-indexed family $(A_x{)}_{x\in X}$ of nonempty subsets of $Y$, there is a choice function $c:X\to Y$ such that $c(x)\in A_x$ for every $x\in X$.

Assume the axiom of choice and suppose a poset satisfying the hypothesis has no maximal element. Fix a choice function on its nonempty subsets. By transfinite recursion, choose at each ordinal stage an upper bound of the chain in a partial order already constructed, then choose a strictly larger member. Both choices are available, including the initial empty stage. This produces distinct members throughout the Hartogs ordinal of $P$, contradicting the Hartogs theorem. Thus a maximal element exists. Conversely, apply Zorn's lemma to partial choice functions on a family of nonempty sets, ordered by extension. A chain in a partial order has the compatible union as an upper bound, and a maximal element must be defined on the whole family, since one missing value could be adjoined.

Zorn's lemma was introduced in 1935 to shorten algebra proofs using choice or the well-ordering theorem.^[ref]

For sets $X$ and $Y$, ${\mathsf{AC}}_X(Y)$ says that every $X$-indexed family $(A_x{)}_{x\in X}$ of nonempty subsets of $Y$ has a choice function $c:X\to Y$ satisfying $c(x)\in A_x$.