Universe enlargement and modal logic

Question

In model theory and category theory, we often need to "enlarge" our universe (whatever that means) so that our proper classes become "small" and we can thereby manipulate them in more sophisticated ways. I imagine that modal logic provides an elegant account of this kind of thing. Has any work been done to this end?

Answer 1

The modal logic of forcing (J. D. Hamkins and B. Löwe) may be the right place to look.

Answer 2

As Adam mentions, my paper with Benedikt Löwe on the The modal logic of forcing is concerned with the modality $\square\varphi$, which means that $\varphi$ holds in all forcing extensions, and the corresponding modality $\Diamond\varphi$, which means that $\varphi$ holds in some forcing extension. It is remarkable, in my opinion, that these set-theoretic modalities are actually expressible in the usual language of set theory. The result is that what might be considered philosophical questions about the nature of the set-theoretic universe become purely mathematical or set-theoretic questions that we can answer purely mathematically.

In particular, the forcing modality language allows us to express a number of quite interesting set-theoretic forcing axioms or principles. The Maximality principle, for example, is the assertion $$\Diamond\square\varphi\to\square\varphi$$ that every statement $\varphi$ that could be forced in such a way that it remains true in all further forcing extensions is already true and true in all forcing extensions. One can investigate this principle when restricting to various forcing classes, and for example The necessary maximality principle for c.c.c. forcing is equiconsistent with a weakly compact cardinal.

Meanwhile, there are other natural modalities to consider in set theory. Solovay, for example, investigated both the modality "true in all transitive models of ZF" and the modality "true in $V_\kappa$ for unboundedly many inaccessible cardinals $\kappa$," and that work was extended by Enayat and Togha.

In terms of category theory, which you mention, I would think that the Solovay interpretation has a lot of affinity with the category theoretic use of the Grothendieck universe axiom.