Analytic determinacy and 0# A forcing-free proof of Harrington’s theorem

We prove the following theorem: Given a⊆ω and ${\displaystyle 1\le \alpha <{\omega }_1^{CK}}$, if for some ${\displaystyle \eta <{\aleph }_1}$ and all u ∈ WO of length η, a is ${\displaystyle {\Sigma }_{\alpha }^0\left(u\right)}$, then a is ${\displaystyle {\Sigma }_{\alpha }^0}$. We use this result to give a new, forcing-free, proof of Leo Harrington's theorem: ${\displaystyle {\Sigma }_1^1}$-Turing-determinacy implies the existence of ${\displaystyle 0^{\#}}$.