= Solution
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 $x\mathrel E y$ 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 by
$$
\pi^{-1}\bigl(\{\pi^{-1}(b):b\subseteq\pi(a)\}\bigr).
$$
Starting 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 $q\mathrel E q$ 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}$.
Back to article page
