Introduction to Categorical Logic 23
Info. 14-16 lectures of 90 minutes each. Course period covers the first semester of 2023. Meeting once a week. The lectures will be delivered at the Maths department in the Mittag Leffler room, every Thursday from 13 to 15 o'clock. We start the 12th of January.
Syllabus. (1) Foundational aspects of the Yoneda Embedding. (2) Lawvere theories and Universal Algebra. (3) Sketches and Accessible Categories. (4) Hyperdoctrines. (5) Type Theories. (6) Topoi as spaces, sets and theories.
Description. Categorical logic emerged in the Category Theory community after the impulse of Bill Lawvere and succeeded in providing a crisper, sharper, and authentically foundational point of view on mathematical logic. Because of its versatility, the diversity and richness of perspectives, and the historical dilution in several communities (theoretical computer science, model theory, proof theory), its initial unity has taken off in the last years, and often students are only introduced to some aspects of this elephant. This course presents a unified point of view on the most prominent topics of Categorical Logic. It's a safari in the territories of categorical foundations of mathematics, stressing on the dissolution of their borders.
Exam rules. Two exercise sheets (). Oral interview on the contents of the course.
Oral interview! Oral exams will take place on the 5th of June in Hagagatan. We shall start early in the morning, around 10:00. An oral exam will last between 20 and 40 minutes, and I will ask questions on the entire content of the course. The precise order/schedule of the students can be agreed upon informally. If you are busy on that day or if it is inconvenient for you for any reason, we can arrange a different day. Please contact me.
Audience and Prerequisites. The course is designed for master and Ph.D. students interested in foundations of mathematics and theoretical computer science in a broad sense. A good knowledge of the language of category theory will be a prerequisite for the audience (the equivalent of the whole (!) book by Riehl in bibliography), yet we will re-discover some of its content from a more foundational perspective.
Relevance and Impact. All the topics above have proven to have horizontal applications in Logic and Theoretical computer science. Lawvere theories have offered a concrete way to handle algebraic effects since the work of Plotkin and Moggi, their relation to monads has later impacted the design of modern programming languages like Haskell after Walder. The theory of Accessible Categories is the most used framework for categorical model theory, and its versatility has found applications even in algebraic topology via algebraic factorization systems. Hyperdoctrines perfectly capture first order logic, and their idea has inspired Benabou's treatment of fibrations to later deliver Jacobs' approach to type theories et similia. Finally, topos theory has pervasive ramifications in mathematics, being motivated from plain geometry and allowing to represent geometric theories (which include coherent and thus first order logic).
Bibliography.
-
Category Theory in Context by Emily Riehl.
-
The history of categorical logic 1963–1977 by Marquis and Reyes.
-
Handbook of categorical algebra, Vol. I, II & III by Francis Borceux.
-
Categorical Foundations edited by Pedicchio and Tholen.
-
The category theoretic understanding of Universal Algebra: Lawvere Theories and Monads by Hyland and Power.
-
Locally Presentable and Accessible Categories by Rosicky and Adamek.
-
Categorical logic and type theory by Jacobs
-
Sheaves in Geometry and Logic by Mac Lane and Moerdijk.
-
Topos Theory by Peter Johnstone.
-
Further readings.
Comments. The course is very dense, and has no intention of completely cover the bibliography above. Instead, one of its main intents is to introduce the students to this corpus of knowledge, making sure that they reach a sufficient level of independence and maturity.