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
Secretary: Baker 135
This course focuses on applications of category theory in logic and
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.
80-413/713 Category Theory, or equivalent.
Topics will be selected from the following
- Functorial semantics for algebraic theories
- Simple type theory and cartesian closed categories
- Dependent type theory and locally cartesian closed categories
- Functorial semantics for elementary logic
- Higher-order logic
- Basic topos theory
- Sheaf semantics
- Algebraic set theory
- Crole, R. L.: Categories for Types. Cambridge University Press,
- Lambek, J. and Scott, P.: Introduction to Higher-Order
Cambridge University Press, Cambridge, 1986.
- Mac Lane, S. and Moerdijk, I.: Sheaves in Geometry and Logic: A
to Topos Theory. Springer, 1992.
- Johnstone, P.: Sketches of an Elephant. Cambridge, forthcoming.
- Asperti, A. and Longo, G.: Categories, Types, and Structures.
- Barr, M. and Wells, C.: Categories for Computing Science, 3rd
- Borceux, F.: Handbook of Categorical Algebra (Encyclopedia of
and its Applications). Cambridge University Press, 1994.
- Freyd, P. and Scedrov, A.: Categories, Allegories.
- Makkai, M. and Reyes, G.: First-Order Categorical Logic. LNM
- Mac Lane, S.: Categories for the Working Mathematician.
(the standard reference)
- McLarty, C.: Elementary Categories, Elementary Toposes. Oxford
21, Oxford University Press, 1992.
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.
Lecture notes: Lecture notes are here.