The modal theory of the category of sets

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}$.