Categorical Logic

80-514/814

Spring 2024

Course information

• Place: BH 150
• Time: TR 3:30-4:50
• Instructor: Steve Awodey
• Office: Baker 135F
• Office Hour: Tuesday 2-3, or by appointment
• Email: awodey@andrew

Overview

This course focuses on applications of category theory to logic. A leading idea is functorial semantics, according to which a model of a logical theory is a (set-valued) functor on a structured category representing the theory.
This introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics.
The lambda-calculus, for example, is treated via cartesian closed categories.
Equational theories are represented by categories with finite products, following Lawvere. Hyperdoctrines are used to model first- and higher-order logics, leading to the categorical notion of a topos. Using sheaves, topos theory also subsumes Kripke semantics for modal and intuitionistic logics. And locally cartesian closed categories provide semantics for dependent type theories. Time permitting, we may also consider Martin-L"of type theory and its recent extension to Homotopy type theory.

Prerequisites

80-413/713 Category Theory or equivalent.

Topics

• Functorial semantics for algebraic theories
• Functorial semantics for propositional and first-order logic
• Simple type theory and cartesian closed categories
• Dependent type theory and locally cartesian closed categories
• Higher-order logic and basic topos theory
• Sheaf semantics and Grothendieck toposes
• Homotopy type theory

Texts

Recommended

Course notes will be provided. The following are recommended for further reading.

• Steve Awodey, Category Theory, 2nd edition, Oxford University Press, 2010.
• Crole, R. L.: Categories for Types. Cambridge University Press, Cambridge, 1993.
• Lambek, J. and Scott, P.: Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge, 1986.
• Mac Lane, S. and Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1992.
• Steve Awodey, Fischbachau Notes.

Supplemental

• Asperti, A. and Longo, G.: Categories, Types, and Structures. MIT Press, 1991.
• Barr, M. and Wells, C.: Categories for Computing Science, 3rd edition.
• Borceux, F.: Handbook of Categorical Algebra (Encyclopedia of Mathematics and its Applications). Cambridge University Press, 1994.
• Freyd, P. and Scedrov, A.: Categories, Allegories. North-Holland, 1995.
• Johnstone, P.: Sketches of an Elephant. Cambridge University Press.
• Makkai, M. and Reyes, G.: First-Order Categorical Logic. LNM 611, Springer, 1977.
• Mac Lane, S.: Categories for the Working Mathematician. Springer, 1971. (the standard reference)
• McLarty, C.: Elementary Categories, Elementary Toposes. Oxford Logic Guides 21, Oxford University Press, 1992.
• Rijke, E.: Introduction to Homotopy Type Theory, Cambridge University Press (forthcoming).
• The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013.

Requirements

Grades will be based on 4 problem sets and, for graduate students, a presentation in class with a brief written report.

Course materials

• Course outline
• Lecture notes
• Problem sets

Updates

Watch this space for news and information!

• We're also using the course zulip for announcements and discussion.
• Have a look at the first set of lecture notes for a brief introduction and the review of basic category theory.
• Also check out the course notes from Fischbachau for a bigger picture.
• The lecture notes for (the first half of) Chapter 1 on Algebraic Theories are available.
• A problem set for Chapter 1 on Algebraic Theories is available.
• The lecture notes for Chapter 1 on Algebraic Theories are now complete.
• Some possible grad student topics are being compiled here.
• The first problem set is due on Tuesday 13 February, in class.
• A problem set for Chapter 2 on Propositional Logic is available.
• The notes on propositional logic are now complete.
• The second problem set is due in class on Tuesday 12 March.
• The first section of the notes on first-order logic are now online.
• The third problem set is due in class on Tuesday 9 April.
• The notes on first-order logic are now complete.
• Graduate student lectures will be in the last week of the semester, April 23 and 25.
• The notes on first-order logic now include a final section on hyperdoctrines.
• The first half of the notes on simple type theory are now online.
• The notes on type theory, including a section on dependent types, are now complete and available online.
• The fourth and final problem set for undergraduates is now online.

---

Steve Awodey
awodey@cmu.edu