9
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ My guess is no. In 2006, looking at a use of computability theory in differential geometry, Csima and Soare called it "perhaps the first example of the use of c.e. sets to demonstrate specific mathematical or geometric complexity of a mathematical structure". projecteuclid.org/euclid.jsl/1164060462 $\endgroup$ – Matt F. May 9 at 10:58
  • $\begingroup$ @MattF. What does that quote have to do with this question? They have a very narrow focus ("specific mathematical or geometric complexity" of individual structures - in particular, ones occurring outside of mathematical logic), and even then I think that's rather overstated. If you're trying to infer that computability theory isn't useful outside of computability theory, that's just false - consider e.g. the role of hyperarithmeticity in proving the Harrington-Kechris-Louveau theorem. $\endgroup$ – Noah Schweber May 9 at 16:07
  • $\begingroup$ I saw Soare regularly in grad school and he knew of my interest in intuitionist logic; given the way that he trumpeted the applications to differential geometry, I think he would have told me of good applications in my area of interest. $\endgroup$ – Matt F. May 9 at 16:48
  • $\begingroup$ @MattF. Soare was my professor in undergrad - I learned computability through his (many) classes - and as far as I know intuitionism/etc. is not one of his areas of expertise. I don't think he would necessarily know about such results. Certainly much of his enthusiasm over the geometry results was, again, the fact that it lay outside logic, and this doesn't apply to realizability. $\endgroup$ – Noah Schweber May 9 at 17:47
  • $\begingroup$ (Strangely, a paper by him and Jockusch is given the tag "intuitionistic logic" on philpapers, but this is a complete misnomer; I suspect the reason comes from the appearance of the word "constructive" in the bibliography, but the word means something different there, and there's no nonclassical content in the paper. The paper itself is available here.) $\endgroup$ – Noah Schweber May 9 at 17:51
6
+200
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ This is quite interesting (and I have some reading to do now) - thanks! $\endgroup$ – Noah Schweber May 11 at 20:29
  • $\begingroup$ If you know of presentation of priority arguments which recast them as a "kind of" topology, or measure theory, or something that is not directly a combinatorial argument, then I'd be interested to know. $\endgroup$ – Andrej Bauer May 11 at 20:35
  • $\begingroup$ If I recall correctly, Lachlan tried to present a topological approach to priority arguments, but I never managed to track down a copy. (Incidentally, I've always thought there should be a good analogy between realizers and the true path for a priority argument, but I've not been able to make this usefully precise.) $\endgroup$ – Noah Schweber May 11 at 20:55
  • $\begingroup$ I think I had that paper in my hands. I'll see if I can get it. I couldn't penetrate it as my priority arguments mojo is quite weak. $\endgroup$ – Andrej Bauer May 11 at 21:54
  • $\begingroup$ By the way: realizability is not really limited to computability, for instance there are topological realizability models. So your question is specific to the kinds of realizability that use computational models which support priority arguments (basically Turing machines, I've never heard of priority arguments for lambda calculus, for instance). $\endgroup$ – Andrej Bauer May 12 at 10:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.