Classical and relative realizability
Theory and applications of categories, Tome 31 (2016), pp. 571-593
Cet article a éte moissonné depuis la source Theory and Applications of Categories website
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/