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.