Quine atom ($q=\{q\}$)

A Quine atom is a set whose sole member is itself. It violates the Axiom of foundation while respecting the axiom of extensionality. Swapping pairwise distinct old objects $a_n$ with their singletons in a Rieger-Bernays permutation model supplies many Quine atoms, provided those transpositions have disjoint supports. For example, the old ordinals $a_n=\omega +n$ and their singletons are disjoint families.

Start with distinct formal atoms $q\in A$ with membership extensions $\{q\}$. Recursively adjoin a unique representative $S(X)$ of every subset $X$ of a previous stage, except that $S(\{q\})=q$ uses the atom already present. Define membership by these extensions. Each set-sized collection of objects has bounded construction rank, so it has a representative at a later stage. This gives full extensionality, unlike adjoining an ordinary singleton distinct from a Quine atom. Definable subsets and ranges, unions and power sets are set-sized collections in the ambient model and hence have representatives. The pure finite hierarchy supplies infinity. Every permutation of the atoms extends recursively; hereditary finite support restriction gives the hereditarily finite-supported Quine-atom model, whose two-element atom subsets have no choice function.

Build the cumulative universe over an infinite set $A$ of Quine atoms, and extend every permutation of $A$ recursively to its other sets. An object has finite support if every permutation fixing that finite subset of $A$ fixes the object. Retain objects whose members, recursively away from the atomic self-loops, also have finite support. Parameters and domains give finite supports for definable subsets and functional ranges; the collection of all retained subsets of a retained set is again supported. These observations verify separation, replacement and power set, and the pure natural-number hierarchy gives infinity. There is no choice function on the two-element subsets of $A$: swap two atoms outside its supposed finite support, fixing their unordered pair but interchanging either possible selected member.