Forcing More DC Over the Chang Model Using the Thorn Sequence

TL;DR

This paper explores forcing techniques within the Chang model under $ ext{ZF}+ ext{DC}$ to enhance dependent choice principles for relations on power sets of ordinals below $eth_ ext{omega}$, using the thorn sequence with specific assumptions.

Contribution

It introduces a method to force $ ext{DC}_oldsymbol{ ext{kappa}}$ in the Chang model leveraging the thorn sequence and specific assumptions about its regularity and justification.

Findings

Successfully forces $ ext{DC}_oldsymbol{ ext{kappa}}$ for certain relations.

Establishes conditions under which Cohen forcing can be applied in the Chang model.

Provides a framework connecting thorn sequence properties with choice principles.

Abstract

In the context of $\mathsf{ZF}+\mathsf{DC}$, we force $\mathsf{DC}_\kappa$ for relations on $\mathcal{P}(\kappa)$ for $\kappa{}<\aleph_\omega$ over the Chang model $\mathrm{L}(\mathrm{Ord}^\omega)$ making some assumptions on the thorn sequence defined by ${\it \unicode{xFE}}_0=\omega$, ${\it \unicode{xFE}}_{\alpha{}+1}$ as the least ordinal not a surjective image of ${\it \unicode{xFE}}_\alpha^\omega$ (i.e. no $f:{\it \unicode{xFE}}_{\alpha}^\omega{}\rightarrow {\it \unicode{xFE}}_{\alpha{}+1}$ is surjective) and ${\it \unicode{xFE}}_\gamma{}=\sup_{\alpha{}<\gamma}{\it \unicode{xFE}}_\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 cardinals $\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 allow us to use Cohen forcing and establish more dependent choice.