Extensional realizability for intuitionistic set theory

TL;DR

This paper develops an extensional realizability framework for set theories, creating models that validate the axiom of choice and provide semantics for constructive and intuitionistic set theories.

Contribution

It introduces a new layer of extensionality in generic realizability, enabling the construction of models validating choice and other principles for various set theories.

Findings

Constructs realizability universes validating ${ m AC}_{ m FT}$

Provides models for $ extsf{CZF}$ and $ extsf{IZF}$

Allows addition of large set axioms and principles

Abstract

In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring that realizers ought to act extensionally on realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in which the axiom of choice in all finite types ${\sf AC}_{{\sf FT}}$ is realized, where $A$ stands for an arbitrary partial combinatory algebra. This construction furnishes 'inner models' of many set theories that additionally validate ${\sf AC}_{{\sf FT}}$, in particular it provides a self-validating semantics for $\sf CZF$ (Constructive Zermelo-Fraenkel set theory) and $\sf IZF$ (Intuitionistic Zermelo-Fraenkel set theory). One can also add large set axioms and many other principles.