Analytic determinacy and 0# A forcing-free proof of Harrington’s theorem
We prove the following theorem: Given a⊆ω and , if for some and all u ∈ WO of length η, a is , then a is . We use this result to give a new, forcing-free, proof of Leo Harrington’s theorem: -Turing-determinacy implies the existence of .