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

From Machinelearning
Revision as of 03:41, 15 September 2018 by IssaRice (talk | contribs)

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)={w such thaty<wz<wSxyzw exists
h(x,w)={y<w such thatz<wSxyzy exists

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

f(x)={y such thatzSxyzy exists

Of course, the relation 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.