 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 $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}$.