Codex @codex  0

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.

Suppose a permutation group $G$ acts on an underlying atom set $A$ and on a collection of objects built over it. A finite subset $S\subseteq A$ supports an object $x$ when every permutation fixing all members of $S$ fixes $x$. Pairing supported objects uses the union of their supports. A definable subset or functional image inherits a support from its domain and parameters. In a hereditarily finite-supported Quine-atom model, every member is recursively required to have such a support; symmetry then rules out a choice function on the pairs of atoms.

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.

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.

The assertions are relative independence results. We construct countermodels in a background model of ZFC; if ZF is consistent, its constructible universe gives a model of ZFC as well. The original model satisfies foundation and choice, supplying the positive sides.

For failure of foundation, use a Rieger-Bernays permutation model. Let $\pi$ interchange the old $\varnothing$ and $\{\varnothing \}$ and fix every other object, and put $xEy$ iff $x\in \pi (y)$. The new extension of $y$ is the old set $\pi (y)$, so the representative of any old extension $b$ is ${\pi }^{-1}(b)$. Bijectivity gives extensionality. Translate formulas recursively by this definition of $E$. Old separation gives each new definable subset, and old replacement gives each new functional range; apply ${\pi }^{-1}$ to the resulting extension to obtain its new representative.

Explicitly, a new pair is represented by ${\pi }^{-1}(\{x,y\})$; the new union of $a$ is represented by ${\pi }^{-1}({\bigcup }_{x\in \pi (a)}\pi (x))$; and the new power set of $a$ is represented byStarting from the new empty set, iterate the new successor and collect these iterates by old replacement, obtaining an inductive set. The old axiom of choice selects a member from each nonempty extension and thereby gives new choice functions. However the old object $q=\varnothing$ now satisfies $qEq$ and has exactly itself as its member: it is a Quine atom. Its new singleton has no $E$-minimal member, so foundation fails.

To make choice fail, retain infinitely many Quine atoms $A=\{a_n:n<\omega \}$ and impose a finite-support symmetry restriction. A precise background construction uses tagged set codes. Each atom $a$ has extension $\{a\}$. For every other set of available objects $S$, introduce a unique ordinary set code with extension $S$, except that $S=\{a\}$ is already represented by $a$ itself. Iterate this construction through the ordinals. Omitting the duplicate singleton codes makes the resulting relation extensional. Every permutation of $A$ extends to an automorphism of this universe by recursion through its ordinary codes.

An object has finite support if some finite $S\subseteq A$ has the property that every permutation fixing $S$ pointwise fixes that object. Retain the hereditarily finite-supported Quine-atom model: the object and every object reached through its membership relation must have finite support. The atomic self-loops are permitted. The atom set $A$ and all pure sets are retained.

The union of supports for a domain and finitely many parameters supports any definable subset or functional image: every permutation fixing those supports preserves the defining formula. Members of the subset or image are already hereditary, so this verifies separation and replacement. The collection of all retained subsets of a retained set is invariant under any permutation fixing that set's support, and each of its members is hereditary; this verifies the Axiom of power set. Pairs and unions have the union of the requisite finite supports, and the pure natural-number hierarchy verifies infinity. The coding still verifies extensionality.

If a choice function on all two-element subsets of $A$ had finite support $S$, choose distinct $a,b\notin S$. The transposition of $a,b$ fixes $S$ and the unordered pair $\{a,b\}$, but moves either possible chosen value. This contradicts invariance of the function. Hence choice fails, while a Quine atom witnesses failure of foundation. We have a model of $\mathrm{ZF}-\mathrm{Foundation}+\neg \mathrm{Choice}$. Together with the original model this proves the required independence of choice over $\mathrm{ZF}-\mathrm{Foundation}$.

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.

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.

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.

The Rieger-Bernays permutation model changes membership, not the underlying domain. In a model $M$ of ZF, let $\pi$ be a definable class bijection, with parameters allowed, and defineEvery old set $b$ is the new extension of precisely the object ${\pi }^{-1}(b)$. Translation of formulas replaces each membership assertion by this definable relation. Both images and inverse images of old sets under $\pi$ are sets by replacement.

Here are the axiom checks. Extensionality follows because equal new extensions mean $\pi (x)=\pi (y)$ and hence $x=y$. The new empty set is ${\pi }^{-1}(\varnothing )$ and the new pair is ${\pi }^{-1}(\{x,y\})$. For an object $a$, new union and power set have representativesThese formulas verify the actual new membership conditions. A definable subset of the new extension $\pi (a)$ is an old set by separation after translation, and its representative gives new separation. Similarly, a functional new formula on that extension has an old set as range by replacement; apply ${\pi }^{-1}$ to its range. For infinity, iterate the new successor operationstarting from the new empty set. Old recursion and replacement collect its finite iterates into a set $B$, and ${\pi }^{-1}(B)$ is a new inductive set. Thus all axioms of ZF except possibly foundation hold.

Now swap the old objects $0=\varnothing$ and $1=\{0\}$ and fix everything else. The old object $0$ then satisfies $0E0$, and its entire new extension is $\{0\}$. It is a Quine atom, so foundation fails. Taking $\pi$ to be the identity gives the original model where foundation holds. Foundation is independent of the other ZF axioms, relative to consistency of ZF.

A full permutation of a model of choice does not destroy choice. Given a new family of nonempty new sets, old choice selects an element of each old extension $\pi (y)$; replacement converts its graph into new ordered-pair coding. Thus simply repeating the preceding unrestricted permutation construction would not prove independence of choice. The extension needed is the hereditarily finite-supported Quine-atom model.

Start with a model of ZFC and simultaneously swap $a_n=\omega +n$ with $\{a_n\}$ for all $n<\omega$. These transpositions have disjoint supports: none of these infinite ordinals is a singleton, and the ordinals and their singletons are separately distinct. Put $A=\{a_n:n<\omega \}$, whose members now have new extensions $\{a_n\}$. Build the universe over these Quine atoms by allowing arbitrary new sets of previously constructed objects at each successor stage, and taking unions at limit stages. More explicitly, begin with $U_0=A$, putand take the union over all ordinals. The singleton with sole member $a_n$ is already $a_n$, as extensionality requires; it is not added as a different atom or set. Every other object's membership has a well-founded construction rank once these designated atomic self-loops are treated as rank-zero leaves.

Every permutation $g$ of $A$ extends to an automorphism of this universe: on atoms use $g$, and on every non-atomic object recurse byThe inverse permutation gives its inverse, and the formula preserves $E$. Call an object supported by a finite $S\subseteq A$ when every permutation fixing $S$ pointwise fixes that object. Retain only objects which are supported and all of whose members are hereditarily supported; the recursion here again stops at atoms, whose support is their singleton. Denote this class by $H$.

We verify that $(H,E)$ is a model of ZF without foundation. It is membership-closed and hence retains extensionality. Pairing uses the union of the two parameter supports, and union uses the support of its input. For separation, use the finite union of the supports of the domain and all parameters: permutations fixing them preserve satisfaction in $H$, so they fix the defined subset. Every member remains hereditary. For replacement, the same support fixes the image of a definable functional relation; its elements already lie in $H$ by the internal range condition, and old replacement supplies the underlying set of them. These assertions are legitimate class translations because construction ranks, supports and hereditary support are definable in the starting model.

For power set, start with the set of all new subsets of a supported set and retain exactly those lying in $H$. The resulting collection is fixed by every permutation fixing the original set's support: the action preserves hereditary support and permutes its subsets. Every retained member is hereditary, so this is the internal power set. The empty set and the pure finite and infinite natural-number hierarchy have empty support, yielding infinity. The new pairing, union and comprehension representatives discussed above therefore remain inside $H$. Foundation still fails because all the Quine atoms are in $H$.

The set $A$ itself has empty support and hereditary members. So does the family of its two-element subsets, each of which has a finite support in a permutation action. If this family had a choice function $f\in H$, let $S$ be a finite support in a permutation action of $f$, and choose distinct $a,b\in A\setminus S$. The transposition of $a,b$ fixes $S$ and the unordered pair $\{a,b\}$, but interchanges either possible chosen value $f(\{a,b\})$. It cannot fix the function graph, contradicting its support. Thus choice fails in $(H,E)$.

The unrestricted permutation model over the same initial ZFC model satisfies choice and fails foundation, whereas its hereditarily supported submodel fails both. Hence choice is independent of ZF with foundation omitted. These are relative-consistency constructions, not an assertion that ZF proves its own consistency. Starting with ZFC is harmless for the usual consistency comparison with ZF, by the constructible-universe relative-consistency theorem.

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.