# 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.

### Prerequisites

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.

### Literature

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

##### Background material

- Awodey, S.:
*Category Theory*. Oxford University Press, 2010. - Mac Lane, S.:
*Categories for the Working Mathematician*. Springer, 1998. - Adámek J., Herrlich H. and Strecker G.:
*Abstract and Concrete Categories – The Joy of Cats*. Reprints in Theory and Applications of Categories, 2006. Available here. - van Dalen, D.:
*Logic and Structure*, Springer, 2004.

##### Supplemental reading

- Pitts, A.:
*Categorical Logic*. Chapter 2 of Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, Oxford University Press, 2000. (Earlier version here.) - Butz, C.:
*Regular Categories and Regular Logic*. BRICS Lecture Series LS-98-2, 1998. Available here. - Lambek, J. and Scott, P.:
*Introduction to Higher-Order Categorical Logic*. Cambridge University Press, 1986. - Mac Lane, S. and Moerdijk, I.:
*Sheaves in Geometry and Logic: A First Introduction to Topos Theory*. Springer, 1992. - Johnstone, P.:
*Sketches of an Elephant*. Oxford University Press, 2002. - Crole, R.:
*Categories for Types*. Cambridge University Press, 1993. - Jacobs, B.:
*Categorical Logic and Type Theory*. Elsevier, 2001. - Palmgren, E.:
*First-order many sorted logic and its interpretation in categories*, Lecture Notes, 2006. Available here. - Goldblatt, R.:
*Topoi : The Categorial Analysis of Logic*, Dover Publications, 2006.

[Warning: considered historically inaccurate, see McLarty, C:*The Uses and Abuses of the History of Topos Theory*, Brit. J. Phil. Sci 41, 1990. (Available here.)]

### 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.