Explicit Turing reduction of $0''$ to TOT

Question

Let TOT be the set of indices of total recursive functions. It is standard that TOT is Turing-equivalent to $0''$, but this is typically proved by showing that TOT is $\Pi^0_2$-complete and then invoking Post's theorem.

I am hoping to find a more explicit proof of this Turing equivalence. It is simple enough to show that $\mathrm{TOT}\leq_T 0''$: one basically wants to make infinitely many calls to the halting oracle, and the extra jump does it for us in one go. But I cannot think of an intuitive reduction in the other direction.

Question: Is there a reasonably explicit/intuitive Turing reduction showing $0''\leq_T \mathrm{TOT}$?

Answer 1

Here is a possible way to see it: the condition $e\in \emptyset''$ can be written as

$$\exists s \, \exists\, \sigma\ (\varphi(\sigma) \land \{e\}^\sigma_s(e)\downarrow) $$ where $\varphi(\sigma)$ is the formula that says "$\sigma$ encodes the answers to the first $|\sigma|$ calls to the oracle", which is a $\Pi^0_1$ condition. Negating the formula you get $$\forall s \, \forall\, \sigma\ (\varphi(\sigma)\rightarrow \{e\}^\sigma_s(e)\uparrow) $$ Now, the condition $(\varphi(\sigma)\rightarrow \{e\}^\sigma_s(e)\uparrow)$ is $\Sigma^0_1$, hence we can write it as $(\exists n)(\psi(n))$ for some computable $\psi$. Consider now the function $f$ that maps $(s,\sigma)$ to the least $n$ s.t. $\psi(n)$ holds. In other words, $f$ searches for a witness of the fact that either $\sigma$ does not encode the answers to the first $|\sigma|$ oracle calls or that $\{e\}^\sigma_s(e)$ does not halt.

Clearly an index for $f$ is computable from $e$. It should be easy to check that $f$ is total iff $e\notin \emptyset''$, but I can elaborate if needed.