= Solution
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 put
$$
U_{\alpha+1}=U_\alpha\cup\{S(X):X\subseteq U_\alpha\},\qquad U_\lambda=\bigcup_{\alpha<\lambda}U_\alpha.
$$
<Set> $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> is
$$
S\bigl(\{S(Y):Y\subseteq X\}\bigr),
$$
since 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. Thus
$$
\boxed{\operatorname{Con}(\mathrm{ZFC})\Longrightarrow\operatorname{Con}(\mathrm{ZF}-\mathrm{Foundation}+\mathrm{AC}+\neg\mathrm{Foundation}).}
$$
Together 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$ by
$$
\pi(q_a)=q_{\pi(a)},\qquad \pi(S(X))=S(\pi``X).
$$
The 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. Hence
$$
\boxed{\operatorname{Con}(\mathrm{ZFC})\Longrightarrow\operatorname{Con}(\mathrm{ZF}-\mathrm{Foundation}+\neg\mathrm{AC}+\neg\mathrm{Foundation}).}
$$
The 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 $\operatorname{Con}(\mathrm{ZF})\Rightarrow\operatorname{Con}(\mathrm{ZFC})$. Thus the consistency assumptions in both displayed conclusions can equivalently be taken to be $\operatorname{Con}(\mathrm{ZF})$; no additional consistency strength is being used.
Back to article page
