= Solution
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.
\b[<Union>.] Put $\lambda=\beth_\omega$ and use the <hereditarily locally small membership model>
$$
B_\lambda=\{x:(\forall y\in\operatorname{TC}(\{x\}))\ |y|<\lambda\}.
$$
The 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|\leq|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 and
$$
|\mathcal P(x)|=2^{|x|}<\lambda.
$$
Consequently 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. \b[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.
\b[<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>. \b[<Power set> fails in $H_{\omega_1}$, with every other ZF <axiom> intact.]
\b[<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. \b[This instance of <replacement> fails.]
\b[<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$ \i[and the atom]. It has exactly the required extension. \b[All remaining ZF <axioms> hold, but <extensionality> fails.] In the usual typed atom theory, the power-set <axiom> instead quantifies only over set-subsets.
\b[<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 model>
$$
x\mathrel E y\quad\Longleftrightarrow\quad x\in\pi(y).
$$
Since $\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$ is
$$
\pi^{-1}\left(\bigcup_{b\in\pi(a)}\pi(b)\right).
$$
An $E$-subset of $a$ is an object $z$ with $\pi(z)\subseteq\pi(a)$, so its $E$-power-set object is
$$
\pi^{-1}\bigl(\{\pi^{-1}(u):u\subseteq\pi(a)\}\bigr).
$$
Translate 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. \b[<Foundation> fails.]
\b[<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>. \b[<Infinity> fails, and all other ZF <axioms> hold.]
\b[<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. \b[Both <choice> and its negation are relatively consistent with the stated weakening of <extensionality>.]
Back to article page
