Limit Filters and Dependent Choice in Countable-Support Symmetric Iterations

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.