80-514 Categorical Logic

9 units, Carnegie Mellon University

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. Geometric logic is treated categorically by the theory of Grothendieck topoi. We shall see how this idea connects logic with topology: the models of a theory form a sort of generalized space. A prerequisite for this course is familiarity with basic category theory (as treated in the course 80-413/713).

Prerequisites: 80-413 (min C)

Offered: Spring 2027, Spring 2026

Courseweave needs JavaScript to show sections, workloads and planning tools.