Symmetric Extensions and Basic Choice-Failure Models

Simultaneously induct on the ranks of $\sigma ,\tau$. In the atomic membership and equality clauses, $q\le p$ iff $\pi q\le \pi p$, compatible extensions correspond under $\pi$, and subnames correspond rank-preservingly. Therefore $p⊩\sigma \in \tau$ iff $\pi p⊩\pi \sigma \in \pi \tau$, and likewise for equality.

Induct on formula complexity. Boolean clauses commute with the bijection of conditions. For an existential, F1 maps the class of all $P$-names bijectively to itself, so witnesses correspond; applying the inverse automorphism from F1 gives the reverse implication. This is a syntactic induction on the stated forcing clauses; no semantic-generic existence hypothesis is used.

Now assume $\pi \in G$ and $\vec{\tau }\in \mathrm{H}\mathrm{S}$. F4 makes $\pi \vec{\tau }$ an HS tuple. Apply the already-proved ordinary forcing equivalence of step 2.1 to these parameter tuples; its existential name quantifier still ranges over all $P$-names, exactly as F3 specifies. This proves the asserted parameter-preserving specialization and makes no claim about an unintroduced HS-restricted forcing relation.

Induct on rank of $x$. Every subname $\check{y}$ for $y\in x$ is HS by induction. F1 gives $\pi \check{x}=\check{x}$ for every automorphism, so its stabilizer is the whole group and belongs to the normal filter. Thus $\check{x}$ is HS.

F3 gives ${\check{x}}_{G_0}=x$. Hence every ground set occurs as the value of an HS name, including $x=\mathrm{\varnothing }$, and the ground model is contained in the symmetric interpretation.

Values of HS names lie in $M[G_0]$, while hereditary closure says that every member of such a value has an HS subname. Hence $M\subseteq N\subseteq M[G_0]$ and $N$ is transitive.

The class is almost universal relative to the ambient transitive ZF extension $M[G_0]$, without choosing simultaneous HS representatives. Let $\dot{x}\in M$ name an ambient set $x\subseteq N$. For each $(\tau ,p)\in \mathrm{dom}(\dot{x})\times P$, define $r(\tau ,p)$ to be the least ordinal rank of an HS name $\sigma$ for which $p⊩\tau =\sigma$, if there is one, and $0$ otherwise. This is a definable ground-model function: the forcing relation and the HS predicate are definable, and any nonempty definable class of ordinal ranks has a least member. ZF Replacement in $M$ strictly bounds its values on the displayed set by an ordinal $\alpha$. If $u\in x$, some $(\tau ,p)\in \dot{x}$ has $p\in G_0$ and ${\tau }_{G_0}=u$; since $u\in N$, some HS $\sigma$ also evaluates to $u$. The truth lemma gives a common strengthening $q\in G_0$ of $p$ forcing $\tau =\sigma$, so $r(\tau ,q)<\alpha$. Thus every $u\in x$ is the value of an HS name of rank below $\alpha$.

For $a,\vec{w}\in N$ and a bounded formula $\phi (u,\vec{w})$ with any finite tuple of parameters, choose HS names $\dot{a},\dot{\vec{w}}$ and form the ground set-name $\{(\tau ,p)\in \mathrm{dom}(\dot{a})\times P:p⊩\tau \in \dot{a}\wedge \phi (\tau ,\dot{\vec{w}})\}$. Every immediate subname $\tau$ of $\dot{a}$ is HS. Bounded truth is absolute between the transitive classes $N$ and $M[G_0]$, so the truth lemma evaluates this name to $\{u\in a:N\models \phi (u,\vec{w})\}$. F2 shows that the finite intersection of the parameter stabilizers fixes this name, whose subnames are HS; filter closure puts that intersection in the filter. Thus $N$ has every instance of ${\mathrm{\Delta }}_0$-Separation.

Apply Jech's transitive-class criterion inside $M[G_0]$, rather than cutting an arbitrary ambient subset by bounded Separation. Transitivity supplies Extensionality and Foundation; check names supply $\mathrm{\varnothing }$ and $\omega$. For $N$-parameters, each of Jech's eight Gödel-operation outputs—unordered pair, difference, product, domain, membership relation restricted to a square, and three coordinate permutations—is an ambient set of elements already in $N$: first use unordered pairs and Kuratowski pairs, then the remaining operations in that finite order. By step 1.2 each such output lies inside an $N$-set, and its defining bounded formula with those parameters lets step 1.3 cut out exactly the output. Hence $N$ is closed under the eight operations. Jech's formula-complexity induction from that closure and almost universality gives full Comprehension, including the unbounded-quantifier cases; it also derives Pairing, Union, internal Power Set, Infinity and Replacement (the last by bounding the outer set of functional values via almost universality, then applying Comprehension). This proves every ZF schema instance. No AC enters this argument, and only the ZF branch of F3 is used.

F1 shows that $\{n\}$ supports ${\dot{a}}_n$ and $\mathrm{\varnothing }$ supports $\dot{A}$; their subnames are checks, so both are HS. For $n\mathrm{\ne }m$, below any condition choose a fresh bit coordinate $k$ and set opposite bits at $(n,k),(m,k)$. Hence the set forcing ${\dot{a}}_n\mathrm{\ne }{\dot{a}}_m$ is dense. Every finite collection is therefore forced to have its displayed size, so $A$ is infinite.

Let $\dot{e}$ be the canonical graph $n\mapsto {\dot{a}}_n$. Given finite $E$, choose $n\mathrm{\notin }E$ and $m\mathrm{\notin }E\cup \{n\}$. Their transposition fixes $E$ but sends the graph value at $n$ from ${\dot{a}}_n$ to ${\dot{a}}_m$, so it does not fix $\dot{e}$. Thus no finite $E$ supports that name.

Now let $p⊩\dot{f}:\check{\omega }\to \dot{A}$ be onto and let the finite set $E$ support $\dot{f}$ and contain the first-coordinate support of $p$. Choose $n\mathrm{\notin }E$. Since $p$ forces surjectivity, some $q\le p$ and $k\in \omega$ satisfy $q⊩\dot{f}(\check{k})={\dot{a}}_n$. Choose $m$ outside $E\cup \{n\}$ and outside the first-coordinate support of $q$, and let $\pi$ swap $n,m$. Then $\pi p=p$, $\pi \dot{f}=\dot{f}$, and F2 gives

Because the $m$-coordinate is absent from $q$, $q$ and $\pi q$ agree on their common domain and have a common extension. That extension forces ${\dot{a}}_n={\dot{a}}_m$, contrary to step 1.1. Therefore no HS name can enumerate $A$.

Let $p⊩\dot{f}:\check{\omega }\to \dot{A}$, and enlarge a finite support $E$ of $\dot{f}$ to support $p$. If some $q\le p$ forces $\dot{f}(i)={\dot{a}}_n$ with $n\mathrm{\notin }E$, choose $m$ outside $E\cup \{n\}$ and outside the first-coordinate support of $q$. Let $\pi$ swap $n,m$. Then $\pi \dot{f}=\dot{f}$, $\pi p=p$, and F2 gives $\pi q⊩\dot{f}(i)={\dot{a}}_m$.

The conditions $q$ and $\pi q$ agree wherever both are defined: the $m$ coordinate was fresh and all other moved coordinates are fixed. Their union is a common extension forcing ${\dot{a}}_n={\dot{a}}_m$, contradicting F1. Hence no extension of $p$ can put a value outside $\{a_n:n\in E\}$, and density of decisions yields $p⊩\mathrm{ran}\dot{f}\subseteq \{{\dot{a}}_n:n\in E\}$.

Thus every such map has finite range, so none is injective or enumerates the infinite set $A$. A countably infinite subset would, by its meaning in ZF, carry a bijection from $\omega$ and hence an injection into $A$, also impossible. Fresh indices were chosen only from explicit complements of finite sets; no AC is used.

For every $k$, the finite set $\{a_0,\dots ,a_{k-1}\}$ belongs to the model and has $k$ distinct members, so $A$ is not finite. This uses each finite initial collection, not the absent full enumeration.

F2 says there is no injection from $\omega$ and no countably infinite subset. F4 identifies either positive condition with Dedekind infinitude as defined by F3. Negating the equivalent clauses shows that there is no bijection from $A$ to a proper subset and that $A$ is Dedekind-finite. No Choice is used.

If $A$ had a well-order, recursion selecting the least unused member would either terminate after finitely many steps—making $A$ finite—or define an injection $\omega \to A$. Both contradict F1. Thus $A$ is not well-orderable.

By F4 the basic Cohen HS interpretation is a ZF model containing $A$. If it satisfied F3, F2 inside that model would well-order $A$, contradicting step 1.1. Hence AC fails. This reductio is the exact use of the choice dependency; the symmetric-model construction itself remains choice-free.

Fix the actual formulas of $\mathrm{\Delta }$ and their subformulas. Use $P=\mathrm{Add}(\omega ,\omega )$, the finite permutations of the first coordinate, and the finite-support normal filter of F2. For each of these fixed formulas the recursions in F1 give ordinary set-theoretic proofs of definability, strengthening, truth and equivariance. Name-rank induction is an object-level transfinite induction in those proofs, not a numerical search over names.

Here is the almost-universality argument used by the HS-model construction. In an ambient generic extension let $x={\dot{x}}_{G_0}\subseteq N={\mathrm{H}\mathrm{S}}^{G_0}$. In the ground model assign to each $(\tau ,p)\in \mathrm{dom}(\dot{x})\times P$ the least rank of an HS name $\sigma$ such that $p⊩\tau =\sigma$, or zero if none exists. Ground Replacement bounds these ranks strictly by an ordinal $\gamma$. For every $u\in x$, a subname $\tau$ evaluating to $u$ and the truth lemma give such an equality at some condition in $G_0$. Thus $u$ has an HS name of rank below $\gamma$. The ground set of all HS names below that rank is invariant under every automorphism; placing all these names at the top condition gives an HS name for an $N$-set containing $x$. This proves relative almost universality. For a bounded matrix, rank-bounded HS subnames satisfying its ordinary forcing clause form the exact cut of an $N$-set. Bounded absoluteness identifies that clause with truth in $N$; the parameter stabilizers and equivariance make the cut HS.

For completeness, the failure-of-Choice argument in F3 has two supported-map branches. Distinct coordinate names ${\dot{a}}_n$ are forced unequal by assigning opposite values at a fresh bit. If an HS name $\dot{f}$ were an injection from $\omega$ to $A$, take a finite support $E$ for it and a condition $p$ forcing this, enlarging $E$ to include the finite first-coordinate support of $p$. If no strengthening decides any value outside $\{a_n:n\in E\}$, density of value decisions confines its range to that finite set, contradicting injectivity. Otherwise choose a strengthening $q$ deciding $f(i)=a_n$ with $n\mathrm{\notin }E$, and $m$ outside $E\cup \mathrm{supp}(q)\cup \{n\}$. The transposition of $n,m$ fixes $p,\dot{f}$; $q$ and its image agree off the swapped coordinates and have disjoint domains on them, so their union forces two distinct values for $f(i)$. Thus $A$ is infinite and has no injection from $\omega$; a well-order of $A$ would give one by successively choosing its least remaining element. Hence $N\models \mathrm{\neg }\mathrm{A}\mathrm{C}$. These are set-theoretic arguments within the chosen proof, not operations performed by a numerical proof constructor.

Pairing HS names directly gives unordered and Kuratowski pairs in $N$. Each of Jech's eight operations (pair, difference, product, domain, restricted membership and three triple-coordinate permutations) produces an ambient set of $N$-elements. Step 2.1 puts it inside an $N$-set; its bounded defining formula cuts out the operation's exact value. To obtain general Separation, induct externally on the fixed formula's complexity. Atomic relations follow from these operations, negation from relative difference, and conjunction from intersection. For an existential subformula $\mathrm{\exists }v\psi (v,\bar{u})$, ambient Separation and Replacement collect, for every parameter tuple, the set of all $N$-witnesses of least rank, or the empty set. Starting from the argument set and the parameters, close under these witness sets for $\omega$ stages. This yields an ambient set containing witnesses for every relevant tuple. Almost universality puts it inside a set $Y\in N$; the induction hypothesis constructs the relation for $\psi$ on $Y$, and projection followed by restriction gives the existential relation on the original argument set. This is the cited Jech all-witness and transitive-class argument, with no choice of a distinguished witness. For a fixed functional Replacement matrix, ambient Replacement bounds its unique $N$-values on the domain, almost universality supplies an internal container, and the just-proved internal Separation cuts out the image. Only bounded matrices used the direct subname cut of step 2.1.

For the externally fixed $\mathrm{\Delta }$, the finitely many formula inductions just described yield finite ZFC derivations of its HS-model axioms and step 2.2. Collect their actual Separation, Replacement, recursion and forcing instances into a finite ground support $\mathrm{\Gamma }$, enlarging it for the names, valuations and generic construction. The preceding argument applied to a countable transitive $\mathrm{\Gamma }$-model proves that its symmetric extension satisfies each member of $\mathrm{\Delta }$; full ZFC in that ground model is not used. F4 proves in ambient ZFC that such a countable transitive source model exists. Enumerate its dense subsets, construct a generic filter, and take the set of valuations of its HS names. This gives a set model of the particular $\mathrm{\Delta }$. Ambient AC has precisely the source-model and generic-construction role of F5.

The ambient ZFC derivation in step 4.1 is finite, so it too uses only finitely many axioms and schema instances. The choice of this proof is made separately for the given external $\mathrm{\Delta }$. Neither a single internally quantified model-existence assertion nor a PA-total selector of these proofs follows from this argument. This proves exactly the fixed-fragment assertion.

The hypothetical contradiction proof uses a finite list $\mathrm{\Delta }$ of axioms of ZF and the negation of F3. Fix this list externally. F2 provides a ZFC proof that a set model of $\mathrm{\Delta }$ exists. Soundness for the particular finite contradiction proof gives a ZFC proof that no such model exists. Thus target inconsistency implies inconsistency of ZFC.

F1 makes ZFC consistent whenever ZF is consistent. Contraposition in step 1.1 therefore proves the stated external relative-consistency implication. Source Choice is available in the ambient ZFC construction; the symmetric target refutes it. Each target proof is handled separately, without a claim that PA verifies a uniform map on proof codes.

F1 makes every $P_n$ and the indexed sequence HS, so the symmetric ZF model regards its range as countable pairs. Distinct-coordinate dense sets ensure $R_{n,0}\mathrm{\ne }{R}_{n,1}$.

Suppose $p⊩\dot{c}(n)\in {\dot{P}}_n$ for a supported choice name $\dot{c}$. Choose $n$ outside the finitely many supported pair indices and strengthen to $q\le p$ deciding, say, $\dot{c}(n)={\dot{R}}_{n,0}$. Choose a block swap at $n$ that fixes the support. By additionally permuting unused $j$-coordinates in that block, arrange that $q$ and its image have disjoint moved domains and hence are compatible.

F2 says the image condition forces the same $\dot{c}(n)$ to equal ${\dot{R}}_{n,1}$. A common extension then forces the two distinct mates equal, contradiction. Therefore no choice function exists and F3 fails. The construction is in pure ZF and uses neither the Recorded transfer result nor AC.