In this paper we show that using implicative algebras one can produce models of set theory generalizing Heyting/Boolean-valued models and realizability models of (I)ZF, both in intuitionistic and classical logic. This has as consequence that any topos which is obtained from a Set-based tripos as the result of the tripos-to-topos construction hosts a model of intuitionistic or classical set theory, provided a large enough strongly inaccessible cardinal exists.
翻译:本文证明,利用蕴涵代数可以构建集合论的模型,这些模型统一推广了直觉主义与经典逻辑中(I)ZF的Heyting/布尔值模型和可实现性模型。由此得出推论:只要存在足够大的强不可达基数,任何通过tripos到topos构造从基于集合的tripos得到的topos,都能承载直觉主义或经典集合论的模型。