Symmetric Collapse and Ultrafilter-Free Models

Let $\dot{x}$ be hereditarily symmetric. Its stabilizer belongs to $\mathcal{F}$. By the definition of the upward closure in F1, some $H_m$ is contained in $\mathrm{sym}(\dot{x})$. Thus every $\pi \in H_m$ fixes $\dot{x}$. Notice that this selects one natural number for one given name; it does not choose supports simultaneously for a family.

Now let $x\subseteq \omega$ belong to $N$, and choose one hereditarily symmetric name $\dot{x}$ with value $x$ in the supplied generic. By step 1.1 fix $m$ such that $H_m$ fixes $\dot{x}$. In the complete Boolean algebra $B$ from F2 put $b_k=\parallel \check{k}\in \dot{x}{\parallel }_B$ for $k<\omega$ and form the Boolean name $\dot{y}=\{⟨\check{k},b_k⟩:k<\omega \}$. By F4, the supplied Boolean generic contains $b_k$ exactly when $k\in {\dot{x}}_G=x$. Hence ${\dot{y}}_G=\{k:b_k\in G\}=x$. This proves equality of the two values in the fixed generic; it does not assert that an arbitrary name which happens to evaluate to a real is forced to be a real in every generic.

Make the Boolean action explicit. In the regular-open presentation from F2, $\widehat{\pi }(U)=\pi \mathrm{‘}\mathrm{‘}U$ preserves arbitrary unions followed by regularization, intersections, and complements, and so is a complete Boolean automorphism extending $p\mapsto \pi p$. The truth value $b_k$ is the regular open generated by conditions forcing $\check{k}\in \dot{x}$. If $\pi \in H_m$, then $\pi \check{k}=\check{k}$ and $\pi \dot{x}=\dot{x}$; F3 therefore maps that generating set to itself, whence $\widehat{\pi }(b_k)=b_k$. Hence $H_m$ fixes the displayed Boolean name $\dot{y}$ and fixes each of its Boolean coefficients. Its only subnames are the canonical natural-number names, so $\dot{y}$ is hereditarily symmetric. This is the asserted common bounded layer support.

Fix $p{\le }_{B}u$ and suppose $p\upharpoonright m\mathrm{̸}{\le }_{B}u$. Density of the embedding in F2 gives $q\in P$ with $q\le p\upharpoonright m$ and $q{\le }_B\mathrm{\neg }u$.

For every layer $n\ge m$ appearing in $q$, choose a finite permutation of its $i$-coordinates which moves all upper-layer coordinates of $q$ away from the finitely many upper-layer coordinates of $p$; extend it by the identity elsewhere. The resulting $\pi$ lies in $H_m$. Below layer $m$, $q$ extends $p\upharpoonright m$ and $\pi$ is the identity; above it, the moved domain of $\pi q$ is disjoint from the domain of $p$. Thus $p$ and $\pi q$ are compatible. This is a finite construction in finitely many represented layers.

Since $u$ is fixed by $H_m$, the regular-open automorphism described in F3 sends $q{\le }_B\mathrm{\neg }u$ to $\pi q{\le }_B\mathrm{\neg }u$. A common extension of $p$ and $\pi q$ would lie below both $u$ and $\mathrm{\neg }u$, contradicting Boolean incompatibility. Hence $p\upharpoonright m{\le }_{B}u$.

Let $v$ be the displayed join. Step 2.1 gives $v\le u$. Conversely every $p{\le }_{B}u$ satisfies $p\le p\upharpoonright m\le v$, and density below the regular open $u$ gives $u=\bigvee \{p\in P:p{\le }_{B}u\}\le v$. Therefore $u=v$.

Every initial-layer condition is fixed by $H_m$, so the complete subalgebra it generates is contained in $B_m$. The equality in step 3.1 writes every member of $B_m$ as a join of such conditions, yielding the reverse inclusion and the final assertion.

The set $P_{<m}=\{p\upharpoonright m:p\in P\}$ has ground cardinal at most ${\mathrm{\aleph }}_m^V$: its elements are finite functions using ordinals below the finitely many cardinals ${\mathrm{\aleph }}_n^V$ for $n<m$ (and for $m=0$ it is a singleton). Every regular open generated by $P_{<m}$ is a subset of $P_{<m}$, so F2 gives $\mathrm{\mid }{B}_m{\mathrm{\mid }}^V\le 2^{{\mathrm{\aleph }}_m^V}={\mathrm{\aleph }}_{m+1}^V$. This deliberately coarse estimate covers $m=0$ uniformly.

By F1, a member of $S_m$ is coded by a function $\omega \to B_m$. In ground ZFC and GCH, step 1.1 gives $\mathrm{\mid }{S}_m{\mathrm{\mid }}^V\le (2^{{\mathrm{\aleph }}_m^V}{)}^{{\mathrm{\aleph }}_0}=2^{{\mathrm{\aleph }}_m^V}={\mathrm{\aleph }}_{m+1}^V$. Since the constantly-zero name belongs to $S_m$, ground Choice supplies a fixed surjection $e_m:{\mathrm{\aleph }}_{m+1}^V\twoheadrightarrow S_m$.

Form the canonical name ${\dot{e}}_m^{\ast }=\{⟨⟨\check{\xi },\dot{x}{⟩}^{\bullet },1_B⟩:\xi <{\mathrm{\aleph }}_{m+1}^V\text{ and }\dot{x}=e_m(\xi )\}$. Every value name belongs to $S_m$ and is fixed by $H_m$, so $H_m$ fixes ${\dot{e}}_m^{\ast }$ and all its subnames. Thus it is hereditarily symmetric. Its interpretation is the function $\xi \mapsto e_m(\xi {)}_G$, whose range is exactly $R_m$ by F1. Hence $N$ contains the required surjection.

The ground use of Choice and GCH occurred only in steps 1.1–2.1 to obtain the single coded enumeration $e_m$. Step 3.1 puts its interpretation in $N$ without choosing enumerations for a family of arbitrary sets. This proves the asserted internal bound.

Define $f_n(i)=\alpha$ exactly when some $p\in G$ contains the triple $(n,i,\alpha )$. Functionality follows because two conditions in the filter are compatible and conditions are functional at $(n,i)$. For each $i<\omega$, conditions assigning a value at $(n,i)$ are dense; for each $\alpha <{\mathrm{\aleph }}_n^V$, conditions putting $\alpha$ at some fresh $(n,i)$ are dense. Therefore genericity, equivalently F2 and F3, makes $f_n:\omega \twoheadrightarrow {\mathrm{\aleph }}_n^V$.

The canonical name for $f_n$ uses only Boolean values from layer $n$. Every member of $H_{n+1}$ fixes all layers below $n+1$, hence fixes this name and its canonical ordinal subnames by F1. It is hereditarily symmetric, so $f_n\in N$.

The ordinal ${\mathrm{\aleph }}_n^V$ is nonempty. In ZF a surjection $f:\omega \twoheadrightarrow A$ onto a nonempty set gives an injection $A\to \omega$ by sending $a$ to the least $i$ with $f(i)=a$; hence $A$ is at most countable. Applying this inside $N$ to $f_n$ proves the claim. The construction is for one specified $n$ and does not assert that the sequence $⟨f_n:n<\omega ⟩$ belongs to $N$.

The ordinal ${\mathrm{\aleph }}_{m+1}^V$ is nonempty. By F2 and F3, fix in $N$ one surjection $f:\omega \twoheadrightarrow {\mathrm{\aleph }}_{m+1}^V$, and form $g_m=e_m\circ f$. Both factors are sets of $N$, and ordinary ordered-pair Separation produces their composition. For each $x\in R_m$, its $e_m$-preimage is nonempty, so take its least ordinal member $\xi$; then the $f$-preimage of $\xi$ is a nonempty set of naturals and has a least member $k$. Thus $g_m(k)=x$, so $g_m:\omega \twoheadrightarrow R_m$. This fixes one witness for one already fixed $m$; it does not choose a family indexed by $\omega$.

The layer is nonempty because it contains the interpretation of the constantly-zero Boolean name. Sending each $x\in R_m$ to its least $g_m$-preimage gives an injection into $\omega$, so $R_m$ is at most countable. The least-preimage clauses are definable and involve one fixed map; no choice function for the family $(R_m{)}_{m<\omega }$ is formed.

If $x\in {\mathbb{R}}^N$, F1 gives a Boolean real name for $x$ whose coefficients are fixed by some $H_m$; by F2 this says $x\in R_m$. Hence ${\mathbb{R}}^N\subseteq {\bigcup }_{m<\omega }{R}_m$. Conversely F2 defines each $R_m$ using names for subsets of $\omega$, so every member of every $R_m$ is a real of $N$. This proves the displayed equality.

F2 supplies the sequence $m\mapsto R_m$ itself as a set of $N$, not merely each layer separately. Its domain is ${\omega }^N=\omega$, so its range is a countable indexed family in the exact ZF sense, including possible repeated layers. By F4, Union applied in $N$ gives the set on the right of step 1.1.

F3 gives $N\models$ “$R_m$ is countable” for every $m<\omega$. Combining this pointwise statement with the sequence from step 2.1 proves that ${\mathbb{R}}^N$ is a countable union of countable sets. No function choosing an enumeration of every $R_m$ is asserted; forming such a simultaneous family would be the invalid Choice step that the theorem deliberately avoids.

By F3, apply F2 inside the ZF model $N$. Its canonical real line ${\mathbb{R}}^N$ is a complete ordered field there, and the theorem's nested-interval construction uses no Choice. Hence $N\models$ “$\mathbb{R}$ is uncountable.”

By F1 the same set ${\mathbb{R}}^N$ equals ${\bigcup }_{m<\omega }{R}_m$, where the sequence and every layer belong to $N$ and each layer is countable there. Combining that identity with step 1.1 gives the claimed contrast; it does not infer that the union is countable.

If $\alpha <\kappa$, then $\alpha <{\mathrm{\aleph }}_n^V$ for some $n<\omega$. For $\alpha =0$ it is finite. Otherwise restrict the surjection from F1 by replacing values outside $\alpha$ with $0$; this is a surjection $\omega \twoheadrightarrow \alpha$ in $N$. Thus every ordinal below $\kappa$ is countable in $N$, and consequently $\kappa \le {\omega }_1^N$.

Suppose for contradiction that some $f\in N$ is a surjection $\omega \twoheadrightarrow \kappa$. Choose an HS name $\dot{f}$ and use F2 to fix $m<\omega$ such that $H_m$ fixes it. For $k<\omega$ and $\alpha <\kappa$ let $u_{k,\alpha }=\parallel \dot{f}(\check{k})=\check{\alpha }\parallel$. These Boolean values are fixed by $H_m$, because $\dot{f}$ and the check names are fixed.

Let $P_{<m}=\{p\upharpoonright m:p\in P\}$. For each $k<\omega$ put $A_k=\{\alpha <\kappa :\mathrm{\exists }q\in P_{<m}(q{\le }_B{u}_{k,\alpha })\}$. Distinct $\alpha ,\beta \in A_k$ require incompatible witnesses, since a condition cannot force two different values of the function at $k$. Choosing the least witness in a fixed ground well-order injects $A_k$ into $P_{<m}$. Ground AC and the finite-function calculation give $\mathrm{\mid }{P}_{<m}{\mathrm{\mid }}^V\le {\mathrm{\aleph }}_m^V$, hence $\mathrm{\mid }{\bigcup }_{k<\omega }{A}_k{\mathrm{\mid }}^V\le {\mathrm{\aleph }}_m^V<\kappa$.

If $p⊩\dot{f}(\check{k})=\check{\alpha }$, then $p{\le }_B{u}_{k,\alpha }$, and F3 gives $p\upharpoonright m{\le }_B{u}_{k,\alpha }$; hence $\alpha \in A_k$. Because the alleged $f$ is surjective, F4 supplies such a $k$ and $p\in G$ for every $\alpha <\kappa$. Thus $\kappa ={\bigcup }_{k<\omega }{A}_k$, contradicting the strict bound in step 1.3. Therefore no such $f$ belongs to $N$, so $\kappa$ is uncountable in $N$.

Since ${\omega }_1^N$ is the least uncountable ordinal of $N$, step 2.1 gives ${\omega }_1^N\le \kappa$, while step 1.1 gives the reverse inequality. Hence ${\omega }_1^N=\kappa ={\mathrm{\aleph }}_{o}meg{a}^V$.

The ground sequence $c(n)={\mathrm{\aleph }}_n^V$ is a set of $V$ and hence, by F3, a set of $N$. Its range is cofinal in ${\mathrm{\aleph }}_{\omega }^V$ by the definition of the limit aleph. Using F1, $c:\omega \to {\omega }_1^N$ is therefore cofinal in $N$, so ${\mathrm{cf}}^N({\omega }_1^N)\le \omega$.

The ordinal ${\omega }_1^N$ is an infinite cardinal and therefore a limit ordinal. F2 makes its cofinality an infinite cardinal, hence at least $\omega$. Combined with step 1.1, this gives ${\mathrm{cf}}^N({\omega }_1^N)=\omega$. The witness is the one ground sequence $c$; no sequence of arbitrary choices is used.

F1 supplies a countable family of countable sets whose union is ${\mathbb{R}}^N$, while F2 says that union is uncountable. This single witness refutes the universal countable-union assertion in $N$.

By F3, ${\mathrm{cf}}^N({\omega }_1)=\omega <{\omega }_1^N$. Hence the internal cardinal ${\omega }_1$ is not regular and is therefore singular.

If $N$ satisfied ${\mathrm{A}\mathrm{C}}_{\omega }$ as defined in F5, F4 applied inside $N$ would give ${\mathrm{cf}}^N({\omega }_1)={\omega }_1^N$, contrary to step 1.2. Therefore $N\models \mathrm{\neg }{\mathrm{A}\mathrm{C}}_{\omega }$. These are deductions in ZF from explicit witnesses; no Choice principle is used in deriving its own failure.

Expand the proofs of the finitely many formulas in $\mathrm{\Delta }$. For the three extra sentences, expand F1 and every dependency used in its collapse, Boolean-value, cardinal, cofinality, and truth-lemma arguments. For each ZF formula in $\mathrm{\Delta }$, expand only the corresponding instance of F3's HS verification. Every displayed proof is finite and every schema occurrence has one fixed formula, so this traversal produces a finite list $\mathrm{\Gamma }$ of ground ZFC+GCH axioms and schema instances.

Include in $\mathrm{\Gamma }$ the finite definitions and absoluteness instances for the collapse order, automorphism action, normal filter, Boolean completion, name ranks, forcing relation, HS predicate, and evaluation that actually occur in step 1.1. Include also the finitely many Separation and Replacement instances used to collect the bounded layers and the selected $\mathrm{\Delta }$-axioms. This is a finite syntactic union; rank recursion contributes its one fixed formula instance, not one axiom for every rank.

Apply F2 to this fixed source fragment and forcing specification. In ambient ZFC+GCH obtain a countable transitive set $M\models \mathrm{\Gamma }$ containing the required parameters and an $M$-generic $G$. Inside the set extension $M[G]$, form the interpretations of the HS names from $M$. Since $M$ is a set, their interpretations form an externally bounded set $N_M\subseteq M[G]$. The retained instances from steps 1.1–2.1 prove that $N_M$ satisfies every ZF formula in $\mathrm{\Delta }$ and all three extra sentences.

The quantifier over $\mathrm{\Delta }$ is external: for each one fixed finite list, the preceding finite trace supplies its corresponding $\mathrm{\Gamma }$ and proof. If the ZF part of $\mathrm{\Delta }$ is empty, the same construction still gives the three explicit sentences in a nonempty set model. Nothing here asserts a single model of full ZFC, a countable transitive model of full ZF, or a uniform truth predicate. Ambient AC is used only through F2 as recorded by F4; the constructed target satisfies the negative choice sentence.

By F2, the given hypothesis implies $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{G}\mathrm{C}\mathrm{H})$. Suppose for contradiction that the target theory $T$ in the Statement is inconsistent. A formal refutation is a finite sequence, so it uses only a finite set $\mathrm{\Delta }$ of ZF axiom instances together with the three extra target sentences.

Apply F1 to exactly this externally fixed $\mathrm{\Delta }$. ZFC+GCH proves that there is a set structure satisfying every sentence used by the alleged refutation. The first-order soundness proof for that finite derivation then proves in ZFC+GCH that the structure satisfies a contradiction, while equality logic proves that no structure does. Hence ZFC+GCH would be inconsistent, contrary to step 1.1.

Therefore $T$ is consistent. The argument uses the finite set of formulas occurring in one hypothetical proof; it does not construct a set model of full ZF, invoke semantic completeness, or infer consistency from a merely external citation.

By F1, $(P,\mathcal{G},\mathcal{F})$ is a symmetric system and ${\mathsf{F}}_{\mathrm{t}\mathrm{f}}={\mathrm{H}\mathrm{S}}_{\mathcal{F}}^G$. The definition also supplies the exact finite-support fact later used by the tail argument; no finite-predicate presentation or equality of two model constructions is used in this step.

Apply F2 to this system. It gives $V\subseteq {\mathsf{F}}_{\mathrm{t}\mathrm{f}}\subseteq V[G]$, transitivity, and every ZF axiom and schema instance. Hence ${\mathsf{F}}_{\mathrm{t}\mathrm{f}}$ is the claimed inner model of ZF.

The legacy identifier records why this symmetric model appears on the Feferman page: its infinite coordinate-tail automorphism is the transform used in Feferman's tail-complement theorem. Feferman's ZF-model theorem concerns his different ramified hierarchy. The present ZF conclusion comes solely from F2 and does not identify the two models or revive the false literal union from F1.

The set $D=\{k:(r,k)\in \mathrm{dom}(Q)\}$ is finite. Let $k_0=0$ if $D=\mathrm{\varnothing }$, and otherwise let $k_0=1+\max D$. Define $a\in (2^{\omega \times \omega }{)}^V$ by $a(i,k)=1$ exactly when $i=r$ and $k\ge k_0$. By F1, $a$ induces an order automorphism ${\pi }_a$ of the forcing.

No point of $\mathrm{dom}(Q)$ belongs to the support of $a$, so ${\pi }_{a}Q=Q$. Because $r\ge m$, the flip $a$ lies in $H_m$. The support hypothesis therefore gives ${\pi }_a\dot{x}=\dot{x}$. F2 then transports any forced formula containing $\dot{x}$ while leaving both its condition and that name fixed.

We have ${\pi }_a{S}_i=S_i$ for $i\mathrm{\ne }r$, while ${\pi }_a{S}_r=S_r\mathrm{△}\{k:k\ge k_0\}$. Thus membership is reversed at every $k\ge k_0$ and preserved below $k_0$, so the following exact symmetric-difference identity holds.

The flip set is an infinite tail; only its intersection with the finite domain of $Q$ had to be empty. Replacing it by a finite flip would preserve membership in every free ultrafilter under finite modification and would not give step 2.2. The construction takes the maximum of one finite set and uses no Choice.

Suppose for contradiction that $I$ is not principal. For each $k<\omega$, primality applied to $\{k\}\cap (\omega \setminus \{k\})=\mathrm{\varnothing }\in I$ puts one of the two factors in $I$. If $\omega \setminus \{k\}\in I$, downward closure and propriety give $I=\{A\subseteq \omega :k\mathrm{\notin }A\}$, the principal prime ideal generated by that coatom. Thus $\{k\}\in I$ for every $k$, and finite-union closure puts every finite subset of $\omega$ in $I$.

Since $\dot{I}$ is HS, choose $m$ with $H_m\subseteq \mathrm{sym}(\dot{I})$, as in F1. Put $A=S_m$, which belongs to ${\mathsf{F}}_{\mathrm{t}\mathrm{f}}$ because its canonical name is supported by $H_{m+1}$. Since $A\cap (\omega \setminus A)=\mathrm{\varnothing }$, F2 yields either $A\in I$ or $\omega \setminus A\in I$. Let $C$ denote the member selected by these two exhaustive cases, and let $\dot{C}$ be the corresponding canonical name.

By F4 choose a finite $Q$ in the actual generic which forces $\dot{C}\in \dot{I}$. Apply F1 with the support bound $m$, condition $Q$, and coordinate $m$. Its tail automorphism $\pi$ fixes both $Q$ and $\dot{I}$. By F5, $Q=\pi Q$ forces $\pi \dot{C}\in \dot{I}$. Hence both $C$ and $\pi C$ belong to $I$ in the actual extension.

If $C=A$, then F1 gives $\pi C\mathrm{△}(\omega \setminus A)$ finite. If $C=\omega \setminus A$, automorphisms commute with Boolean complementation and F1 gives $\pi C\mathrm{△}A$ finite. Thus in either case $\pi C$ differs finitely from $\omega \setminus C$. By step 1.1 the finite difference belongs to $I$; since $\omega \setminus C\subseteq \pi C\cup (\pi C\mathrm{△}(\omega \setminus C))$, F2 puts $\omega \setminus C$ in $I$.

Step 2.1 gives $C\in I$ and step 3.1 gives its complement in $I$. Finite-union closure then puts $\omega$ in $I$, contradicting propriety. Therefore the assumption in step 1.1 was false, and every prime ideal is principal. Both decisions in step 1.2 lead to the same contradiction, and every finite-modification use was derived from the finite singletons rather than assumed.

First, maximality makes $U$ decide every $A\subseteq \omega$: if neither $A$ nor $\omega \setminus A$ belonged to $U$, then every $B\in U$ would meet $A$ (otherwise upward closure would put $\omega \setminus A$ in $U$), so the filter generated by $U\cup \{A\}$ would be a proper strict extension, contradicting F2. Thus exactly one of $A$ and its complement lies in $U$, since a proper filter cannot contain both.

Define $I=\{A\subseteq \omega :\omega \setminus A\in U\}$. Complementation converts upward closure to downward closure and intersections to unions, so $I$ is a proper ideal. If $A\cap B\in I$, then $(\omega \setminus A)\cup (\omega \setminus B)\in U$. Were neither complement in $U$, step 1.1 would put both $A$ and $B$ in $U$, and then $A\cap B\in U$, a contradiction. Hence $A\in I$ or $B\in I$, so $I$ is prime.

By F1 the ideal $I$ is generated by some $C\subseteq \omega$, so $I=\{A\subseteq \omega :A\subseteq C\}$. Propriety gives $C\mathrm{\ne }\omega$. Choose $k\in \omega \setminus C$. Since $I$ is prime and $\{k\}\cap (\omega \setminus \{k\})=\mathrm{\varnothing }\in I$, while $\{k\}⊈C$, we have $\omega \setminus \{k\}\in I$ and hence $\omega \setminus \{k\}\subseteq C$. Together with $k\mathrm{\notin }C$, this gives $C=\omega \setminus \{k\}$ and therefore $I=\{A\subseteq \omega :k\mathrm{\notin }A\}$. For every $B\subseteq \omega$, it follows that $B\in U$ iff $\omega \setminus B\in I$ iff $k\in B$. Thus $U$ is the principal ultrafilter at $k$ in the sense of F2. Since $U$ was arbitrary, no free ultrafilter on $\omega$ exists in the model.

Let $\mathcal{C}=\{A\subseteq \omega :\omega \setminus A\text{ is finite}\}$. It contains $\omega$, excludes $\mathrm{\varnothing }$ because $\omega$ is infinite, is upward closed, and is closed under finite intersections because the complement of an intersection is the finite union of the complements. Hence $\mathcal{C}$ is a proper set filter in the model.

Suppose BPI holds. By F3, the set Ultrafilter Lemma extends $\mathcal{C}$ to an ultrafilter $U$ on $\omega$. For every $k<\omega$, the cofinite set $\omega \setminus \{k\}$ belongs to $U$. But the principal ultrafilter at $k$ omits that set, so $U$ is not principal at any point and is free by F4. This contradicts F1.

Therefore BPI fails. Since F3 proves both directions of the equivalence, the set Ultrafilter Lemma fails as well. The empty-set UFL instance is vacuous, while the explicit nonempty witness is the cofinite filter on $\omega$ from step 1.1.