= Hereditarily finite-supported Quine-atom model
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.
Back to article page
