Woodin on Posner-Robinson for the hyperjump and sharp

MR2449474 (2009j:03067) Woodin, W. Hugh. A tt version of the Posner-Robinson theorem. Computational prospects of infinity. Part II. Presented talks, 355–392, Lect. Notes Ser. Inst. Math. Sci. Natl. Univ. Singap., 15, World Sci. Publ., Hackensack, NJ, 2008.

The proof is nice, invoking both recursion-theoretic and set-theoretic tools. Hugh uses a Prikry-like forcing notion, and considers forcing over countable non-standard $\omega$-models of (a large fragment of) set theory.

(For other examples of forcing over non-standard models, see Projective prewellorderings vs projective wellfounded relations by X. Shi, or the last few chapters of the monograph Super-real fields by Hugh and Garth Dales.)


This result by Woodin is stated as "unpublished" in a paper published by his former Ph.D. student Xianghui Shi in July 2015, so that seems to be an authoritative source:

Axiom $I_0$ and higher degree theory
The Journal of Symbolic Logic 80, 970-1021 (2015).