The modified realizability topos (Q678851): Difference between revisions

The modified realizability topos [see \textit{J. M. E. Hyland} and \textit{L. Ong}, ``Modified realizability toposes and strong normalization proofs'', in: M. Bezem et al. (eds.), Typed Lambda Calculi and Applications, Lect. Notes Comput. Sci. 664, 179-194 (1993; Zbl 0793.03079)] is the semantic counterpart of a variant of Kreisel's modified realizability. This topos is here analyzed as a closed subtopos of the ``effective topos built on sheaves on the Sierpinski space'' (with the open complement being the ordinary effective topos of Hyland). An interesting logical principle holds in this larger topos, and this has also some consequences for modified realizability.