The modal theory of the category of sets

TL;DR

This paper classifies propositional modal validities in the category of sets based on morphism classes, size, and substitution, using a modal and quantifier elimination approach.

Contribution

It introduces a modality-and-quantifier elimination theorem that enables exact classification of modal validities for various set categories.

Findings

Finite n-element worlds realize Prepartition_n.

Surjection worlds realize Grz.3J_n at the sentential level.

Infinite categories have trivial sentential validities, with function and surjection validities matching Grz.2.

Abstract

We classify the propositional modal validities arising from the category of sets under its natural classes of morphisms. The resulting validities depend on the morphism class, the size of the world, and the permitted substitution instances. Our main technical tool is a modality-and-quantifier elimination theorem for the first-order modal language of equality, reducing formulas to finite Boolean combinations of partition conditions and exact cardinality assertions. This yields exact classifications for the main categories of sets, including the full subcategories of finite sets and of infinite sets. In particular, finite $n$-element worlds in the category of sets with parameters realize $\mathrm{Prepartition}_n$; finite $n$-element worlds in the category of sets and surjections realize $\mathrm{Grz.3J}_n$ at the sentential level; and in the infinite-only subcategories, sentential validities collapse to the trivial modal theory, while the formulaic validities for functions and surjections are exactly $\mathrm{Grz.2}$.