Deep effectively closed sets

We know from Gödel's theorem that there is no deterministic algorithm to generate a coherent completion of Peano Arithmetic (PA). But could there be a probabilistic algorithm which achieves this with positive probability? As one can expect, the answer is also negative, by a result of Jockusch and Soare (1972). In the early 2000, Levin and Stephan independently improved Jocksuch and Soare's result; using essentially the same technique, but with different motivations, they respectively showed that (1) Any probabilistic algorithm has probability at most $2^{-n}$ to generate a coherent completion of PA restricted to formulas of "size" n and (2) if a Martin-Löf random real X computes an coherent extension of PA, then it in fact computes the halting problem. We will present the Levin-Stephan argument, and if time permits explain how to generalize their argument to many classes of problems (other than coherent extensions of PA), which we call deep effectively closed sets.
This is joint work with Chris Porter and Antoine Taveneaux.