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
    0 references
    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
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    relative realizability
    0 references
    modified realizability
    0 references
    ralizability topos
    0 references
    partial combinatory algebras
    0 references
    Sierpiński topos
    0 references