Turing degree of finding independent formulas

Question

In this Paper of D. Isaacson, it is proved that the true arithmetic($Th(\mathbb{N}$)) is the only $\omega$-consistent and complete extension of $Q$ (Robinson's arithmetic). This, together with the fact that $Th(\mathbb{N})$ is not definable, immediately implies the following result:

Proposition. If $T\supseteq Q$ is a $\omega$-consistent theory such that the set of (Godel numbers of ) axioms of $T$ is definable by a $\Sigma_n$ (or $\Pi_n$) formula (for some $n\in \mathbb{N}$), then $T$ is incomplete.

It can be proved that this incompleteness phenomenon is essentially non-constructive, which means that there is no computable function $f$ such that for every formula $\sigma(x)$ which defines the set of (Godel numbers of) axioms of an $\omega$-consistent theory $T$, then $f(\ulcorner\sigma(x)\urcorner)\downarrow=\theta$ and $\theta$ is a sentece independent from $T$. It is the case even when we restrict the problem to $\Sigma_4$ formulas. The idea of the proof is as follows:

$\omega$-consistency of a r.e. theory can be written as a $\Pi_3$ formula. By using the parametric version of the diagonal lemma, we can construct a formula $\psi(x)$ such that : $Q\vdash \psi(x)\equiv [f(\ulcorner \psi \urcorner)\downarrow \wedge \omega\text{-}con(Q+f(\ulcorner \psi \urcorner)) \wedge (x=q \vee x=f(\ulcorner \psi \urcorner))] \vee$ $[f(\ulcorner \psi \urcorner)\downarrow \wedge \omega\text{-}con(Q+\neg f(\ulcorner \psi \urcorner)) \wedge (x=q \vee x=\neg f(\ulcorner \psi \urcorner))]\vee$ $[x=q]$

Where $q$ is the Godel number of conjunction of all axioms of $Q$. Now it is not hard to check that $\psi(x)$ is a $\Pi_3$ and then $\Sigma_4$ formula which defines a $\omega$-consistent theory $T_\psi$, but $f(\psi)$ is not independent from $T_\psi$ (see this preprint for more details).

So there is no computable $f$ with the desired property, even when we restrict the problem to $\Sigma_4$-definable theories. My question is about Turing degree of a function like $f$. Obviously one can enumerate the graph $f$ by oracle $0^{(4)}$ (because for a given $\Sigma_4$-definable theory, the problem of provability or refutability of a given sentence can be decided by oracle $0^{(4)}$). Hence it is a $0^{(4)}$-r.e. set, so its Turing degree is less that (or equal to) $0^{(5)}$.

Question: Is this Turing degree (necessarily) $0^{(5)}$ or it can be strictly less than $0^{(5)}$?

Answer 1

From your use of "$\downarrow$" it seems you do not require $f$ to give an answer on non-$\omega$-consistent theories.

At least we can get a function $f$ partial computable in $0^{(3)}$ (perhaps you already knew this).

We just go through the $\Sigma_3$ formulas $\sigma$ defining the axioms of theories $T$, and ask, given an input $\theta$,

Is there a proof or disproof in $T$ of $\theta$?

This is a $\Sigma^0_3$ property so $0^{(3)}$ can give a definite answer yes/no. If no, we let $f(\sigma)\downarrow=\theta$. If yes, we move on to the next $\theta$.