Universiteit van Amsterdam


Institute for Logic, Language and Computation

9 February 2017, Colloquium on Mathematical Logic, Andrew Swan

Speaker: Andrew Swan (ILLC)
Title: Lifschitz Realizability as a Topological Construction
Date: Thursday 9 February 2017
Time: 16:00-17:00
Location: F1.15, Science Park 107


Lifschitz realizability is a form of realizability with the unusual property that the omniscience principle LLPO holds in the model alongside a form of Church's thesis: all functions N -> N are computable. Jaap van Oosten proved that there is a Lifschitz realizability topos and the remarkable result that the Lifschitz realizability topos can be viewed as a topos of sheaves over a Lawvere-Tierney topology in the effective topos. We are developing a new presentation of this result. Instead of topos theory we work in constructive set theory, and instead of Lawvere-Tierney topology and sheaves we use a topological model over formal topologies developed by Nicola Gambino. We show that the Lifschitz realizability model for IZF developed by Rathjen and Chen can be constructed by building a topological model inside the usual realizability model for set theory, V(K_1). Instead of working in V(K_1) directly, we identify the axioms needed to build the topological model: Markov's principle and a special case of independence of premises. This allows one to easily generalise the construction to several variants of Lifschitz realizability. Finally we use this to show several consistency and "existence property" results for IZF and CZF with LLPO or the weaker variants LLPO_n studied by Richman. (jww Michael Rathjen)