Classical and relative realizability
Theory and applications of categories, Tome 31 (2016), pp. 571-593
We show that every abstract Krivine structure in the sense of Streicher can be obtained, up to equivalence of the resulting tripos, from a filtered opca (A,A') and a subobject of 1 in the relative realizability topos RT(A',A); the topos is always a Boolean subtopos of RT(A',A). We exhibit a range of non-localic Boolean subtriposes of the Kleene-Vesley tripos.
Publié le :
Classification :
03B40, 03E99, 03B40, 18B25
Keywords: realizability toposes, partial combinatory algebras, geometric morphisms, local operators, abstract Krivine structures, non-localic Boolean toposes
Keywords: realizability toposes, partial combinatory algebras, geometric morphisms, local operators, abstract Krivine structures, non-localic Boolean toposes
@article{TAC_2016_31_a21,
author = {Jaap van Oosten and Tingxiang Zou},
title = {Classical and relative realizability},
journal = {Theory and applications of categories},
pages = {571--593},
year = {2016},
volume = {31},
language = {en},
url = {http://geodesic.mathdoc.fr/item/TAC_2016_31_a21/}
}
Jaap van Oosten; Tingxiang Zou. Classical and relative realizability. Theory and applications of categories, Tome 31 (2016), pp. 571-593. http://geodesic.mathdoc.fr/item/TAC_2016_31_a21/