Any advantages of using Gödel universal functions in proving unsolvability? Let $U$ be a universal function for the class of computable functions of one variable. This means that $U:N\times N\to N$ is a computable (partial) function and for every computable (partial) function $f$ there exists $n\in N$ such that for all $x\in N$ one has $f(x)=U(n,x)$. 
Consider the set $O=\{p:U(p,0) \text{ is defined}\}$. Below, in the quoted text, is a proof of the fact that $O$ is not decidable that uses $m$-reducibility (essentially, this proof written a bit differently). 
I was told that the quoted proof below implicitly uses a Gödel universal function. A Gödel universal function is a universal function with the following property: if $V:N\times N\to N$ is any partial computable function, then there exists a total computable $s:N\to N$ such that for all $x,n\in N$ one has $V(n,x)=U(s(n),x)$. 
I suppose  a Gödel universal function can be used as follows.  Define $V:N\times N\to N$, $$(q,x)\mapsto 1\text { if } U(q,q) \text{ is defined}; \\(q,x)\text{ is undefined if } U(q,q) \text{ is undefined}$$
This is a computable function (a program that computes it accepts $(q,x)$, forgets $x$ and returns $U(q,q)$ (if $U(q,q)$ is undefined, then the program will run forever)). So there is a total computable $s$ such that $U(s(q),x)=V(q,x)$. This $s$ $m$-reduces $S$ (see the definition of $S$ below) to $O$.
My question is why the use of this Gödel universal function make the proof (I'm assuming I wrote the proofs correctly, if not, let me know) any more rigorous (or does it?) Are there any advantages in using the above argument as opposed to the below argument? Or is the proof below rigorous enough by itself? Should I try using the above technique in proving facts like this (maybe there are some hard problems for which an argument as below doesn't work)? 

Consider $S=\{q:U(q,q)\text{ is defined}\}$. We show that $S\le_m O$ (the result will follow).
  We need to define a computable $f:N\to N$ such that  $q\in S\iff f(q)\in O$.
Define $p=f(q)$  to be the following program:
  
  
*
  
*it accepts $x$
  
*it runs $U(q,q)$
  
*it returns $1$
This function is computable as pointed out in the link above. 
Now if $U(q,q)$  is defined, then $p$ halts on all inputs. Otherwise it halts on no input. It follows that $q\in S\iff f(q)\in O$.

 A: Note that your two versions of the halting problem make sense for arbitrary numberings in place of $U$; given a numbering $V$ I'll write "$S_V$," "$O_V$" for those analogues, and "$S_U$" and "$O_U$" in place of the original "$S$" and "$O$".
Also, below I write "$\downarrow$" for "is defined" and "$\simeq$" for equality of partial functions.

Yes, there is an issue with that argument.
The hairline crack in the wall that eventually brings it down is a type ambiguity: what exactly does "program" mean?
Sometimes we use the term "program" in a precise way, e.g. "Python program," in which case it is morally equivalent to "$V$-index"$^1$ for some appropriate $V$. Other times however we use it synonymously with "informal algorithm." In practice this conflation is largely justified, since we can "easily" convert informal algorithms to $V$-indices for the $V$s corresponding to the programming languages we use. However, in this case it matters a lot, since speaking in terms of informal algorithms winds up hiding some essential details.
We'll ultimately be using "program" in its precise sense, since the punchline of the argument occurs when we ask whether $f(q)$ is in $O$. However, $f(q)$ itself is presented as an informal algorithm. In doing ths you've tacitly assumed that we can in fact translate informal algorithms into $U$-indices in an appropriate way.
Certainly for some universal functions this is true: taking $P$ to be the universal function corresponding to your favorite programming language, the whole point of programming in the first place is that we can "easily" convert informal algorithms to $P$-indices. However, this doesn't mean that we can translate from informal algorithms to $U$-indices for arbitrary $U$. And this is a problem. Your argument does tell us how to go from a $U$-index $q$ to a $P$-index $p$ such that $p\in S_P$ is defined iff $q\in O_U$ is defined, but we don't want that since we're trying to reduce $O_U$ to $S_U$.
We need to take that $P$-index and turn it into a $U$-index. We can do this by adding an assumption on $U$, basically saying that any other computable listing of partial computable functions can be "folded in" to $U$ in a computable way. This property of numberings is called acceptability, and without it things can get pretty darn nasty ($[1]$, $[2]$). Acceptability will let us many-one reduce any $S_V$ to $S_U$ - that is to say, the following are equivalent:

*

*For some $V$, the set $S_V$ is incomputable.


*For every acceptable $U$, the set $S_U$ is incomputable.
After proving this equivalence, we then wrap up the proof of "$S_U$ is incomputable for every acceptable $U$" by rigorously proving the incomputability of $S_P$ for some fixed $P$. The good news is that we get to choose the $P$ here, so things will be nice and concrete; the bad news is that at this point we actually have to dig into the details of $P$, so things will be annoying and tedious.
(Alternatively, after choosing an "obviously good" $P$ we can just shout "Church-Turing thesis!" and scuttle off into the night. On that note, see the philosophical coda below.)

Mathematical coda
The above analysis raises a couple worrying questions:

*

*Need $S_U:=\{q: U(q,0)\downarrow\}$ be incomputable given only the weaker hypotheses on $U$?


*For that matter, what about $O_U:=\{q: U(q,q)\downarrow\}$? We've taken that for granted, but did we secretly use acceptability in that initial argument?
The situation is deeply weird. $O_U$ is guaranteed to be incomputable since the usual proof doesn't assume acceptability, but I believe we can modify the usual construction of a Friedberg numbering to get a $U$ such that $S_U$ is computable! This argument is messy - hence "I believe" - but here's why we might expect this sort of nonsense:
Roughly speaking, the difference between the $O$s and the $S$s is all about degrees of freedom. When we argue that $O_U$ is incomputable we don't need to know the index of the function we whip up: "run $U(p,p)$ and halt and output $0$ iff $U(p,p)\downarrow$ and don't halt otherwise" corresponds to some $U(n,-)$ and it doesn't matter which. By contrast, when we (try to) argue that $S_U$ is incomputable we only get one shot at diagonalization since we have to "get it right (or wrong?)" on input $0$. So to prove that $S_U$ is incomputable we do seem to need to know the $U$-index of the function we're building as we build it - which leans on the Recursion Theorem, which leans on acceptability.
The moral of the story is that unacceptable numberings are unacceptable.

Philosophical coda
Note that the above really illuminates a subtlety in the Church-Turing thesis: we don't just claim that the partial computable functions correspond exactly to the "informal algorithmic" functions, but rather that there is some computable enumeration of the partial computable functions $P$ such that there is an "informal algorithm" map for turning an "informal algorithm" into a $P$-index following it. This "one-level-up" aspect of the Church-Turing thesis is often not stated explicitly, which is a shame since it's important (and makes the thesis itself a bit less obvious at first!).
Here are a couple comments about this subtlety I think are worth making at this point (I'll write "$\mathsf{CTT}$" for the strong version of the Church-Turing thesis in the previous paragraph, and "$\mathsf{CTT_0}$" for the weaker one which just says that informal algorithmic functions and partial computable functions coincide):

*

*We can see how these two versions of the thesis work differently by looking in more detail at your original idea for constructing $f$. Thinking thesily, we first use $\mathsf{CTT}$ to get a very nice $P$. With this in mind, we write an informal algorithm $\alpha$ for taking a given $U$-index to a related $P$-index. Both $U$- and $P$-indices are just natural numbers, so we can apply $\mathsf{CTT}_0$ to the informal algorithm $\alpha$ to get a corresponding partial computable function, and this is your $f$. I think this breakdown of which thesis is used where helps clarify things.


*Next, from a practical standpoint note that $\mathsf{CTT}$ is the "right" version of the thesis to have in mind. Accepting $\mathsf{CTT_0}$ but rejecting $\mathsf{CTT}$ amounts to saying "Sure, I believe that every algorithm can be implemented by a Turing machine, but I have no idea how to actually do that." Besides being weird, this contradicts how we actually use the thesis, namely as a substitute for actually writing down the specific objects we care about. So $\mathsf{CTT_0}$, while interesting on its own, doesn't actually let us do what we want to do with it.


*Finally, on a more wishy-washy note it may also help to think of $\mathsf{CTT}$ as saying that $\mathsf{CTT_0}$ is un-accidentally true: the informal algorithmic and partial computable functions don't just happen to coincide, but rather coincide because of an overall good behavior.

$^1$Note that the term "$V$-index" here is purely intensional: no matter what $V$ is, the $V$-indices are just the natural numbers. "$V$-index" is just a context clue indicating how that number will be thought of in the rest of the argument.
