Implicative models of intuitionistic set theory

TL;DR

This paper demonstrates how implicative algebras can be used to construct models of intuitionistic set theory, unifying realizability and Heyting-valued models, with implications for topos theory under certain axioms.

Contribution

It introduces a new approach using implicative algebras to generate models of intuitionistic set theory, extending existing frameworks.

Findings

Models generalize realizability and Heyting-valued models

Every topos from a Set-based tripos hosts an intuitionistic set theory model under inaccessible cardinal axiom

Bridges between algebraic and categorical models of 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.