Norihiro Yamada (CMUC) will be teaching an informal course on Categorical Logic this semester.
The course will last 15 hours in total, 1.5 hours per lecture (40 + 40 = 80 min, with a 10 min break between the two parts).

The aim of the course is to provide an introduction and an overview of categorical logic, i.e., the categorical study of mathematical logic. (N.B. Traditionally, categorical logic is concerned with proof theory and model theory, but it certainly extends to set theory and computability theory though the latter two are rather advanced and beyond the scope of the course.)
To this end, the course focuses on basic concepts and main ideas of the field (as opposed to an encyclopedic study).
The main messages of the course include:
- Categorical logic and type theory constitute "abstract algebra of proofs," and this algebraic runaissance corresponds to the shift from classical to constructive mathematics (where this algebraic perspective explains why constructive mathematics is interesting not only for logicians and computability theorists but also for other pure mathematicians, and applications of constructive mathematics attract computer scientists too though they are not our/my focus),
- Categories and types are essentially the same thing, and they are quite useful to each other, and
- Categorical logic offers a categorical/constructive generalisation of topos theory.
After the course, the audiences will be ready for more advanced topics such as categorical linear/classical logic, constructive topology, homotopy type theory, realisability topoi and game semantics.
The course outline and references are listed below.

Where: Room 5.5 (CMUC)
When: Tuesdays 15:00-16:30 (except when there is a seminar session of the Algebra, Logic and Topology research group).
First session: 25 February 2025.

Feel free to attend.


Table of contents:
1. Propositional logic (2.5 hours)
2. Simple type theory (2.5 hours)
3. Predicate logic (2.5 hours)
4. Dependent type theory (4.5 hours)
5. Elementary and predicative topoi (3 hours)

References:
1. Lambek, J., & Scott, P. J. (1988). Introduction to higher-order categorical logic (Vol. 7). Cambridge University Press.
2. Jacobs, B. (1999). Categorical logic and type theory. Elsevier.
3. Pitts, A. M. (2001). Categorical logic. Handbook of logic in computer science, 5, 39-128.
(1 is a classic standard textbook, while 2 is a more recent, encyclopedic one. 3 is a more gentle, concise monograph. The course will be based on 3 yet with some contents incorporated from 1 and 2.)