Categorical logic

As the name suggests, categorical logic is the study of logic using categorical methods. The subject originated with Lawvere’s PhD thesis on the functorial semantics of algebraic theories and has grown to encompass a vast array of logical systems from mathematics and computer science. In my view, categorical logic is among the most important set of ideas to emerge from category theory.

Categorical logic in general

Surveys

  • Bell, 2005: The development of categorical logic (doi, pdf)
    • Sec. 1 is a history of categorical logic
    • Sec. 2-7 exposit elements of algebraic theories, cartesian closed categories, and toposes
  • Abramsky & Tzevelekos, 2010: Introduction to categories and categorical logic (doi, arxiv)
  • de Paiva & Rodin, 2013: Elements of categorical logic: Fifty years later (doi, pdf)
    • Short introduction to a special issue on categorical logic
    • Distinguishes categorical model theory, based on functorial semantics, from categorical proof theory, based on the Curry-Howard-Lambek correspondence between types and terms, propositions and proofs, and objects and morphisms

Books and notes

  • Awodey & Bauer, 2019, lecture notes: Introduction to categorical logic (GitHub )
    • An excellent place to start, covering algebraic theories and aspects of first-order logic, particularly regular logic
  • Shulman, 2016, lecture notes: Categorical logic from a categorical point of view (GitHub , pdf)
    • Emphasizes multicategories as intermediate between type theories and monoidal categories/cartesian categories

Unifying frameworks

Doctrines are the oldest principle for organizing systems of categorical logic, even if the term “doctrine” does not have a fixed technical meaning. John Baez has a brief introduction at the nCat Cafe .

  • Kock & Reyes, 1977: Doctrines in categorical logic (doi)
  • Kelly & Street, 1974: Review of the elements of 2-categories, Sec 3: Monads in a 2-category (doi, nCat Cafe )
  • Paugam, 2014: Towards the Mathematics of QFT, Sec 2.1: Higher categories, doctrines, and theories
  • Dagnino & Rosolini, 2021: Doctrines, modalities and comonads (arxiv)

Other frameworks:

  • Makkai, 1997: Generalized sketches as a framework for completeness theorems (parts I, II, III)
    • Proposes a framework, generalizing Ehresmann’s sketches, to specify categorical doctrines, especially (but not exclusively) those based on universal properties
    • Has a model theory and a proof theory, both categorical in nature
  • Fujii, 2019: A unified framework for notions of algebraic theory (pdf, arxiv)
    • Encompasses not just algebraic theories, in the strict sense of the term, but PROs, PROPs, symmetric and nonsymmetric operads, and so on

Logical systems

Algebraic theories

See dedicated page on algebraic theories.

Regular logic

  • Awodey & Bauer, 2019, lecture notes: Introduction to categorical logic, Sec 2.5: Regular logic (pdf)
  • van Oosten, 1995: Basic category theory, Sec 4.2: The logic of regular categories (pdf)
  • Butz, 1998: Regular categories and regular logic (pdf)
  • Johnstone, 2002: Sketches of an Elephant, Sec A1.3: Regular categories & Sec D1.1: First-order languages

Regular categories, from the viewpoint of categorical algebra:

  • Gran, 2021: An introduction to regular categories (doi, arxiv)
  • Borceux, 1994: Handbook of Categorical Algebra, Vol 2, Ch. 2: Regular categories

Coherent logic

  • Reyes, 1997: Sheaves and concepts: a model-theoretic interpretation of Grothendieck topoi, Ch. II: Coherent logic (pdf)
  • Johnstone, 2002: Sketches of an Elephant, Sec A1.4: Coherent categories & Sec D1.1: First-order languages
  • Bezem, 2005: On the undecidability of coherent logic (doi)

Applications of coherent logic

  • Bezem & Coquand, 2005: Automating coherent logic (doi)
    • Stojanovic et al, 2010: A coherent logic based geometry theorem prover capable of producing formal and readable proofs (doi, swMath )
    • Stojanovic et al, 2014: A vernacular for coherent logic (doi, arxiv)
  • Avigad et al, 2009: A formal system for Euclid’s Elements (doi, arxiv)
  • Ganesalingam & Gowers, 2013: A fully automatic problem solver with human-style output (doi, arxiv, blog posts by Tim Gowers and Dustin Mixon )

Toposes

See dedicated page on topos theory.