Journal of Mathematical Logic. Volume 20, Issue Supp01, October 2020. 1950013.
DOI: 10.1142/S0219061319500132. PDF. arXiv.
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.