Limit Filters and Dependent Choice in Countable-Support Symmetric Iterations

TL;DR

This paper develops a method for constructing limit filters in countable-support symmetric iterations, ensuring the resulting symmetric models satisfy ZF and DC, and demonstrates applications to models with controlled failures of the Axiom of Choice.

Contribution

It introduces a novel construction of limit filters for symmetric iterations that guarantees ZF and DC in the resulting models, extending the understanding of choice failures in set theory.

Findings

Constructed limit filters are normal and ω₁-complete.

Symmetric models satisfy ZF and DC, but not AC.

Finite-support iterations fail DC at the ω-limit stage.

Abstract

We isolate the limit-stage filter construction needed for countable-support symmetric iterations built from standard successor-step symmetric systems. At successor stages we take the $\omega_1$-completion of the usual successor-stage symmetry filter. At limit stages of uncountable cofinality, countable supports are bounded and the direct-limit filter is $\omega_1$-complete by stage-bounding; at limits of cofinality $\omega$, we define the limit filter as the smallest normal $\omega_1$-complete filter extending the head-pullback generators. In all cases the resulting limit filter is normal and $\omega_1$-complete. Using these limit filters, we prove that the class of hereditarily symmetric names is closed under the operations required for ZF, that the resulting symmetric model satisfies ZF, and that over a ZFC ground it satisfies DC=DC_$\omega$. We also explain why no general class-length ZF-preservation theorem is claimed here, although specific class-length symmetric iterations may still be analyzable separately over a GBC background. As a self-contained application, we construct, for any uncountable cardinal $\kappa$ with cofinality greater than or equal to $\omega_1$, a model of ZF+DC+$\neg$AC_$\kappa(\mathcal{F})$, where $\mathcal{F}$ is a $\kappa$-indexed family of $2$-element sets of reals with no choice function. Each step of the iteration adds one unpickable pair, so the degree of AC-failure is controlled by the iteration length. We also prove that the analogous finite-support construction fails DC at the first $\omega$-limit stage, showing why $\omega_1$-complete limit filters are structurally needed for this application.