Abstract

One aim of the theory of realizability toposes is to give a conceptual and semantic account of the various realizability interpretations one can find in the proof-theoretic literature. But there is no direct route which goes from a proof-theoretic interpretation to its “corresponding” topos. In fact, one quickly finds that one has to make some choices on the way. I will discuss some of the issues that come up when one tries to define a modified realizability topos. Recall that the proof theorist (Kreisel, Troelstra) will think of modified realizability as an interpretation of arithmetic in finite types which validates independence of premise and the axiom of choice for all finite types. In the literature (Van Oosten’s book, for instance) one can find a modified realizability topos, due to Grayson, but it does not validate the axiom of choice for all finite types. I will discuss two possible ways in which this can be fixed. If time permits, I may even discuss a fourth topos which also has some claim to being a topos for modified realizability. (Joint work with Mees de Vries)