= Extensional cumulative universe over Quine atoms
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>.
Back to article page
