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.