Implicative models of set theory
Samuele Maschio, Alexandre Miquel
TL;DR
The work develops implicative algebras and implicative triposes as a unified framework for forcing and realizability, then constructs implicative models of $(I)ZF$ inside a Set-based universe using a cumulative hierarchy $\mathbf{W}=W^{\mathbb{A}}_{\kappa}$ and a semantic interpretation valued in the implicative algebra. It proves the internal validity of $(I)ZF$ axioms within $\mathbf{W}$ (and $\mathbf{ZF}$ when the algebra is classical), and shows these models subsume Heyting/Boolean-valued models, Friedman/Rosolini/McCarty realizability, and Krivine’s classical realizability. The paper also connects the construction to topos theory by showing that any topos generated from a Set-based tripos hosts an internal model of $(I)ZF$ (or $ZF$ in the classical case) given a sufficiently large inaccessible cardinal, thereby providing a unified path from forcing, realizability, and topos theory to internal set theory in toposes. Overall, it offers a broad, unifying method for obtaining set-theoretic universes within toposes and clarifies the relationships among several major model-building paradigms in logic and category theory.
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.