Models of Intuitionistic Set Theory in Subtoposes of Nested Realizability Toposes

Abstract

With every pca \(\mathcal{A}\) and subpca \(\mathcal{A}_\#\) we associate the nested realizability topos \(\mathsf{RT}(\mathcal{A},\mathcal{A}_\#)\) within which we identify a class of small maps \(\mathcal{S}\) giving rise to a model of intuitionistic set theory within \(\mathsf{RT}(\mathcal{A},\mathcal{A}_\#)\). For every subtopos \(\mathcal{E}\) of such a nested realizability topos we construct an induced class \(\mathcal{S_E}\) of small maps in \(\mathcal{E}\) giving rise to a model of intuitionistic set theory within \(\mathcal{E}\). This covers relative realizability toposes, modified relative realizability toposes, the modified realizability topos and van den Berg's recent Herbrand topos.