I have been trying to understand the proof of Baker-Gill-Solovay theorem as described in Complexity Theory: Modern Approach. I think I do understand most of it, but what troubles me is that let's say one can not easily see why $U_B \in NP^B$. If he rewrites the following proof about $P^B$ using non-deterministic oracle Turing machines then this seems to prove that $U_B$ is not in $NP^B$ either. Hence, there should be something in this proof that beaks if we try to use non-deterministic Turing machines. Could someone point out to me, what exactly does not work out?
I believe that the following is what breaks in translating the deterministic proof to non-determinism.
Suppose that the non-deterministic Turing machine $M_i$ rejects according to the condition in the text. Note that this means that all runs of $M_i$ reject, and we now have to pick some string of length $n$ which $M_i$ has not queried in any run. The proof as written relies heavily on the fact that in $ < 2^n$ steps a deterministic TM cannot query all strings of length $n$. But since we are talking about numerous "simultaneous" runs it is possible that all strings of length $n$ were queried in some run of $M_i$ of $< 2^n$ steps, making it impossible to choose a string as required. (If every string of length $n$ was checked in some run, then by declaring any string of length $n$ to be in $B$ would result in the "oracle" answering incorrectly in some run.)