What is Modified Realizability?
Peter Johnstone – 15 November 2017
Among the many variants of the realizability interpretation of constructive logic, modified realizability (first introduced by Georg Kreisel in 1959) has received less than its share of attention from topos-theorists. Previous work (Grayson 1981, Hyland and Ong 1993, van Oosten 1997) has largely concentrated on particular algebras such as the Kleene algebra, and has not addressed the question of how to define modified realizability over an arbitrary Sch"onfinkel algebra. In this talk I'll introduce the notion of `right pseudo- ideal' in a Sch"onfinkel algebra, and show that these suffice to define modified realizability toposes; to the extent that time permits, I'll also discuss the functoriality of the construction -- i.e., when do morphisms of Sch"onfinkel algebras induce geometric morphisms between modified realizability toposes?
Back