Seminario: Lifschitz Realizability as a Topological Construction

Mercoledì 23 Settembre 2015, ore 16:00 - Aula 2AB45 - Andrew Swan



Mercoledì 23 Settembre 2015 alle ore 16:00 in Aula 2AB45, Andrew Swan (University of Leeds) terrà un seminario dal titolo "Lifschitz Realizability as a Topological Construction".

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 remarkable consistency and "existence property" results for IZF and CZF with LLPO or the weaker variant LLPO_n studied by Richman.

(jww Michael Rathjen)