Swansea University
Computer Science

Seminar series on categorical logic

Next meeting

The seminar is over!

Categorical logic is a generalisation of Tarski-style semantics of logical formulas to categories other than Set. The idea is to identify the structure needed in a category in order to interpret different fragments of First-order logic in them. Completeness can then be elegantly proved by constructing a syntactic category and observing that it has the required structure.

The aim of the seminar is also to get some practise and “working knowledge” of standard categorical concepts, which should be of benefit to most theoretical computer scientists.

Time and place

Fridays 15.00 - 16.30 in the Robert Recorde room, Faraday, 2nd floor.


It will be helpful to know some basic category theory and model theory. Useful categorical concepts are e.g. categories, functors, natural transformations, adjoints, equalisers, pullbacks, presheaves and the Yoneda Lemma. From logic, it helps to know terms, formulas, theories, models, soundness and completeness.

Do not worry if you do not recognise all these terms; we aim to keep the seminar friendly.


We will follow the lecture notes by Steve Awodey and Andrej Bauer. Feel free to incorporate material from other sources as well!

Background material
Supplemental reading

Time plan

5/10 0. Overview. Planning. Fred
14/10 0½. Informal review of prerequisites. [Appendix A and B] Phil
19/10 1. Algebraic theories. Models in finite product categories. [1.1.1] Andy L
26/10 2. First order theories. Predicates as subobjects. Substitution. [2.1 – 2.2] Jens
2/11 2½. Exercises on algebraic theories, subobjects and pullbacks.
9/11 3. Cartesian logic. Soundness. [2.3] Matt
16/11 3½. Exercises on cartesian categories.
23/11 4. Quantifiers as adjoints. The Beck-Chevalley condition. [2.5.1] Fred
2/12 4½. Exercises on adjoints and quantifiers.
7/12 5. Universal quantifiers in locally cartesian closed categories. [2.5.2] Martin
14/12 5½. Exercises on locally cartesian closed categories.
– Christmas –
25/1 6. Implication from universal quantification. [2.5.3] Phil
3/2 7. Regular logic. Soundness. [2.6.1 – 2.6.3] Caroline
10/2 7½. Exercises on regular categories.
21/2 8. Coherent logic. Soundness. [other sources] Fred
24/2 8½. Exercises on coherent categories.
2/3 9. The classifying category of a theory. Completeness. [1.1.2 – 1.1.4, 2.6.4] Martin
9/3 9½. Exercises on the classifying theory.
19/3 10. Topos theory. [other sources] Oliver
23/3 10½. Topos theory (cont.). Oliver
30/3 11. Any topos is a Heyting category. [other sources] Jens

This information also exists in pdf form.

Fredrik Nordvall Forsberg. Last modified: Wed 27 Feb 12:17:56 UTC 2013.