= Solution
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> by
$$
\boxed{x\mathrel E y\quad\Longleftrightarrow\quad x\in\pi(y).}
$$
Write $S(b)=\pi^{-1}(b)$; the $E$-members of $S(b)$ are exactly the old members of $b$. In particular $a\mathrel E a$, 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$ is
$$
S\left(\bigcup\{\pi(x):x\in\pi(y)\}\right).
$$
Its elements are precisely objects with an $E$-membership chain of length two into $y$. The $E$-power <set> of $y$ is
$$
S\left(\{S(b):b\subseteq\pi(y)\}\right),
$$
since $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):\varphi^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 proved
$$
\boxed{\operatorname{Con}(\mathsf{ZF})\Rightarrow
\operatorname{Con}(\mathsf{ZF}-\mathsf{Foundation}+\neg\mathsf{Foundation}),}
$$
with <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 define
$$
D_{\alpha+1}=D_\alpha\cup\{(1,X):X\subseteq D_\alpha,
\ X\ne\{q\}\text{ for every }q\in A\},\qquad
D_\lambda=\bigcup_{\alpha<\lambda}D_\alpha.
$$
The 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''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,\ldots,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 of
$$
\{S(Y):Y\subseteq\operatorname{ext}(x),\ S(Y)\in H\}.
$$
It 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. Thus
$$
\boxed{H\models\mathsf{ZF}-\mathsf{Foundation}
+\neg\mathsf{Foundation}+\neg\mathsf{AC}.}
$$
The 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.
Back to article page
