Topos Semantics for First- and Higher-Order Modal Logic
Modal logic is a logical study of various ways in which sentences can be true. In particular, in close connection to intuitionistic logic, the modal logic of topology provides a study of "provably (true)", "constructively", "verifiably", "observably", etc. Though it is usually studied in a setting of propositional logic, the geometric concept of sheaf over a topological space extends the setting naturally to the first order. In this talk I push ahead with this extension, by reformulating the framework in a more topos-theoretic fashion and by internalizing the semantics into the topos of sheaves (and, in fact, in any topos). This facilitates a semantics for higher-order modal logic, in a way integrating higher-order type theory with expressions for observability.