Hereditarily finite-supported Quine-atom model

ID: hereditarily-finite-supported-quine-atom-model

Build the cumulative universe over an infinite set of Quine atoms, and extend every permutation of recursively to its other sets. An object has finite support if every permutation fixing that finite subset of 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 : swap two atoms outside its supposed finite support, fixing their unordered pair but interchanging either possible selected member.

New to topics? Read the docs here!