Mice with Finitely many Woodin Cardinals from Optimal Determinacy Hypotheses

(with R. Schindler and W. H. Woodin)

Submitted. PDF. Bibtex.

We prove the following result which is due to the third author. Let $n \geq 1$. If $\boldsymbol\Pi^1_n$ determinacy and $\Pi^1_{n+1}$ determinacy both hold true and there is no $\boldsymbol\Sigma^1_{n+2}$-definable $\omega_1$-sequence of pairwise distinct reals, then $M_n^\sharp$ exists and is $\omega_1$-iterable. The proof yields that $\boldsymbol\Pi^1_{n+1}$ determinacy implies that $M_n^\sharp(x)$ exists and is $\omega_1$-iterable for all reals $x$. A consequence is the Determinacy Transfer Theorem for arbitrary $n \geq 1$, namely the statement that $\boldsymbol\Pi^1_{n+1}$ determinacy implies $\Game^{(n)}(<\omega^2 - \boldsymbol\Pi^1_1)$ determinacy.