Relative and modified relative realizability (Q1849865): Difference between revisions

The notion of relative realizability, originally due to Kleene and Vesley, has recently been studied in topos-theoretic terms by the first author of this paper together with \textit{S. Awodey} and \textit{D. S. Scott} [``Local realizability toposes and a modal logic for computability'', Math. Struct. Comput. Sci. 12, 319-334 (2002; Zbl 1007.03057)]. The topos-theoretic version of Kleene's modified realizability was studied by the second author in ``The modified realizability topos'' [J. Pure Appl. Algebra 116, 273-289 (1997; Zbl 0882.03059)]. In the present paper, the authors show how the two notions may be combined, by regarding an inclusion (\(A_{\sharp}\subseteq A\)) between partial combinatory algebras as an internal PCA in the Sierpiński topos; in this setting, the relative realizability topos of the pair \((A,A_{\sharp})\) appears as an open subtopos of the realizability topos of this internal PCA, and its closed complement yields a `relative modified realizability' topos. This point of view makes it easy to construct various functors between the different realizability toposes under consideration.