Lifschitz Realizability as a Topological Construction

TL;DR

This paper introduces topological models of Lifschitz realizability within realizability models for CZF, leading to new insights into the consistency and properties of constructive set theories with LLPO variants.

Contribution

It develops novel topological constructions of Lifschitz realizability for CZF, enabling analysis of metamathematical properties and consistency results.

Findings

Consistency with unique Church's thesis

Consistency with Brouwerian principles

Variants of the numerical existence property

Abstract

We develop a number of variants of Lifschitz realizability for CZF by building topological models internally in certain realizability models. We use this to show some interesting metamathematical results about constructive set theory with variants of LLPO including consistency with unique Church's thesis, consistency with some Brouwerian principles and variants of the numerical existence property.