Toposes from Forcing for Intuitionistic ZF with Atoms

TL;DR

This paper develops a forcing model for IZFA set theory using Grothendieck topologies, showing that the topos of sheaves on any site corresponds to the category of sets within this model, bridging forcing and topos theory.

Contribution

It introduces a novel forcing construction for IZFA set theory applicable to any Grothendieck topology, establishing an equivalence with sheaf toposes.

Findings

Forcing models for IZFA are constructed for arbitrary Grothendieck topologies.

The topos of sheaves on any site is equivalent to the category of sets in the forcing model.

This unifies forcing and topos theory in the context of intuitionistic set theory.

Abstract

We introduce the forcing model of IZFA (Intuitionistic Zermelo-Fraenkel set theory with Atoms) for every Grothendieck topology and prove that the topos of sheaves on every site is equivalent to the category of 'sets in this forcing model'.