Categorical Logic — 80-413/713

Categorical Logic

80-514-814 — Spring 2017

Meeting place and time: Baker Hall 150 — MW 9:00AM–10:20AM
Instructor: Jonas Frey (jonasf[at]andrew.cmu.edu)
Office: Baker Hall 152
Office Hours: Tuesday 10:30-12:00, or by appointment

Announcements

Course Description

This course focuses on applications of category theory in logic and computer science. A leading idea is functorial semantics, according to which a model of a logical theory is a set-valued functor on a category determined by the theory. This gives rise to a syntax-invariant notion of a theory and introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics. Such categorical models occur, for example, in denotational semantics. e.g. treating the ambda-calculus via the theory of cartesian closed categories. Higher-order logic is treated categorically by the theory of topoi. In particular we will cover the notion of realizability topos, which is a category theoretic incarnation of the realizability technique from proof theory. A prerequesite for this course if familiarity with basic category theory (as treated e.g. in Steve Awodeys Category Theory textbook), but depending on demand the course can start with a quick refresher of the central concepts.

Literature, resources

  • Steve Awodey, Category Theory, 2nd edition, Oxford University Press, 2010.

    This book contains the prerequesites for the course. You should already be familiar with most of the basic concepts introduced in here.

  • Saunders Mac Lane, Categories for the Working Mathematician, 2nd edition, Springer, 1998.

    Although the notation is a bit old-fashoined at times, this book remains the standard reference for category theory in general.

  • Saunders Mac Lane and Ieke Moerdijk, Sheaves in Geometry and Logic, Springer, 1994.

    An introduction to sheaves and toposes presupposing a good deal of prior knowledge of category theory.

  • Peter Johnstone, Sketches of an Elephant: A topos theory compendium (2 volumes).

    The standard reference on topos theory, containing a lot of categorical logic in Part D (warning: probably hard to read). Part D1 contains a thorough and systematic treatment of first order logic, which I'm basing the treatment in the course on.

  • Francis Borceux, Handbook of categorical algebra (3 volumes) .

    Contains a lot of stuff and is fairly detailed, volume 2 contains a chapter on algebraic theories.

  • Jiří, Adámek, and Jiří Rosicky, Locally presentable and accessible categories.

    Contains material on algebraic theories and generalizations like “quasi-algebraic theories” and “essentially algebraic theories” (a quasi-algebraic theory is a Horn theory whose axioms are sequents of equations, and “essentially algebraic” is a notion that is somewhere between “Horn” and “regular”, but there is no easy correspondence to a fragment of first order logic. Essentially algebraic theories are also known as “cartesian” or “finite-limit” theories).

  • To be extended

Grading

    50% homework (probably around five exercise sheets in total), 50% in class presentation accompanied by short report.