Categorical logic

Builds on

Required prerequisites, all the way down: 29

You will learn to

• Interpret the simply typed λ-calculus with products in any cartesian closed category, and show that Set is cartesian closed.
• Express ∃ and ∀ as left and right adjoints to pulling back predicates along a projection (Lawvere).
• Use Heyting algebras to model intuitionistic propositional logic, and show that P ∨ ¬P fails in some models.

Definition

• A cartesian closed category has finite products and, for every object B, a right adjoint (−)^B to the functor − × B.
• A Heyting algebra is a bounded lattice with an operation → such that c ≤ (a → b) if and only if c ∧ a ≤ b.
• For a projection π : X × Y → X, pulling back subsets π* has a left adjoint ∃_π and a right adjoint ∀_π (Lawvere).

Theorem

• Curry–Howard–Lambek: the simply typed λ-calculus with products serves as an internal language for cartesian closed categories.
• Quantifiers are adjoints to substitution.
• Intuitionistic propositional logic is sound and complete with respect to Heyting algebras.
• The open subsets of ℝ form a Heyting algebra that is not Boolean.

Common misconceptions

• Thinking categorical semantics replaces set-theoretic semantics; models in Set are one important case among many.
• Believing intuitionistic logic asserts the negation of excluded middle; it merely does not assume excluded middle, and it proves ¬¬(P ∨ ¬P).

Leads to

Optional discoveries

• Homotopy type theory Dependent type theories with identity types have models in homotopical and higher-categorical structures, which led to homotopy type theory.
• ← First-order logic
• ← Categories
• ← The λ-calculus
• ← Proof theory

Further reading

• J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic (1986)
• Steve Awodey, Category Theory (2006)