Computability-theoretic results relevant to realizability

Question

This may be a very naive question which only reflects my failure at literature search, but:

Although realizability (in its original form at least) is grounded in computability, the details of computability theory itself don't seem too relevant for realizability as far as I can tell. For example, I don't know of any result in realizability which relies on (say) the Low Basis Theorem or on the solution to Post's problem. Basic computability of course plays a role - e.g. whipping up realizability semantics appropriate for computability notions which lack universal machines, such as the primitive recursive functions, is difficult and interesting - but (to my practically-nonexistent knowledge) the deeper results don't seem to play a role.

My question is whether this is accurate. In particular, I'd be extremely interested in any significant role played by priority arguments in realizability.

The most relevant thing I've found is Charles McCarty's paper "Realizability and recursive set theory", which established a connection between isols/recursive equivalence types and realizability. There are many results about isols, of course, which are proved via complicated priority arguments. However, unless I'm missing something this seems to be a situation where realizability sheds light on the isols, rather than results about isols being relevant to realizability.

Answer 1

Many results of computability theory can be stated synthetically in the effective topos. I have dubbed this idea "synthetic computability" and have tried to develop as much computability this way as I can. Some examples of how classical theorems in computability theory are stated synthetically:

• "There is no computable enumeration of total recursive functions" becomes "The set of functions $\mathbb{N} \to \mathbb{N}$ is uncountable" in the internal language of the effective topos.
• "There is a computable enumertion of computably enumerable sets" becomes "There are countably many countable subsets of $\mathbb{N}$".
• "There is a c.e. set whose complement is not c.e." becomes "there is a countable subset of $\mathbb{N}$ whose complement is not countable".
• "There is an immune set" becomes "there is a subset of $\mathbb{N}$ which is neither finite nor infinite".

One can keep going this way. So far I have been stuck on obtaining a suitable synthetic definition of Turing reducibility. I have one, but I am not completely happy with it. Intermediate degrees are also out of my reach, although it looks like they should translate to results about measure theory, or perhaps descriptive set theory, I am not sure. Essentially, a priority argument feels a bit like showing that a certain intersection of open sets is non-empty, but it's subtle.

The only other place where I would look for the kinds of results that you are asking about is perhaps the work of Jaap van Oosten, in particular his study of the subtoposes of the effective topos (I am not sure how much is published). It seems exceedingly hard to get a grip on the Lawvere-Tierney $j$-operators in the effective topos, and this may be related to some complicated structures in computability.

There is a general principle: in order for a result $A$ in computability theory to have significance in realizability, you need to find an intuitionistic statement $B$ such that validity of its realizability interpretation is related to $A$. I started to study synthetic computability more seriously when I discovered that the Recursion theorem corresponds to a variant of Lawvere's fixed-point theorem (see this paper¹).

Until we find out what priority arguments correspond to under realizability interpretation, we pretty much have no clue how to use them.

¹Bauer, Andrej, On fixed-point theorems in synthetic computability, Tbil. Math. J. 10, No. 3, 167-181 (2017). Author's website, ZBL1403.03076, MR3725758.

Answer 2

This wasn't exactly what I had in mind when I first asked this question, but I don't think it's unrelated either: combining realizability (in a very naive way) with classical computability-theoretic arguments yields results in "reverse constructive recursion theory."

Consider the following principle:

• $(\mathsf{FM})\quad$ There are numbers $c_0,c_1$ such that for each $e$ and each $i\in\{0,1\}$ there is an $n$ such that for every $s$ there is a $t>s$ with $$\neg\Phi_e^{W_{c_i, t}}(n)[t]\downarrow=W_{c_{1-i}, t}(n)$$ (note that that final expression is $\Delta_0$, so "uncomplicated").

All of the complexity of $(\mathsf{FM})$ rests in the choice of $n$ given $e$. A priori, if $W_{c_0}$ and $W_{c_1}$ are Turing-incomparable, we are only guaranteed such a function computable in ${\emptyset''}$, but the finite injury nature of the proof of Friedberg-Muchnik gives us a pair of indices with a $\emptyset'$-computable such function. Put another way, Friedberg-Muchnik is "$\emptyset'$-realizable."

The usual proof that every (intuitionistic) theorem of $\mathsf{HA}$ is realizable relativizes to any degree, so any (intuitionistic) theorem of $\mathsf{HA+\mathsf{FM}}$ must also be $\emptyset'$-realizable. Meanwhile, it's easy to show that e.g. the existence of a maximal c.e. set (phrased in any reasonable way) is not $\emptyset'$-realizable in the same sense. So we get for free a theorem in "constructive reverse recursion theory," namely that $(\mathsf{FM})$ does not imply the existence of a maximal c.e. set over $\mathsf{HA}$.

Now admittedly this is extremely artificial, but I think the analogy between true paths and (relative-to-an-oracle-)${}$realizers (and some related questions, e.g. here) is potentially interesting.