arXiv · 1603.03621
Classical and Relative Realizability
Abstract
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 Booleanization of a closed subtopos of RT(A',A). We exhibit a range of non-localic Boolean subtoposes of the Kleene-Vesley topos.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Jaap van Oosten, Tingxiang Zou. 2016-03-11. Classical and Relative Realizability. https://arxiv.org/abs/1603.03621
Cite the original work for its findings. Save a collection to share your selection of sources.