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 + AC_{wo} + \neg AC$. The construction starts with a Cohen symmetric seed model $N$ over $Add(\omega,\omega_1)$ and performs an Ord-length countable-support symmetric iteration. For fixed parameters $S:=A^\omega$ and $T:=PowerSet(S)$ (as computed in $N$), successor stages add orbit-symmetrized packages which force the localized splitting principle $PP^{\mathrm{split}}\!\restriction T$ (hence $PP\restriction T$) and the choice principle $AC_{wo}$, while preserving $DC$ and keeping $A$ non-well-orderable. A diagonal-lift/diagonal-cancellation scheme produces $\omega_1$-complete normal limit filters. A persistence argument yields $SVC^+(T)$ in M, and Ryan--Smith localization then upgrades $PP\restriction T$ and $AC_{wo}$ to $PP$.