Analytic determinacy and $0^{\# }$ A forcing-free proof of Harrington’s theorem
Ramez L. Sami · Fundamenta Mathematicae · 1999
We prove the following theorem: Given a⊆ω and $1 ≤ α < ω_1^{CK}$, if for some $η < ℵ_1$ and all u ∈ WO of length η, a is $Σ _α^0(u)$, then a is $Σ_α^0$. We use this result to give a new, forcing-free, proof of Leo Harrington's theorem: $Σ_1^1$-Turing-dete