Mice with finitely many Woodin cardinals from optimal determinacy hypotheses

Abstract

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

121 pages