arXiv · 2301.11740
Implicative models of intuitionistic set theory
Abstract
In this paper we will show that using implicative algebras one can produce models of intuitionistic set theory generalizing both realizability and Heyting-valued models. This has as consequence that if one assumes the inaccessible cardinal axiom, then every topos which is obtained from a Set-based tripos as the result of the tripos-to-topos construction hosts a model of intuitionistic set theory.
Explore related subjects
Keep this discovery
Samuele Maschio. 2023-01-27. Implicative models of intuitionistic set theory. https://arxiv.org/abs/2301.11740
Cite the original work for its findings. Save a collection to share your selection of sources.