Categorical Logic

80-514/814

Fall 2009

Course Information

Place: BH 150
Time: M 3:30 - 5:50
Instructor: Steve Awodey
Office: Baker 152 (mail: Baker 135)
Office Hour: Monday 1-2, or by appointment
Phone: 8947
Email: awodey@andrew
Secretary: Baker 135

Overview

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 structured 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. In this connection the lambda-calculus is treated via the theory of cartesian closed categories. Similarly higher-order logic is modelled by the categorical notion of a topos. Using sheaves, topos theory also subsumes Kripke semantics for intuitionistic logic.

Prerequisites

80-413/713 Category Theory, or equivalent.

Topics will be selected from the following

Texts

Recommended Supplemental

Requirements and Evaluation

Grades will be based on occasional homework problem sets for undergraduates.
Graduate students are required to also prepare and present one lecture on a topic provided by the instructor.
Undergrads have the option of lecturing or taking a final exam.

Course materials

Lecture notes: Lecture notes are here.

Steve Awodey
awodey@cmu.edu