Categorical logic

Online resources:

Literature

General

  • Awodey, 2009, lecture notes: Introduction to categorical logic (GitHub )
  • Shulman, 2016, lecture notes: Categorical logic from a categorical point of view (pdf)
  • Abramsky & Tzevelekos, 2010: Introduction to categories and categorical logic (doi, arxiv)
  • Bell, unpublished: The development of categorical logic (pdf)
    • Sec. 1 is a history of categorical logic
    • Sec. 2-7 exposit elements of algebraic theories, cartesian closed categories, and toposes

Algebraic theories

See dedicated page on algebraic theories.

Regular logic

  • Awodey, 2009, lecture notes: Introduction to categorical logic, Sec 2.5: Regular logic (pdf)
    • Very readable; a nice introduction to categorical logic
  • 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, 2020, lecture notes: An introduction to regular categories (arxiv)
  • Borceaux, 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

Books on topos theory, in roughly increasing order of difficulty:

  • Lawvere & Schanuel, 2009: Conceptual mathematics, 2nd ed. (doi)
    • Elementary introduction to the topos of sets
  • Reyes, Reyes, Zolfaghari, 2004: Generic figures and their glueings: A constructive approach to functor categories (online , pdf)
    • A nice book on “combinatorial toposes”, such as the topos of graphs
    • Main examples also appear in videos by MathProofsable
    • Sec 9.1 has interesting interpretation of the two negation operations in categories of presheaves: Reyes et al, 1994: The non-boolean logic of natural language negation (doi)
  • Goldblatt, 1984: Topoi: The categorical analysis of logic (online )
    • Level similar to Reyes et al, but focus on logic, not geometry
  • Mac Lane & Moerdijk, 1992: Sheaves in geometry and logic: A first introduction to topos theory (doi, nLab )
  • Johnstone, 2002: Sketches of an Elephant: A topos theory compendium (nLab )
    • The bible of topos theory
    • In three volumes, two of which are published (~1200 pages)
    • Sequel to Johnstone, 1977: Topos theory (nLab )