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:
  1. Basic notions of category theory
  2. Syntax of logics (signatures, terms, formulas, sequents, and theories)
  3. Categorical semantics (subobjects, structures, and term evaluation)
  4. Satisfaction of first-order formulas in Heyting categories
  5. Lawvere's hyperdoctrines
  6. Elementary toposes and their logical interpretation
  7. Kripke-Joyal semantics
  8. Interpretation of higher-order logic in elementary toposes
  9. Geometric logic and geometric categories
  10. Grothendieck toposes
  11. Inference systems (rules, correctness, and completeness)
  12. Syntactic categories and universal models
  13. Representable functors and T-Mod
  14. 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