Logic, categories and topos : from category theory to categorical
logic
Mathematical logic, originally formulated within the framework of set
theory, was later extended to category theory. Inspired by
Grothendieck's work on toposes in the late 1950s and their structural
similarities to sets, logicians -- led by Lawvere -- developed categorical
semantics for first-order logic and its fragments, including
higher-order logic and geometric logic. This development also led to a
finitary axiomatization of elementary toposes, providing a categorical
foundation for logic.
This series of seminars will cover the following topics:
- Basic notions of category theory
- Syntax of logics (signatures, terms, formulas, sequents, and theories)
- Categorical semantics (subobjects, structures, and term evaluation)
- Satisfaction of first-order formulas in Heyting categories
- Lawvere's hyperdoctrines
- Elementary toposes and their logical interpretation
- Kripke-Joyal semantics
- Interpretation of higher-order logic in elementary toposes
- Geometric logic and geometric categories
- Grothendieck toposes
- Inference systems (rules, correctness, and completeness)
- Syntactic categories and universal models
- Representable functors and T-Mod
- Classifying toposes
All this aims to provide a comprehensive introduction to the logical
foundations of topos theory, bridging category theory with formal
logic and demonstrating its unifying power across mathematical
disciplines.
Marc Aiguier
Last modified: Tue Mar 18 2025