Permutation Models and Transfer to ZF

Every atom is symmetric because ${\mathrm{fix}}_G(\{a\})$ fixes $a$, and every pure set is fixed by every permutation; both are hereditarily symmetric, so $A\cup K\subseteq \mathrm{H}\mathrm{S}$, while conversely the pure kernel is unchanged because no atom lies in a pure set. Transitivity is F1. Empty Set, Infinity, Extensionality and Foundation restrict from $M$. If $x,y\in \mathrm{H}\mathrm{S}$, the stabilizer intersection fixes $\{x,y\}$, $x\cup y$, and the usual finite set operations; their members are hereditary, giving Pairing and Union.

Because $G,\mathcal{F}$ and their action are internal to $M$, the predicate “$u\in {\mathrm{H}\mathrm{S}}_{\mathcal{F}}^M$” is definable over $M$ from those parameters by rank recursion. Hence $M$-Separation forms

For Replacement, suppose the internal formula assigns a unique $y$ to every $x\in a$. Ambient Replacement forms the image $b$. Any permutation fixing $a$ and all parameters maps a witnessed pair $(x,y)$ to $(gx,gy)$; uniqueness therefore maps $b$ to itself. Each value $y$ is in HS by the internal quantifier domain, so $b$ is hereditarily symmetric. This proves every ZFA axiom without Choice.

Noninheritance is witnessed by the finite-support full-permutation system on a countably infinite atom set: its atom set is HS, but a supported well-order would be moved by a transposition outside its finite support. Thus the ambient $M$ may satisfy F2 while its HS submodel does not.

Let $B\subseteq A$ in the model and let finite $E$ support it. If two atoms $a,b\mathrm{\notin }E$ had different membership in $B$, their transposition would fix $E$ but move $B$. Thus either no atom outside $E$ lies in $B$, making $B$ finite, or every atom outside $E$ lies in $B$, making it cofinite.

The set $A$ is infinite because every ground finite subset omits an atom. If $f:\omega \to A$ were injective in the model, the even-indexed range would be infinite and its complement would contain the infinite odd-indexed range, contradicting step 1.1. Hence there is no such injection, in agreement with F2.

If a well-order $<$ of $A$ had finite support $E$, the nonempty invariant set $A\setminus E$ would have a least member $a$. Choose $b\mathrm{\notin }E\cup \{a\}$ and transpose $a,b$. The transposition fixes $<$ and $E$, so must send its uniquely least outside-$E$ member to itself, but sends $a$ to $b$, contradiction. Thus $A$ is not well-orderable. F3 now shows by contraposition that AC fails in the permutation model. This reductive use of AC is the only choice dependence of the conclusion.

Every permitted permutation maps each $P_n$ to itself, so each pair and the graph $\{(n,P_n):n\in \omega \}$ have empty support and belong to the model. The pairs remain two-element and their range is countable there.

Suppose $c(n)\in P_n$ were a choice function with finite atom support $E$. Choose $n$ with $P_n\cap E=\mathrm{\varnothing }$. The permutation swapping the two atoms of $P_n$ and fixing all other atoms belongs to $G$, fixes $E$, every $P_k$, and $n$, but moves $c(n)$. It must both fix $c$ by support and move its value at $n$, contradiction. Thus the displayed family witnesses failure of F2. No AC is used.

The order relation is fixed by every order automorphism, so it has empty support. We first verify the finite-support intersection fact used below. If $E_1,E_2\subseteq A$ are finite and $E=E_1\cap E_2$, then \operatorname{fix}(E)=\langle\operatorname{fix}(E_1)\cup\operatorname{fix}(E_2)\rangle. \tag{*} Indeed, cut $A$ at the points of $E$. In each resulting open interval the two finite sets $E_1\setminus E$ and $E_2\setminus E$ are disjoint. List their points and the images of those points under a given $\pi \in \mathrm{fix}(E)$. Move the image points into their required successive cuts, one at a time. To cross a point of $E_1\setminus E$, use an increasing finite partial bijection which fixes $E_2$; to cross a point of $E_2\setminus E$, use one which fixes $E_1$. The point being crossed is not in the fixed set, and density and the absence of endpoints provide a fresh point on the required side. Each such finite increasing partial bijection extends, by the usual interval-by-interval back-and-forth for a countable dense order without endpoints, to an automorphism in the indicated pointwise stabilizer. There are only finitely many marked and image points, so after finitely many moves the residual automorphism fixes $E_1$ (and the last correction may be taken to fix $E_2$). This proves $(\ast )$ on each component; joining the component automorphisms proves it on $A$. If $E_1,E_2$ support $x$, every factor on the right of $(\ast )$ fixes $x$. Thus every element of $\mathrm{fix}(E)$ fixes $x$, and $E_1\cap E_2$ supports $x$.

All supports contained in one fixed finite support form a finite family. Repeated intersection therefore gives a support $E_x$ contained in every support; it is the unique least support. Conjugating shows $g{E}_x$ is the least support of $gx$, so the least-support assignment is itself symmetric.

Suppose a well-order $◃$ of $A$ belonged to the model, and let $E$ be a finite support for it. The nonempty set $A\setminus E$ has a $◃$-least element $a$. It lies in one of the open intervals cut out by $E$; choose $b\mathrm{\ne }a$ in that interval. The finite increasing partial map fixing $E$ and sending $a$ to $b$ extends by back-and-forth to an order automorphism $\pi \in \mathrm{fix}(E)$. Because $E$ supports $◃$, $\pi$ preserves $◃$ and maps $A\setminus E$ to itself. It must therefore fix that subset's unique $◃$-least element, contradicting $\pi (a)=b$. Hence $A$ is linearly ordered by the empty-supported dense order but is not well-orderable. Since F2 implies well-orderability of every set, AC fails.

Work first in $M$. By [F5], the choices stated above can be made with $A^{\mathrm{\prime }}$ a pure ordinal and a bijection $j:A\to A^{\mathrm{\prime }}$. The ordinal $\kappa$ and the set $A^{\mathrm{\prime }}$ belong to $K$; regularity of $\kappa$ in $M$ implies regularity in $K$, since any shorter cofinal sequence in $K$ would also belong to $M$. By [F4], $K$ satisfies ZFC. Work in the specified $K$-generic outer universe for the poset $P\in K$ of partial binary functions of size $<\kappa$ on $(A^{\mathrm{\prime }}\times \kappa )\times \kappa$. The pure coordinate set ensures that $P$, unlike a poset indexed directly by atoms, belongs to $K$; regularity makes it $<\kappa$-closed. Moreover, every $M$-set sequence of pure conditions and every $M$-set of pure conditions is itself pure and therefore belongs to $K$; closure and genericity apply to the ambient enumerations used below. For each $(a,\xi )$, use the coordinate $(j(a),\xi )$ to name a generic subset $x_{a\xi }$ of $\kappa$, put $a^{\ast }=\{x_{a\xi }:\xi <\kappa \}$, and $A^{\ast }=\{a^{\ast }:a\in A\}$. Recursively translate atoms to $a^{\ast }$ and sets to the set of translations of their members.

Transport each original atom permutation through $j$ to the blocks $\{j(a)\}\times \kappa$ of the pure coordinate set, allowing arbitrary within-block permutations. Generate a normal filter from the transported original filter and finite pointwise stabilizers. The coordinate names, each $a^{\ast }$, and $A^{\ast }$ are hereditarily symmetric. For the transported automorphism $\pi$, the atomic forcing clauses commute with $p\mapsto \pi p$ and $\dot{x}\mapsto \pi \dot{x}$: a common strengthening or subname witness is carried bijectively to one on the other side. Simultaneous induction on name ranks and then on formula complexity (including the existential name witness) gives $p⊩\phi (\vec{\tau })$ iff $\pi p⊩\phi (\pi \vec{\tau })$. This derives the equivariance used below from F2's definable forcing clauses, without assuming it as an extra theorem. A further simultaneous induction on rank proves $x\in y$ iff $x^{\ast }\in y^{\ast }$ and $x=y$ iff $x^{\ast }=y^{\ast }$; distinct coordinate generics make the atom case injective.

The translation of $x$ is hereditarily symmetric exactly when $x\in V$. For the reverse implication, take a least-rank counterexample and a symmetric name forced equal to its translation. A permutation from the original support filter moving $x$ can be lifted so that it fixes the finite coordinate support and moves the forcing condition to a compatible one, producing contradictory forced equalities.

Let $W$ be the interpretations of the hereditarily symmetric (HS) names for the lifted group and filter. These values are transitive and contain every pure check name. We establish almost universality relative to $K[G]$ without choosing simultaneous HS representatives. If an ambient set $x\in K[G]$ has $x\subseteq W$, take a $K$-name $\dot{x}$ for it. For each $(\tau ,p)\in \mathrm{dom}(\dot{x})\times P$, let $r(\tau ,p)$ be the least rank of an HS name $\sigma$ such that $p⊩\tau =\sigma$, or $0$ if none exists. The forcing relation and HS predicate are definable in $K$; Replacement there bounds these ranks by one ordinal $\gamma$. For $u\in x$, choose one pair $(\tau ,p)\in \dot{x}$ with $p\in G$ and ${\tau }_G=u$, and one HS name $\sigma$ evaluating to $u$. The truth lemma yields a common $q\in G$ below $p$ forcing $\tau =\sigma$; hence $r(\tau ,q)<\gamma$ and $u$ has an HS name below $\gamma$.

For $a,\vec{w}\in W$ and any bounded formula $\phi (u,\vec{w})$, use HS names $\dot{a},\dot{\vec{w}}$ and the subname $\{(\tau ,p)\in \mathrm{dom}(\dot{a})\times P:p⊩\tau \in \dot{a}\wedge \phi (\tau ,\dot{\vec{w}})\}$. Its immediate subnames are HS; forcing equivariance makes the finite intersection of the parameter stabilizers fix it. Bounded absoluteness between the transitive $W$ and $K[G]$, followed by the truth lemma, identifies its value with the desired cut of $a$. Thus $W$ has ${\mathrm{\Delta }}_0$-Separation.

Let $S$ be the ground set of all HS names of rank below $\gamma$ and form the value-collecting name $\dot{y}=\{⟨\sigma ,p⟩:\sigma \in S\text{ and }p\in P\}$.

Its value is $\{{\sigma }_G:\sigma \in S\}$ because $G$ is nonempty. Automorphisms preserve $S$ and all of $P$, so $\dot{y}$ is fixed; its immediate subnames are HS. Thus $\dot{y}$ is itself HS and its value is a $W$-set containing $x$.

Now apply Jech's transitive-class criterion inside the ambient transitive ZF model $K[G]$. For $W$-parameters, each of its eight Gödel-operation outputs—unordered pair, difference, product, domain, the membership relation restricted to a square, and the three permutations of triple coordinates—is an ambient set whose members already lie in $W$: construct unordered and Kuratowski pairs first, then the remaining outputs in that order. Almost universality puts each output inside a $W$-set, and its bounded defining formula cuts it out by step 3.3. Hence $W$ is closed under all eight operations. Jech's formula-complexity induction from transitivity, almost universality, and this closure supplies full Comprehension, including unbounded quantifiers; the criterion also yields Pairing, Union, internal Power Set, Infinity, and Replacement. Thus $W$ is a symmetric ZF model between the kernel and the full generic extension. This argument uses no AC in $W$.

Induct through $\beta \le \alpha$ to prove surjectivity onto ${\mathcal{P}}^{\beta }(A^{\ast }{)}^W$. At $\beta =0$ this is the explicit bijection $a\mapsto a^{\ast }$ from step 2.1. At a limit $\beta$, both power-set hierarchies are the unions of their lower stages, so the compatible earlier identifications give the result. At a successor stage, the earlier members retain their translations. Put $x={\mathcal{P}}^{\beta -1}(A{)}^V$, and let $y={\dot{y}}_G\in W$ be a subset of the translated image $x^{\ast }$. By the truth lemma choose $p_0\in G$ forcing $\dot{y}\subseteq {\dot{x}}^{\ast }$. The ambient $M$-cardinality bound $\mathrm{\mid }x\mathrm{\mid }<\kappa$ from step 1.1 supplies an enumeration $⟨x_i:i<\lambda ⟩$ with $\lambda <\kappa$. Its translated pure-name sequence, together with $\dot{y}$, is a $K$-set by step 1.1. For each $i<\lambda$ the conditions deciding ${\dot{x}}_i^{\ast }\in \dot{y}$ are dense. Starting below any $p\le p_0$, recursively choose one stronger decider for each $i$ and take a lower bound at limit stages below $\lambda$, using $<\kappa$-closure. This pure recursion lies in $K$, so the set $D$ of conditions below $p_0$ deciding every listed membership is a $K$-dense set below $p_0$. Since $G$ is $K$-generic and contains $p_0$, choose $q\in G\cap D$. Define in $M$ the ground subset $z=\{x_i:i<\lambda ,q⊩{\dot{x}}_i^{\ast }\in \dot{y}\}$. The decisions and $q⊩\dot{y}\subseteq {\dot{x}}^{\ast }$ give $q⊩{\dot{z}}^{\ast }=\dot{y}$; in particular $z^{\ast }=y$ in the chosen generic extension. By the reverse HS criterion of step 3.1, the symmetric name $\dot{y}$ forced equal to the translation below $q$ implies $z\in V$. The dense-set/genericity step is essential: a lower bound deciding all memberships outside $G$ would not determine the actual $y$. Thus translation is a membership isomorphism at every lower iterate. If $A=\mathrm{\varnothing }$, the coordinate forcing is trivial and $W=K$, so the same identification includes the empty-atom endpoint. Ambient AC in $M$ supplies the well-order of ${\mathcal{P}}^{\alpha }(A)$, the regular cardinal $\kappa$, and the atom-to-pure-coordinate bijection; the pure kernel inherits AC for the closure recursion, while $W$ need not satisfy AC.

Apply F2 at height $\alpha$ to obtain the bijections on every sort named by $\theta$. Pure-kernel parameters are fixed by the recursive translation of pure sets, with their mixed atomic incidences checked as part of the certificate. The carried bijections preserve equality and membership between the named objects. They assert nothing about members of an image $a^{\ast }$ lying outside those sorts. General boundability in F1 supplies no missing preservation claim; the certificate explicitly limits the formula to this carried incidence structure.

Induct on the finite typed formula $\theta$. Atomic equality and membership are preserved by step 1.1, and Boolean connectives follow immediately. For a quantifier over a named sort, F2 is onto that sort, so every possible target witness has exactly one source preimage and the induction hypothesis applies in both directions. Thus $\theta$ has the same truth value in the source and target incidence structures. No quantifier ranges over the uncarried members of a base-sort image.

Step 2.1 already gives the parameterized typed-formula assertion. When the two extra equivalences to a global $T$ are supplied, compose them with step 2.1 to get $V\models T$ if and only if $W\models T$. A one-way target consequence of a transported typed assertion may also be inferred without a global source equivalence. The atom-sensitive two-empty-objects formula fails the certificate: two atoms can be memberless in ZFA, while distinct memberless sets violate Extensionality in ZF, so no target equivalence to the same typed incidence formula can be proved. The only Choice hypothesis is the ambient ZFA+AC premise of F2; $W$ need not satisfy AC.

Write the atoms as $a_{n,i}$ for $n\in \omega$ and $i<2$. The group swaps members within each pair $P_n=\{a_{n,0},a_{n,1}\}$; its normal filter is generated by finite pointwise supports. F1 makes $(P_n{)}_{n\in \omega }$ symmetric. If a choice graph had finite support, swapping a pair disjoint from that support would fix the graph and its input while moving its selected value, a contradiction.

Fix an ordinal power-iterate height $\alpha$ large enough to contain $\omega$, the pair sequence and its graph, every possible choice graph from $\omega$ to ${\bigcup }_n{P}_n$, and every intermediate singleton, unordered pair and Kuratowski ordered-pair code used to express $T$; $\alpha =\omega +\omega$ is more than enough for these fixed finite-rank coding operations. No finite iterate suffices, because the von Neumann naturals have unbounded finite rank. A graph is a subset of $\omega \times {\bigcup }_n{P}_n$, so this one ordinal height bounds every hypothetical witness. The pure parameter $\omega$ is fixed by the embedding. Encode the ZFA ambient source with distinct atom tags and set tags; F5's atom/set distinction prevents an atom from being identified with the empty set. The tagged interpretation uses ambient AC to well-order the atom set and make the pure coordinate copy required by F2.

Apply F2 at height $\alpha$ in a pure-forcing generic outer universe. Its set $A^{\ast }$ and symmetric ZF model $W$ carry the relevant power iterates, including the pair sequence and all possible choice graphs. For each fixed formula in $\mathrm{\Delta }$, the formal proof of the HS-model axioms uses finitely many ambient Separation and Replacement instances. In the unbounded Separation case, the proof first establishes almost universality, closes under the eight Gödel operations, and then proceeds by formula complexity; an existential step collects all least-rank witnesses before projecting. Replacement bounds the ambient functional image and cuts it by the resulting internal Separation certificate. Direct subname cuts are used only for bounded formulas. Thus the instances actually needed for $\mathrm{\Delta }$ have a finite ambient axiom support.

Use the carried pair-sequence parameter and the pure parameter $\omega$ to express the typed assertion $\theta$ that this particular sequence has no choice graph. The recursive translation in F2 fixes pure sets, so it fixes each finite ordinal and $\omega$; the chosen ordinal height contains them. Every candidate graph for this sequence lies in a named carried sort by step 1.2. Singleton and unordered-pair codes, hence Kuratowski ordered-pair codes, are preserved because their intermediate sets lie in the carried hierarchy and their membership relations are preserved. Atomic equality and membership, including those involving the fixed parameters, are preserved, and the base atom sort is opaque. F3's typed-formula induction therefore transports $\theta$ from step 1.1 to $W$. This yields the existential ZF sentence $T$ because the copied sequence is a witness. It does not assert the false converse that any witness to $T$ in either universe must be this particular sequence.

For the fixed $\mathrm{\Delta }$, collect the finitely many ZFA source instances, pure-forcing and HS-model instances, and transfer formulas used in steps 1.1–2.1. F4 gives a countable transitive model of a sufficiently large fixed finite ZFC source fragment; its constructible interpretation supplies the particular GCH instances required by the construction. The tagged construction inside it supplies the finite ZFA+AC ambient source. The set forcing and symmetric submodel construction are formalizable from those selected instances, and yield in the ambient theory a set model of every member of $\mathrm{\Delta }$. Enlarging the source fragment finitely absorbs the proof's exact reflection, genericity, name-rank and soundness instances. This selection is external and may depend on $\mathrm{\Delta }$; it asserts neither a single PA-total selector nor a full-ZFC countable transitive model.

A contradiction proof from $\mathrm{Z}\mathrm{F}+T$ uses only a finite target fragment $\mathrm{\Delta }$. Fix $\mathrm{\Delta }$ externally. F2 supplies a proof in $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$ that a set model of $\mathrm{\Delta }$ exists. The alleged contradiction proof and finite-model soundness give a proof that no such model exists. Hence target inconsistency implies inconsistency of $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$.

By F1, consistency of ZF implies consistency of $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H}$, so step 1.1 gives the external relative-consistency implication. F3 identifies $T$ as a countable family of pairs without a choice function. If ZF proved ${\mathrm{A}\mathrm{C}}_{\omega ,2}$, then $\mathrm{Z}\mathrm{F}+T$ would be inconsistent; therefore consistency of ZF prevents such a proof.