Models of Intuitionistic Set Theory in Subtoposes of Nested Realizability Toposes

2014/07/08 by Samuele Maschio, Maschio, Samuele, Thomas Streicher +1
Mathematics · #18B25 #Category Theory (math.CT) #FOS: Mathematics #math.CT #msc:18B25

paper · pdf · doi:10.48550/arxiv.1407.2287

arxiv created 2014/07/08 · arxiv updated 2014/07/10

Abstract

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

Related

• Implicative models of intuitionistic set theory
• Extensional realizability for intuitionistic set theory
• Aspects of Predicative Algebraic Set Theory II: Realizability
• The independence of premise rule in intuitionistic set theories
• An Intuitionistic Set-theoretical Model of the Extended Calculus of Constructions