Relative and modified relative realizability (Q1849865)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Relative and modified relative realizability |
scientific article |
Statements
Relative and modified relative realizability (English)
0 references
2 December 2002
0 references
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.
0 references
relative realizability
0 references
modified realizability
0 references
ralizability topos
0 references
partial combinatory algebras
0 references
Sierpiński topos
0 references
0 references