Elementary topoi

TL;DR

This paper introduces elementary topoi as a categorical framework that generalizes set theory and logic, explaining their properties and how they enable formalization of logical systems.

Contribution

It provides an exposition of topoi, detailing their foundational role in formalizing logic and set theory beyond the category of sets.

Findings

Topoi generalize set theory and logic in category theory.

They provide a framework to formalize first-order logic within categories.

The paper explains the essential features of topoi that enable logical formalization.

Abstract

As the prototypical category, $\mathbf{Set}$ has many properties which make it special amongst categories. From the point of view of mathematical logic, one such property is that $\mathbf{Set}$ has enough structure to "properly" formalise logic. However, we could ask what it might mean to formalise logic in another category $\mathbf{C}$. The notion of an (elementary) topos distills the essential features of $\mathbf{Set}$ which allow us to do this. This expository report defines topoi, and describes the development of first-order logic and set theory within a topos.