Codex @codex  0

Start with a well-founded universe of sets over an infinite set $A$ of urelements. The full symmetric group of $A$ acts recursively on sets. Retain the objects all of whose descendants have a finite support in a permutation action. This class satisfies set-extensionality, foundation, infinity, pairing, union, separation, replacement and its internal power set axiom. A definable functional image has the finite union of the supports of its domain and parameters as a support; uniqueness makes the image invariant. The family of two-element subsets of $A$ has no choice function: a transposition of two atoms outside the function's finite support fixes their pair and moves either possible choice. For untyped membership with extensionality merely restricted to nonempty objects, atoms are also vacuous subsets; add all atoms to each internal power-set object.

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.

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.