Alex Simpson: A Tutorial on Sheaf Semantics

Abstract: Sheaf semantics provides a unifying framework for modelling intuitionistic, intermediate and classical logics. On the one hand, it seamlessly generalises several more specific forms of semantics such as the Kripke and Beth models of intuitionistic logic, as well as Cohen's forcing interpretation of classical logic (as used in his set-theoretic independence proofs). On the other, it naturally embraces some genuinely new types of model in which the underlying structure of “possible worlds” or “conditions” is given by a category rather than a partial order.

Starting with the Kripke semantics of intuitionistic logic, I shall build towards the goal of presenting and explaining sheaf semantics for logic in its general form, together with example applications.