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.

Build well-founded coded sets over a single urelement $a$ with no members, retaining a distinct empty set. Use the unmodified membership language, so both $a$ and the empty set have the same empty extension and extensionality fails. Pairs, unions, separation and functional ranges have set codes, and pure natural numbers give infinity. For the unrestricted Axiom of power set, the power-set code must contain $a$ as well as all ordinary subset codes, since the atom is vacuously a subset of every object. Rank gives foundation. Thus the other ZF axioms hold.

The independence statements are relative consistency statements. We construct models from an ambient model of ZFC; the construction is an interpretation and does not assume that the ambient model is transitive. Foundation is already true in the ordinary ambient membership structure, so its positive consistency direction is immediate.

For the negative direction, construct an extensional cumulative universe over Quine atoms. Let $A$ be a countably infinite set of formal symbols $q_a$. Give each $q_a$ the extension $\{q_a\}$. For a set $X$ of already constructed objects, let $S(X)$ be its unique representative: set $S(\{q_a\})=q_a$, and otherwise use a fresh tagged code $(1,X)$. Atom codes have a different tag. Begin with $U_0=A$ and putSet $W={\bigcup }_{\alpha }{U}_{\alpha }$. The interpreted membership relation $E$ gives $S(X)$ exactly the members $X$, and gives $q_a$ exactly the member $q_a$. This convention matters: creating a second representative for $\{q_a\}$ would violate extensionality. Every object is uniquely determined by its extension, so $E$ satisfies full extensionality. Every set-sized collection $X$ of objects has bounded construction rank, by ambient replacement, and hence has its representative $S(X)$ in $W$.

Here are the remaining axiom verifications. Empty set and pairing use $S(\varnothing )$ and $S(\{x,y\})$. If $E(y)=X$, its interpreted union is $S({\bigcup }_{x\in X}E(x))$. Its interpreted power set issince every subset extension has a unique representative. The pure, atom-free finite hierarchy supplies a copy of $\omega$ and an inductive set. For separation, translate an $E$-formula into the ambient language, with quantifiers restricted to the definable class $W$; ambient separation gives the appropriate subset of $X$, and $S$ represents it. For replacement, uniqueness in the interpreted functional relation gives an ambient definable functional image of the set $X$. Ambient replacement makes that image set-sized, and $S$ again represents it. These arguments also establish that all the operations used have bounded construction rank.

Ambient choice gives choice in $W$: choose a member from each nonempty extension in a set-sized family and represent the graph, using interpreted ordered pairs. But $q_{a}E{q}_a$, and the nonempty set with extension $\{q_a\}$ has no $E$-minimal member. ThusTogether with the ordinary model, this proves independence of foundation from the other ZF axioms, even when choice is retained.

To extend the construction to failure of choice, let the full permutation group of $A$ act on $W$ byThe singleton convention is equivariant, so this is an automorphism of $(W,E)$. An object has finite support if some finite $F\subseteq A$ has the property that every permutation fixing $F$ pointwise fixes the object. Retain objects all of whose membership descendants have finite support, stopping the hereditary recursion at the atomic self-loops. This gives the hereditarily finite-supported Quine-atom model $\mathcal{H}$; each $q_a$ belongs to it, with support $\{q_a\}$.

Extensionality persists because every retained object's members are retained. Empty set, pairing, infinity and union preserve hereditary finite support. For separation on a retained set $x$, the union of finite supports for $x$ and the formula's parameters supports the separated extension: permutations fixing those supports preserve satisfaction in $\mathcal{H}$. All its members are retained, so its representative is retained. For replacement, the same support fixes the functional range, because an automorphism must take the unique output at an input to the unique output at its transported input. Ambient replacement bounds that range; all its members are in $\mathcal{H}$, so its representative belongs to $\mathcal{H}$. Finally, the collection of all retained subset representatives of $x$ is an ambient set, contained in the full interpreted power set of $x$. A support of $x$ permutes this collection onto itself, and its members are retained. Its representative is therefore the internal power set in $\mathcal{H}$. This verifies every ZF axiom except foundation; foundation still fails at each $q_a$.

The atom set $A$ and the family $[A{]}^2$ of its two-element subsets have empty support and are retained. Suppose a choice function $f$ on $[A{]}^2$ were retained, with finite support $F$. Choose distinct $q_a,q_b$ outside $F$ and transpose them. The transposition fixes $f$ and fixes the unordered pair $\{q_a,q_b\}$, but moves whichever of its two members $f$ selects. Equivariance would require that selected member to be fixed, a contradiction. HenceThe full universe $W$ gives the corresponding positive-choice model. Choice is therefore independent of ZF without foundation. Unlike a permutation model with ordinary urelements, this model retains full pure-set extensionality: the atomic objects are self-membered sets, not empty objects exempted from extensionality.

The constructible-universe interpretation gives $\mathrm{Con}(\mathrm{ZF})\Rightarrow \mathrm{Con}(\mathrm{ZFC})$. Thus the consistency assumptions in both displayed conclusions can equivalently be taken to be $\mathrm{Con}(\mathrm{ZF})$; no additional consistency strength is being used.

Independence here is a relative consistency assertion: from a ground first-order model satisfying ZFC, construct a first-order model of each remaining theory in which the omitted axiom fails. The ground axiom of choice is a tool for constructing these countermodels, not an extra axiom imposed on the theories being tested. The constructible universe supplies the usual relative-consistency implication from ZF to ZFC, so this ground choice assumption requires no additional consistency strength. These constructions can be formalized inside an arbitrary ground model; they do not require the stronger assumption that a transitive model exists.

Union. Put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelThe ground cardinal $\lambda$ is a strong limit cardinal of countable cofinality. This transitive class contains the empty set and $\omega$. Pairing preserves the bound, as does taking a subset, so separation holds for every formula relativized to this class. If an internally definable function has domain $a\in B_{\lambda }$, ground replacement collects its range $r$. Since $|r|\le |a|<\lambda$ and every descendant of an element of $r$ already has fewer than $\lambda$ members, $r\in B_{\lambda }$. Thus the full functional Axiom schema of replacement holds. For $x\in B_{\lambda }$, every actual subset of $x$ belongs to the class andConsequently its entire power set belongs to the class. Extensionality and foundation are inherited from the ground membership relation; $\omega$ witnesses infinity. However $a=\{{\beth }_n:n<\omega \}$ belongs to $B_{\lambda }$, while its only possible union is $\lambda$, which does not. All the other ZF axioms hold, and union fails. Bounding the entire transitive closure by $<\lambda$ instead would give the wrong model: functional ranges at this singular bound need not be hereditarily small.

Power set. Use the transitive class $H_{{\omega }_1}$ of hereditarily countable sets. Pairing, union and separation preserve hereditary countability. A functional image of a countable domain is countable, and its members have countable transitive closures; their countable union is countable in the ground ZFC model. This proves replacement. The remaining structural axioms and infinity are inherited. Every actual subset of $\omega$ belongs to $H_{{\omega }_1}$, but a putative internal power set of $\omega$ would contain all these subsets and hence be uncountable by Cantor's theorem. Power set fails in $H_{{\omega }_1}$, with every other ZF axiom intact.

Replacement. Use $V_{\omega +\omega }$ in the cumulative hierarchy. At a limit ordinal cutoff, pairing, union, power set and every instance of separation remain below the cutoff; foundation, extensionality and infinity hold as well. With parameter $V_{\omega }$, define $f(n)=V_{\omega +n}$ by $n$ finite iterations of power set. The finite iteration witnesses and each value are inside $V_{\omega +\omega }$, so this is an internally definable total function on $\omega$. Its range has rank of a set $\omega +\omega$ and is absent from the model. This instance of replacement fails.

Extensionality. Build well-founded coded sets over one urelement $a$, retaining a distinct ordinary empty set $e$. Membership of an atom is always false, and membership of a set code is its coded extension. Thus $a\ne e$ but they have identical empty extensions. Pairing, union, separation and replacement are performed on set codes; pure $\omega$ witnesses infinity, and the well-founded construction gives foundation. There is a small point concerning the unmodified, untyped Axiom of power set: the atom is vacuously a subset of every object. Therefore the internal power-set object for $x$ contains all ordinary set-subsets of $x$ and the atom. It has exactly the required extension. All remaining ZF axioms hold, but extensionality fails. In the usual typed atom theory, the power-set axiom instead quantifies only over set-subsets.

Foundation. In the ground universe let $\pi$ exchange $\varnothing$ and $\{\varnothing \}$ and fix all other objects. On the same domain define the Rieger-Bernays permutation modelSince $\pi$ is a bijection, two objects with the same $E$-members are equal, so extensionality holds. Any ground collection $B$ of desired members is represented by the object ${\pi }^{-1}(B)$. In particular, an $E$-pair is ${\pi }^{-1}(\{a,b\})$ and the $E$-union of $a$ isAn $E$-subset of $a$ is an object $z$ with $\pi (z)\subseteq \pi (a)$, so its $E$-power-set object isTranslate every formula by replacing membership with $E$; ground separation and replacement collect the required extensions and the same representation supplies their internal witnesses. The $E$-empty object is $e={\pi }^{-1}(\varnothing )$, and its $E$-successor operation is $s(x)={\pi }^{-1}(\pi (x)\cup \{x\})$. Ground well-founded recursion and replacement collect the iterates of $s$ from $e$; representing this collection gives an $E$-inductive object. Thus infinity holds. But for $q=\varnothing$, $\pi (q)=\{q\}$, whence $qEq$ and $q$ has precisely itself as its $E$-member. Foundation fails.

Infinity. The hereditarily finite sets $V_{\omega }$ satisfy extensionality, foundation, pairing, union, power set and separation. Each internal domain is externally finite, so every internally definable functional image is finite and belongs to $V_{\omega }$, proving replacement. No finite object can contain the empty set and all its successive Finite von Neumann ordinals. Infinity fails, and all other ZF axioms hold.

Choice with atoms. For the negative model use the Basic Fraenkel permutation model. Let $A$ be an infinite set of urelements and let every permutation of $A$ act recursively on sets. Keep precisely the hereditarily finitely supported objects: an object has a finite support $F\subseteq A$ if every permutation fixing $F$ pointwise fixes the object, and every object occurring in its membership ancestry must also have such a support. The class of these objects contains the pure universe and $A$ itself.

Supports for a pair are united; union preserves a support; a formula defining a subset uses the finite union of the supports of its domain and parameters. An internally definable functional range has the same support, since its values are uniquely specified, and its elements are already hereditarily supported. This proves the full separation and replacement schemas. All hereditarily supported set-subsets of a fixed set form its symmetric internal power set; this collection is invariant under the pointwise stabilizer of a support of the original set. For the untyped version add all the atoms, as above. Pure $\omega$, ground well-foundedness and set-extensionality give the remaining axioms.

The family $[A{]}^2$ of unordered pairs of atoms is hereditarily supported. If it had a choice function $f$, let $F$ be a finite support of $f$. Choose distinct $a,b\in A\setminus F$. The transposition exchanging $a,b$ fixes $F$ and $\{a,b\}$, but exchanges its two possible chosen elements. Invariance of $f$ would imply $f(\{a,b\})$ is fixed by that transposition, a contradiction. Conversely, the full well-founded universe over the atoms, before restricting to finite supports, satisfies choice when the ground universe does. Both choice and its negation are relatively consistent with the stated weakening of extensionality.

All assertions of independence below are relative consistency assertions. We construct structures satisfying the other ZF axioms but falsifying the indicated axiom; an ordinary model of ZF supplies the positive side. The convenient ground theory is ZFC, which has the same consistency strength as ZF by the constructible universe theorem.

For the Axiom of union, put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelIt is a transitive class. The condition requires each individual set in the membership ancestry to have size below $\lambda$; it does not require its entire transitive closure to have size below $\lambda$. Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and $\omega$ witnesses infinity. For $x\in B_{\lambda }$, the actual $\mathcal{P}(x)$ also belongs to $B_{\lambda }$: if $|x|=\mu <\lambda$, then $2^{\mu }<\lambda$ by the strong-limit property, while every subset of $x$ and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain $x\in B_{\lambda }$, ground replacement, applied to the relativized first-order formula, gives its range $r$. Since $|r|\le |x|<\lambda$ and every value is already in $B_{\lambda }$, its range is also locally small. Thus every replacement instance holds.

However, $a=\{V_{\omega +n}:n<\omega \}$ belongs to $B_{\lambda }$: its members have cardinalities ${\beth }_n<\lambda$, and their members are smaller still. Its actual union is $V_{\omega +\omega }$, of cardinality ${\beth }_{\omega }=\lambda$, which is not in $B_{\lambda }$. Transitivity makes any internal union witness equal to this actual union. Hence Union fails while all the other ZF axioms hold.

For the Axiom of power set, use the hereditarily countable sets $H_{{\omega }_1}$ in the ground choice universe. This is transitive and contains $\omega$. Pairs, subsets and unions have countable transitive closure. For replacement, a functional image of a countable domain is countable, and the union of countably many countable transitive closures is countable; hence that image is again hereditarily countable. These observations, with inherited extensionality and foundation, verify all the remaining axioms. Every real, viewed as a subset of $\omega$, belongs to $H_{{\omega }_1}$. A power-set witness for $\omega$ would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas $\mathcal{P}(\omega )$ is uncountable by Cantor's theorem. Power set fails.

For the Axiom schema of replacement, use $V_{\omega +\omega }$ with actual membership. This limit-rank structure contains $\omega$ and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below $\omega +\omega$. A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable functionis obtained by $n$ successive power-set operations starting with the parameter $V_{\omega }$. Each finite iteration, including its finite history, belongs to the structure. Its range has rank $\omega +\omega$ and is not an element of $V_{\omega +\omega }$. Thus the replacement instance for this first-order formula fails, although every other ZF axiom holds.

For the axiom of extensionality, take the well-founded cumulative set universe over two distinct urelements, and forget the predicate distinguishing urelements from sets. Each urelement has no members, just as the ordinary empty set has no members, so extensionality fails. Every other axiom survives in this pure membership language. Pairing, union, separation and replacement are witnessed by the corresponding ordinary sets of urelements and sets; foundation follows from their well-founded ranks, and the pure $\omega$ supplies infinity. Here foundation is written with “has a member” as its nonemptiness antecedent, and disjointness means having no common member. Formulations using inequality to one designated empty object are not equivalent after removing extensionality. There is also one necessary adjustment to power set: an urelement is vacuously a subset of every object because it has no members. Thus the power-set witness for $x$ is the ordinary set of all usual subsets of its extension, together with both urelements. This is still a set, and contains exactly the objects satisfying the unrestricted subset first-order formula. Consequently the countermodel falsifies Extensionality alone, without silently weakening Power set to sets only.

Finally, the hereditarily finite sets $V_{\omega }$ satisfy extensionality, foundation, pairing, union, power set and separation. Every functional image of a finite domain is a finite set of hereditarily finite objects, hence also belongs to $V_{\omega }$, giving all replacement instances. No finite set contains $\varnothing$ and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.

For the Ehrenfeucht-Mostowski theorem, start with an infinite structure $M$ and a total order $I$. Choose a Skolem expansion $M^{\ast }$, and adjoin constants $c_i$ for $i\in I$. Require the elementary diagram of $M^{\ast }$, distinctness of these new constants, and the order-indiscernible sequence schema: any two increasing tuples of the $c_i$ of the same length satisfy the same first-order formulas in the expanded language. Every finite fragment mentions finitely many new constants and finitely many first-order formulas. Enumerate a countably infinite subset of $M$. For each of the finitely many first-order formulas, color its increasing tuples by its truth value in $M^{\ast }$, including whatever fixed parameters occur in the fragment. Successive applications of the infinite Ramsey theorem leave an infinite subset homogeneous for all these colorings. Assign the finitely many new constants to distinct elements of this subset in their index order. Their finite indiscernibility requirements and the elementary diagram are then simultaneously satisfied.

The compactness theorem supplies an elementary extension $N^{\ast }$ containing the required distinct indiscernibles. Their Skolem hull is an elementary substructure: an existential first-order formula true of its elements has its chosen Skolem-function witness in the hull, so the Tarski-Vaught test applies. Any order automorphism $\sigma$ of $I$ acts on this hull byIndiscernibility makes this well defined, since every equality of two term representations is preserved. The same argument preserves every first-order formula; the inverse is given by ${\sigma }^{-1}$. Thus it is an automorphism, uniquely determined in the language of the chosen Skolem expansion by its values on the generators. This proves both the indiscernible-model and automorphism forms of the Ehrenfeucht-Mostowski theorem. Uniqueness is not claimed for automorphisms of the reduct which need not preserve the chosen Skolem functions.

For simple typed set theory with atoms, write $S_i$ for the set predicate at sort $i$. Members have sort one lower; urelements have no typed members, extensionality applies to sets, and every well-typed first-order formula defines a set at the next sort. Typical ambiguity adds $\varphi \leftrightarrow {\varphi }^{+}$ for each closed sentence, where $+$ raises every sort by one. We prove finite satisfiability using Ramsey theorem, rather than assuming that adjacent sorts have the same cardinality.

Let $X_n=V_{\omega +2n}$. If $n<m$, then $\mathcal{P}(X_n)\subseteq X_m$. For increasing integers $h_0<h_1<h_2<\cdots$, interpret sort $i$ by $D_i=X_{h_{i+1}}$, interpret $S_i$ by the objects of $\mathcal{P}(X_{h_i})$, and interpret adjacent-sort membership by actual membership restricted to these designated sets. All other objects of a sort are typed urelements. Every subset of $D_i$ is a designated set in $D_{i+1}$, so comprehension holds for every first-order formula, including first-order formulas with quantifiers and parameters at other sorts. Two designated sets with the same members are equal, while the other objects have no typed members. Thus this is a full model of the typed axioms for every increasing sequence of levels. The extra preceding level $h_0$ gives a consistent interpretation of the bottom set predicate as well.

Take finitely many ambiguity sentences and let $r$ bound their highest sort before raising. Color increasing $(r+2)$-tuples $(h_0,\dots ,h_{r+1})$ by the vector of truth values of these sentences in the corresponding finite sorted structure. There are finitely many colors. The infinite Ramsey theorem supplies an homogeneous set of indices. Choose the level sequence from it. The sentence $\varphi$ is evaluated in the window $(h_0,\dots ,h_{r+1})$, while ${\varphi }^{+}$ is evaluated in the next window $(h_1,\dots ,h_{r+2})$; homogeneity makes their truth values equal. Sentences using fewer sorts simply ignore the unused final levels. Thus every finite family of ambiguity axioms has a model satisfying all the typed axioms. Apply many-sorted first-order compactness theorem to obtainThis is a relative consistency construction in the ordinary set-theoretic metatheory. Allowing urelements is essential here: skipping ranks leaves objects outside the represented power sets, and those objects must be permitted as urelements.