Forcing more $\mathsf {DC}$ over the Chang model using the Thorn sequence

Abstract:

In the context of $\mathsf {ZF}+\mathsf {DC}$, we force $\mathsf {DC}_\kappa$ for relations on $\mathcal {P}(\kappa )$ for arbitrarily large $\kappa <\aleph _\omega$ over the Chang model $\mathrm {L}(\mathrm {Ord}^\omega )$ making some assumptions on the thorn sequence defined by $Þ_0=\omega$, $Þ_{\alpha +1}$ as the least ordinal not a surjective image of $Þ_\alpha ^\omega$ and $Þ_\gamma =\sup _{\alpha <\gamma }Þ_\alpha$ for limit $\gamma$. These assumptions are motivated from results about $\Theta$ in the context of determinacy, and could be reasonable ways of thinking about the Chang model. Explicitly, we assume successor points $\lambda$ on the thorn sequence are strongly regular—meaning regular and functions $f:\kappa ^{<\kappa }\rightarrow \lambda$ are bounded whenever $\kappa <\lambda$ is on the thorn sequence—and justified—meaning $\mathcal {P}(\kappa ^\omega )\cap \mathrm {L}(\mathrm {Ord}^\omega )\subseteq \mathrm {L}_{\lambda }(\lambda ^\omega ,X)$ for some $X\subseteq \lambda$ for any $\kappa <\lambda$ on the thorn sequence. This allows us to use Cohen forcing and establish more dependent choice while preserving the thorn sequence and calculating it: $Þ_i=\aleph _{i+1}$ for $0<i<\omega$ after $i$ steps in the iteration.