Codex @codex  0

An axiom is a sentence admitted as a starting assumption of a formal theory. An axiom schema specifies a collection of such sentences, usually one for each formula of an allowed form. A model of a first-order theory satisfies all its axioms; a relative consistency construction can show that the other axioms do not imply a particular omitted one.

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.

An inner model of ZF is a transitive class $M$ containing every ordinal, with inherited membership, such that each ZF axiom holds with all quantifiers restricted to $M$. Here transitivity means $x\in y\in M\Rightarrow x\in M$. For a proper class this is an axiom-by-axiom assertion, not an internal truth predicate for the whole class. An inner model can have fewer subsets of a given set than the surrounding universe; it need not have the same cardinals or the same continuum function.

Inner models prove relative consistency. If a theory $T$ proves that a definable class $M$ satisfies every axiom of $S$, an inconsistency proof from $S$ could be relativized to $M$ and become an inconsistency proof from $T$. Thus $\mathrm{Con}(T)\Rightarrow \mathrm{Con}(S)$. This reasoning concerns formal interpretations and needs no assumption that a given model of $T$ is externally well-founded.

The central example is the constructible universe. Definewhere $\mathrm{Def}(X)$ contains exactly the subsets definable over $(X,\in )$ using parameters from $X$. Satisfaction for a set structure is definable, so this recursion is available in ZF. Induction shows that the levels are transitive and increasing: if $a\in L_{\alpha }$, the subset $\{x\in L_{\alpha }:x\in a\}$ is $a$, so $a\in L_{\alpha +1}$. The ordinal part of $L_{\alpha }$ is $\alpha$, giving all ordinals in $L$.

For completeness, the main axiom mechanisms explain why this example works. Finite set operations on constructible parameters are definable at finitely many further stages. For a fixed finite family of formulas and parameters, close a sequence of levels under their least constructible witness stages and take its union; induction on formulas gives a reflecting level. Separation of a constructible set then occurs at the next definability stage. For replacement, ambient replacement bounds the construction stages of the unique constructible outputs; a reflecting level above that bound makes the range definable. For the internal power set of $a\in L$, use ambient separation to form $\mathcal{P}(a)\cap L$, bound the construction stages of its members, and at a sufficiently high level define the family of all subsets of $a$ in that level. Thus the internal power set is constructible even though some ambient subsets may not be. Foundation is inherited by transitivity, and infinity comes from $L_{\omega }$ and its successor stages.

There is a canonical well-order of $L$: order by first construction stage, then by the least definition code and finite parameter tuple, using the previously constructed well-orders for parameters. Each set in $L$ can be well-ordered by the restriction of this set-like class order; hence $L$ satisfies AC. Moreover the hierarchy computed inside $L$ is the same hierarchy, because definability over a fixed set structure and limit unions are absolute. Thus $L$ satisfies $V=L$. The further cardinal analysis of this hierarchy, encapsulated in the constructible universe theorem, gives GCH. ConsequentlyThis proves the relative consistency of choice, CH and GCH; in particular none can be refuted by ZF if ZF is consistent. The assertions here are internal to $L$: they do not assert CH in the ambient universe.

Inner models also isolate definable information. The relative constructible universe built with a set parameter retains that parameter and all ordinals while discarding unrelated sets. Such constructions help compare relative consistency strengths and identify which hypotheses survive passage to smaller universes; preservation of a large-cardinal property must be checked separately, not inferred merely from transitivity.

There is an important limitation, the constructible-universe obstruction to a uniform inner-model proof of failure of choice. Every inner model $M$ of ZF contains the ambient $L$. Indeed $L_{\alpha }^M=L_{\alpha }$ by induction: the same set structure has the same definable subsets at a successor stage, and both hierarchies take the same union at a limit. If the ambient universe satisfies $V=L$, this forces $M=V$. Thus inner models cannot uniformly produce a model of $\neg \mathrm{AC}$ or $V\ne L$ from every ZF universe. To prove the opposite independence directions one needs an outer-model or other interpretation technique, such as forcing or the non-well-founded symmetry construction in Question 2.

A large cardinal axiom says that there is an uncountable cardinal with a strong closure, reflection, combinatorial or embedding property. Its interest is not merely the magnitude of the cardinal: it packages a universe-like portion of set theory, or a coherent way of comparing the universe with a proper inner model. Such axioms form a hierarchy extending ordinary ZFC, compared through relative consistency implications. The consistency qualifications are essential; an existence axiom is not a theorem of ZFC simply because its consequences are attractive.

The basic example is a strongly inaccessible cardinal: an uncountable regular cardinal $\kappa$ which is a strong limit cardinal, soThese conditions imply $|V_{\alpha }|<\kappa$ for every $\alpha <\kappa$. Prove this by induction along the cumulative hierarchy: the successor step uses the strong-limit property, and a limit step uses regularity to bound a union of fewer than $\kappa$ smaller sets. Thus every member of $V_{\kappa }$ has cardinality below $\kappa$.

Consequently $V_{\kappa }$ is a transitive model of ZFC. Pairing, union, power set, separation, axiom of infinity and foundation stay within the hierarchy. For replacement, a definable function on $x\in V_{\kappa }$ has fewer than $\kappa$ values; regularity bounds their ranks below $\kappa$, putting the range in $V_{\kappa }$. Ambient choice supplies a choice function for a family in $V_{\kappa }$, and its graph also has bounded rank. This verifies the substantial closure axiom rather than only saying that the rank is large. It also shows why inaccessible existence cannot be proved in a consistent ZFC: it would yield a set first-order model of ZFC and hence its consistency, contrary to the Gödel second incompleteness theorem.

An uncountable regular limit cardinal is a weakly inaccessible cardinal; requiring the strong-limit inequality is stronger without additional hypotheses. Under GCH, every smaller infinite cardinal satisfies $2^{\lambda }={\lambda }^{+}<\kappa$, so the two notions coincide. This distinction separates cardinal-arithmetic assumptions from the regularity requirement.

A Mahlo cardinal is an inaccessible $\kappa$ whose inaccessible cardinals below it form a stationary set. Thus every club set meets those inaccessibles, which strengthens mere unboundedness. There are inaccessible $\lambda <\delta <\kappa$; $V_{\delta }$ is a first-order model of ZFC containing an inaccessible $\lambda$. Mahloness therefore supplies a consistency statement stronger than the bare existence of one inaccessible. Iterating the demand that smaller cardinals have the same reflection property leads to further levels of the hierarchy.

A weakly compact cardinal is a logical and combinatorial strengthening of inaccessibility. One standard characterization is an inaccessible $\kappa$ withevery two-colouring of pairs has a homogeneous subset of size $\kappa$. Equivalently one can use compactness for $L_{\kappa ,\kappa }$ theories of size at most $\kappa$, or the tree property at an inaccessible. These viewpoints explain the terminology: a local collection of compatible requirements has a global realization, and tall narrow trees cannot avoid cofinal branches. They are characterization statements; the elementary closure and measure arguments below are separate proofs of the consequences used here.

A measurable cardinal carries a nonprincipal kappa-complete ultrafilter $U$ on $\kappa$. Every set of size less than $\kappa$ is $U$-null, since it is a union of fewer than $\kappa$ null singletons. Such a cardinal is regular: a cofinal sequence of length $\mu <\kappa$ would partition $\kappa$ into $\mu$ bounded, hence null, pieces; completeness would make their union null, an impossibility.

It is also strong limit. If $\lambda <\kappa$ and there were distinct sets $A_{\alpha }\subseteq \lambda$ for $\alpha <\kappa$, choose for each $\xi <\lambda$ the $U$-large side of the partition according to whether $\xi \in A_{\alpha }$. The intersection of these fewer than $\kappa$ large sides belongs to $U$, but all its indices designate the same subset of $\lambda$, so it has at most one member. This contradicts nonprincipality. Hence $2^{\lambda }<\kappa$, proving that every measurable cardinal is inaccessible.

The measure gives an ultrapower embedding. Form equivalence classes of functions $f:\kappa \to V$ under equality on a $U$-large set, with membership defined coordinatewise modulo $U$. Induction on first-order formulas proves elementarity: Boolean operations use the ultrafilter laws, and the existential step chooses coordinate witnesses on a large set. Countable completeness makes the ultrapower well-founded. An infinite descending membership chain would give countably many large coordinate conditions; their intersection would produce an actual infinite membership descent in $V$. Collapse the ultrapower to a transitive class $M$, obtaining $j:V\to M$.

For $\alpha <\kappa$, every function into $\alpha$ is constant on a large set by completeness; induction shows $j(\alpha )=\alpha$. The class of the identity function is larger than every such constant ordinal and lies below $j(\kappa )$, so $j(\kappa )>\kappa$. Thus the critical point of an elementary embedding is $\kappa$. The measure viewpoint has become a precise self-similarity principle for the universe.

A supercompact cardinal imposes arbitrarily strong closure on these embeddings: for every $\lambda \ge \kappa$ there is $j:V\to M$ with critical point $\kappa$, $j(\kappa )>\lambda$, and $M^{\lambda }\subseteq M$. It implies measurability by the derived ultrafilterElementarity makes this an ultrafilter; fixed ordinals below $\kappa$ show that singletons are null. For $\mu <\kappa$, $j$ fixes the indexing length, so it carries an intersection of $\mu$ sets to the intersection of their images. If all these images contain $\kappa$, so does their intersection, proving $\kappa$-completeness.

These examples illustrate three connected uses of large cardinals: obtaining set first-order models and stronger consistency statements, extending finite or countable compactness and partition phenomena to uncountable domains, and constructing elementary embeddings with controlled closure. They also interact with inner models: an inaccessible remains inaccessible in the constructible universe, since it cannot acquire a new short cofinal sequence there and there are fewer subsets of smaller ordinals. A measurable cardinal's measure need not belong to that inner model, so preservation of the stronger property is a different issue. Large cardinal axioms are thus structured additional hypotheses, with carefully distinguishable consequences and relative-consistency claims, rather than a single claim that sufficiently big cardinals exist.

All independence assertions here are relative consistency results. Begin with a first-order model of ZF; for the choice-preserving side use ZFC. The original first-order model already gives the side where foundation holds. We construct the opposite side while checking the other axioms, then add a symmetry restriction to make choice fail.

Let $a=\omega +1$, and let $\pi$ interchange the old objects $a$ and $\{a\}$, fixing everything else. They are distinct. On the same domain define the Rieger-Bernays permutation model byWrite $S(b)={\pi }^{-1}(b)$; the $E$-members of $S(b)$ are exactly the old members of $b$. In particular $aEa$, and $a$ has no other $E$-member. Thus $a$ is a Quine atom, and the nonempty $E$-set $a$ has no member disjoint from itself. Foundation fails.

Here are the other axioms explicitly. Equal $E$-extensions imply $\pi (y)=\pi (z)$ by old extensionality, hence $y=z$. An $E$-pair of $x,z$ is $S(\{x,z\})$. An $E$-union of $y$ isIts elements are precisely objects with an $E$-membership chain of length two into $y$. The $E$-power set of $y$ issince $x{\subseteq }_{E}y$ means $\pi (x)\subseteq \pi (y)$. These are old sets by power set and replacement.

Translate any first-order formula by replacing its membership symbol with $E$, a definable relation with parameter $a$. Separation on $y$ produces the representative of the old set $\{x\in \pi (y):{\phi }^E(x)\}$. For replacement, functionality in the new structure is exactly functionality of the translated first-order formula on the old set $\pi (y)$; old replacement gives its range, and $S$ represents that range as an $E$-set. Thus the full schemas, not merely their quantifier-free instances, survive. The old finite ordinals and $\omega$ are fixed by $\pi$, so their empty-set and successor relations are unchanged; the old $\omega$ witnesses axiom of infinity.

If the original first-order model satisfies AC, the new one does too. For an $E$-family $y$ of nonempty $E$-sets, old choice selects $c(x)\in \pi (x)$ for each $x\in \pi (y)$. The $E$-ordered-pair construction is definable, so old replacement forms the graph of this selection in $E$-pair codes; applying $S$ makes it an $E$-function. It chooses an $E$-member from each member of the family. Therefore a full membership permutation alone does not refute choice. We have provedwith choice preserved if it was initially present. Together with the unchanged well-founded first-order model, this proves foundation's independence from the remaining axioms.

For the choice-failing extension, work in an ambient first-order model of ZFC and build the extensional cumulative universe over Quine atoms. Let $A$ be a countably infinite collection of distinct tagged objects. Give each $q\in A$ the membership extension $\{q\}$. Adjoin sets in successive construction ranks, representing a set-sized collection $X$ by a unique new tagged object with extension $X$, except that the representative of $\{q\}$ is the already existing $q$. Denote this representative by $S(X)$ again. Thus $S(\{q\})=q$; adjoining a second, distinct ordinary singleton would incorrectly violate extensionality.

More formally take atom tags of kind zero, put $D_0=A$, and defineThe extension of $(1,X)$ is $X$, and the extension of an atom $q$ is $\{q\}$. Tags of the two kinds are disjoint. Any set-sized collection of objects has bounded construction ranks and hence a representative at a later stage. This proves pairing, union, power set, separation and replacement by representing their extensions, just as above. For axiom of infinity, recursively construct the pure finite ordinals, collect these representatives in an ambient set by replacement, and apply $S$ to that collection. The resulting inductive set is fixed by every atom permutation. Every object has a unique extension, so full extensionality holds, although foundation fails at the atoms.

Let $G$ be the full symmetric group of $A$. Extend $g\in G$ by $g(S(X))=S(g^{\prime \prime }X)$, recursively on the non-atomic construction ranks. This preserves membership, including the atomic self-loops. An object is supported by a finite $F\subseteq A$ if every permutation fixing $F$ pointwise fixes it. Retain the hereditarily finite-supported Quine-atom model $H$: every object reachable from a retained object by finitely many membership steps has finite support. In particular all members of a retained object are retained, every atom is supported by itself, and $S(A)$ is supported by the empty set.

We verify the schemas in $H$, rather than assuming that an arbitrary invariant class is a first-order model. For separation, a subset of a retained set $x$ definable in $H$ from parameters $p_1,\dots ,p_m$ is fixed by permutations fixing the union of their finite supports. Its members are already in $H$, so its representative belongs to $H$. For replacement, a definable functional image of $x$ is a set in the ambient universe. Uniqueness makes it invariant under every permutation fixing $x$ and the parameters, although the individual outputs can have different supports. Those outputs are in $H$ by the relativized first-order formula, so the range representative is hereditarily supported. This proves replacement without falsely requiring one finite support for every individual value.

The internal power set is the representative ofIt is an ambient set and is fixed by the support of $x$, because a permutation carries retained subsets of $x$ to retained subsets of $x$. Every member is retained by its definition. This proves the internal power-set axiom. Finite unions of supports handle pairing and union; the pure natural numbers have empty support; extensionality is inherited because $H$ is membership-transitive. Hence $H$ satisfies all ZF axioms except foundation, which still fails.

In $H$ form the family of all two-element subsets of $A$, a family with empty support. Suppose it had a choice function $f\in H$, with finite support $F$. Choose distinct $q,r\in A\setminus F$. Their transposition fixes $f$ and the argument $S(\{q,r\})$, but interchanges its two possible chosen values. Equivariance gives a contradiction. ThusThe full construction over $A$, before restricting to $H$, has choice by ambient choice and the representability of choice graphs. Alternatively an ordinary ZFC first-order model gives the positive choice side. This proves the independence of AC from ZF minus foundation. The required metatheoretic consistency can be expressed using Con(ZF), since the constructible universe of a ZF first-order model supplies ZFC, as explained in the next solution. No assumption of a transitive model follows from mere consistency or is needed for these interpreted first-order model constructions.

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.