A countable-support symmetric iteration separating PP from AC

Abstract

We construct, from a ground model of $ZFC$, a transitive symmetric model $M$ satisfying $ZF+DC+PP+A{C}_{wo}+\neg AC$. The construction starts with a Cohen symmetric seed model $N$ over $Add(\ddot{I}‰,\ddot{I}{‰}_1)$ and performs an Ord-length countable-support symmetric iteration. For fixed parameters $S:=A^{\ddot{I}}‰$ and $T:=PowerSet(S)$ (as computed in $N$), successor stages add orbit-symmetrized packages which force the localized splitting principle $P{P}^{\mathrm{split}}\upharpoonright T$ (hence $PP\upharpoonright T$) and the choice principle $A{C}_{wo}$, while preserving $DC$ and keeping $A$ non-well-orderable. A diagonal-lift/diagonal-cancellation scheme produces $\ddot{I}{‰}_1$-complete normal limit filters. A persistence argument yields $SV{C}^{+}(T)$ in M, and Ryan--Smith localization then upgrades $PP\upharpoonright T$ and $A{C}_{wo}$ to $PP$.

updated with corrections and notes, one Gap remains