User:IssaRice/Computability and logic/First graph principle using a semirecursive relation

This is about proposition 7.17 (first graph principle) in Boolos, Burgess, Jeffrey's Computability and Logic.

The proof in the book defines two functions as follows:

$g(x)=\{\begin{array}{c}w\text{ such that}\\ \mathrm{\exists }y<w\mathrm{\exists }z<wSxyz& w\text{ exists}\\ & \end{array}$

$h(x,w)=\{\begin{array}{c}y<w\text{ such that}\\ \mathrm{\exists }z<wSxyz& y\text{ exists}\\ & \end{array}$

How would one discover such functions? It seems like a first attempt would be:

$f(x)=\{\begin{array}{c}y\text{ such that}\\ \mathrm{\exists }zSxyz& y\text{ exists}\\ & \end{array}$

Of course, the relation $\mathrm{\exists }zSxyz$ is semirecursive, not recursive, and this is the problem.

If the relation were recursive, then by proposition 7.9 we would know that $f$ is recursive. So the next question is, what is so special about the recursive relation in proposition 7.9? Can we replace it by a semirecursive relation and get a similar result?

If the characteristic function was recursive (and total) then it seems like we would be able to use the same proof. But in the case of a semirecursive relation, the characteristic function is not necessarily recursive.

What if we use the semicharacteristic function? The problem now is that a semicharacteristic function only takes on the value 1 (where it is defined), so the minimization will just be undefined everywhere.

Since the proof of proposition 7.9 uses the characteristic function of $\sim R$, we might use a "bit-flipped" semicharacteristic function $g$ defined by $g(x,y)=\stackrel{\mathrm{g}}{\mathrm{s}}(c(x,y))$, where $c$ is the semicharacteristic function of $\mathrm{\exists }zSxyz$. Now $g$ only takes on the value 0 (where it is defined). This means the minimization will return after the first step, returning 0, or else is undefined.

I guess the upshot here is that it's really nice to have a recursive characteristic function because the minimization works to define a useful function.