So I'm looking at the proof of the ZBC lemma in Odifreddi's Classical Recursion Theory volume 2 page 808 and I don't see why $ 0' \oplus C$ produced computes $B'$ as claimed. The positive requirements try and code $$ P^C_e: \; x \in C^{[e]} \iff (\exists z > x) B^{[e]}(x) \not= B^{[e]}(z) $$

Now if these requirements always succeeded we would be great. We could read off from $C^{[e]}$ the point at which $B^{[e]}$ achieved its limit and from that compute $W$ which in turn computes $B'$. However, higher priority negative requirements might restrain $P^C_e$ from acting. These requirements have the form. $$ N^C_e : \; (\exists_\infty s)(\phi^{B\oplus C_s}_{e,s}(e)\downarrow) \implies \phi^{B\oplus C}_{e}(e)\downarrow $$

However, since $B$ isn't low we can't guarantee that $0'$ can tells us whether or not such a higher priority negative requirement might be falsely resulting in $C^{[e]}(x)=0$ so how do we actually conclude that $B' \leq_T 0' \oplus C$?

While I'm at it am I correct in presuming that the only reason that one can assume we meet the negative requirement for $B$ is that we assumed $C$ meets its own negative requirements above. This almost makes me think the right proof would build them simultaneously so they satisfied a requirement more like

$$ N^C_e : \; (\exists_\infty s)(\phi^{B^{e}_s\oplus C_s}_{e,s}(e)\downarrow) \implies \phi^{B\oplus C}_{e}(e)\downarrow $$

where $$B^{e}_s(x) = \begin{cases} B(x) & \text{ if } x = <i,y> \land i \leq e \\ B_s(x) & \text{ otherwise } \end{cases} $$

That way one could get some kind of induction off the ground where $0'$ would be able to determine if the next negative requirement ever engaged using the knowledge of $B'$ restricted to $e$. Or is there some easier trick I'm missing?

Note that the reason I'm interested is that I wanted to see if I could extend the ZBC theorem so that given r.e. set $A$ and set $W$ r.e. in $A$ it produced $B, C$ with $B \oplus C \leq_T A \oplus W$ and $(B \oplus C)' \equiv_T 0'\oplus B \oplus C \equiv_T 0' \oplus W$. So thoughts about that are appreciated as well.


A proof of Harrington’s ZBC Lemma can be found in Theorem 2.5 of

Hinman, Peter G.; Slaman, Theodore A., Jump embeddings in the Turing degrees, J. Symb. Log. 56, No. 2, 563-591 (1991). ZBL0745.03036.

It consists of a finite injury construction on top of an infinite injury construction. So it sounds like you're on the right track.

  • $\begingroup$ Excellent! Thanks1 $\endgroup$ – Peter Gerdes Dec 20 '18 at 8:12

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.