A graduate course (6 course points) in mathematical logic.
Topos theory grew out of the observation that the category of sheaves over a fixed topological space forms a universe of "continuously variable sets" which obeys the laws of intuitionistic logic. These sheaf models, or Grothendieck toposes, turn out to be generalisations of Kripke and Beth models (which are fundamental for various non-classical logics) as well as Cohen's forcing models for set theory. The notion of topos was subsequently extended and given an elementary axiomatisation by Lawvere and Tierney, and shown to correspond to a certain higher order intuitionistic logic. Various logics and type theories have been given categorical characterisations, which are of importance for the mathematical foundations for programming languages. One of the most interesting aspects of toposes is that they can provide natural models of certain theories that lack classical models, viz. synthetic differential geometry.
This graduate course offers an introduction to topos theory and categorical logic. In particular the following topics will be covered: Categorical logic: relation between logics, type theories and categories. Generalised topologies, including formal topologies. Sheaves. Pretoposes and toposes. Beth-Kripke-Joyal semantics. Boolean toposes and Cohen forcing. Barr's theorem and Diaconescu covers. Geometric morphisms. Classifying toposes. Sheaf models of infinitesimal analysis.
We will assume some familiarity with basic category theory, such as is obtained in courses in domain theory or algebra. The course will be given English, in case someone requests this.
S. Mac Lane and I. Moerdijk: Sheaves in Geometry and Logic. Springer 1992.
P.T. Johnstone. Topos Theory. Academic Press 1977.
J. Lambek and P.J. Scott: An introduction to Higher Order Categorical Logic. Cambridge University Press 1986
S. Mac Lane: Categories for the Working Mathematician. Springer 1971.
A.M. Pitts. Categorical Logic. Chapter in the Handbook of Logic in Computer Science, vol. VI. Oxford University Press (to appear)