Lecturers: Ivan Di Liberti and Lingyuan Ye.
Categorical Logic, and Functorial semantics more specifically, emerged in the 1960s as an alternative framework to capture universal algebra. The framework offers a collection of advantages, including a more flexible and modular approach to semantics, which delivers a perfect correspondence with syntax. These tools offer a more quantitative and conceptual take on completeness results and definability-type theorems.
After a brief introduction to the language of categories, we focus on universal algebra and functorial semantics. We capture the notion of algebraic theory via categories with products (Lawvere theories) and present a syntax-semantics duality between varieties and Lawvere theories. The course ends with some vistas on the theory of sketches which offers a much more general framework, covering the leap from universal algebra to infinitary first order logic.
Prerequisites: The audience is expected to be familiar and have played with the basic definitions of one of following objects: vector space, monoid, group, ring, module, set equipped with operations.
| Day 1 | Categories, functors, natural transformations. | |
|---|---|---|
| Day 2 | Adjunctions. | |
| Day 3 | Functorial semantics: from posets to Lawvere theories | meet semilattices and their semantics, Lawvere theories and natural operations |
| Day 4 | Dualities: from posets to Gabriel and Ulmer | Algebraic lattices and duality, GU duality, Varieties from Universal algebra |
| Day 5 | Sketches of a broader vision | (co)limits and sketches |