Classical and relative realizability

Jaap van Oosten and Tingxiang Zou

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.

Keywords: realizability toposes, partial combinatory algebras, geometric morphisms, local operators, abstract Krivine structures, non-localic Boolean toposes

2010 MSC: 03B40, 03E99, 03B40,18B25

Theory and Applications of Categories, Vol. 31, 2016, No. 22, pp 571-593.

Published 2016-06-22.

http://www.tac.mta.ca/tac/volumes/31/22/31-22.pdf

TAC Home