Categorical Logic

Course description

Categorical logic studies the interpretation of logical theories in categories and the interplay between formal theories and categories. As such, it is abstract algebraic logic extended to predicate logic and beyond. Categorical semantics provides a wide variety of models for various formal languages and theories, including for intuitionistic first- and higher-order logic. Moreover, the categorical framework provides a rich conceptual background for constructions and perspectives that are not (always so easily) obtainable in the more classical model theoretic setting.

This course gives a first introduction to central ideas and concepts in categorical logic. We shall focus primarily on first-order logic, including intuitionistic first-order logic and fragments of first-order logic. Prerequisites will be kept to a minimum, with an initial emphasis on from-the-ground-up explanations of the categorical interpretation of the logical constants, examples of interpretations is various categories, the familiar Tarski and Kripke semantics as special cases, the models-as-functors perspective, and the construction of universal models. On this basis, we will give pointers to and discuss further topics, such as higher-order logic, forcing semantics, duality between syntax and semantics, and type theories (depending on time and interest).

Course material

• (Pre-)lecture notes: These notes give a quick summary of basic categorical notions that will be assumed known, or only mentioned very briefly, in the course. They also contain some material that is convenient to have written out in full beforehand.
• Version 1.1 (fixed typos and updated to)
• Version 1.2
• Version 1.3 (added the exercises to the end and got)
• Version 2.1
• Handouts:
• Exercises:
• Some suggestions for further reading

Course schedule

In parenthesis the sections of the prelecture notes that that part is based on, in the sense that one should really at least have had a good look at it before the lecture.

1. day
• Intro: the propositional case. (2.3)
• Categorical semantics. (3.2 and 2.2)
2. day
• Categorical semantics. (3.2 and 2.2)
• Some fragments of first-order logic. (3.1)
• Start internal languages
3. day
• Internal languages and theories continued
• Syntactic categories and generic models
• Examples of interpretations in categories---Moved to Exercises.
4. day
• Syntactic categories and generic models
• Models as functors
• An example: Kripke completeness---Moved to Exercises
5. day
• Cartesian closed categories and λ-calculus.
• Higher-order logic and toposes