Jaap van Oosten: Classical and relative realizability
Date of publication: 17. 10. 2016
Mathematics and theoretical computing seminar
Torek, 18. 10. 2016, od 12h do 14h, Plemljev seminar, Jadranska 19
Abstract: J.-L. Krivine has employed a notion of realizability for interpretations of classical set theory. Thomas Streicher analyzed the underlying logical framework from a tripos theoretic point of view, by giving the notion of "abstract Krivine structure" and "Krivine triposes".
In the talk we shall present this material, and our result, obtained in joint work with Tingxiang Zou, that every Krivine topos is a Boolean subtopos of a relative realizabilty topos. We also give a host of examples of such suboposes of the Kleene-Vesley topos, which do not arise from triposes formed by complete Boolean algebras.
