Implicative models of set theory
Logic in Computer Science
2024-02-14 v2 Logic
Abstract
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.
Cite
@article{arxiv.2310.10576,
title = {Implicative models of set theory},
author = {Samuele Maschio and Alexandre Miquel},
journal= {arXiv preprint arXiv:2310.10576},
year = {2024}
}
Comments
arXiv admin note: substantial text overlap with arXiv:2301.11740