Categorical Logic — Mathematics Knowledge System

Overview

Categorical logic establishes a deep correspondence between logical systems and categorical structures. Under this correspondence, a theory (in a suitable logic) corresponds to a category, and models of the theory correspond to functors out of that category. Toposes, for instance, are categories that model intuitionistic higher-order logic. This framework unifies proof theory, model theory, and category theory, and underpins the Curry-Howard-Lambek correspondence between proofs, programs, and morphisms.

Intuition

Logic and category theory speak the same language in disguise. A type in type theory is an object in a category; a term of type A is a morphism into A; a proof of a proposition is a section of a subobject. The quantifiers 'for all' and 'there exists' are right and left adjoints to substitution (weakening). This is not mere analogy — the categorical structure literally is the logic, and theorems in one language translate directly to the other.

Formal Definition

Definition

The fundamental correspondence (Curry-Howard-Lambek) relates three structures. The key notions are: (1) a cartesian closed category (CCC) models the simply-typed lambda calculus; (2) a Heyting algebra (or more generally a Heyting category) models intuitionistic propositional logic; (3) an elementary topos models intuitionistic higher-order logic.

A \times B \text{ (product)} \leftrightarrow A \wedge B \text{ (conjunction)} \leftrightarrow A \times B \text{ (product type)}

Products correspond to conjunction and product types

curry-howard-product

B^A = [A, B] \text{ (internal hom)} \leftrightarrow A \Rightarrow B \text{ (implication)} \leftrightarrow A \to B \text{ (function type)}

Exponentials correspond to implication and function types

curry-howard-hom

\Omega = \text{subobject classifier} \leftrightarrow \text{truth values}

The subobject classifier Omega in a topos classifies subobjects, playing the role of the set of truth values

truth-values

\forall_f \dashv f^* \dashv \exists_f \quad (f^*: \mathrm{Sub}(B) \to \mathrm{Sub}(A))

Universal and existential quantification along f are the right and left adjoints to substitution f*

quantifiers-as-adjoints

Notation

Notation	Meaning
$\mathrm{Sub}(A)$	Poset of subobjects of A in a category
$\Omega$	Subobject classifier in a topos
$\mathsf{true}: 1 \to \Omega$	Universal truth arrow classifying the top subobject
$\chi_U: A \to \Omega$	Characteristic morphism of subobject U -> A
$\forall_f$	Right adjoint to f*: universal quantification along f
$\exists_f$	Left adjoint to f*: existential quantification along f
$\mathcal{L}(\mathcal{C})$	Internal language of a category C

Theorems

Theorem 1: Curry-Howard-Lambek Correspondence

There are equivalences of categories: \{\text{CCCs}\} \simeq \{\text{simply-typed lambda theories}\} \simeq \{\text{intuitionistic propositional theories}\}. Under this equivalence, objects are types/propositions, morphisms are terms/proofs, and the CCC structure encodes the type-theoretic/logical operations.

Theorem 2: Classifying Topos Theorem

For every (geometric) theory T, there exists a topos \mathcal{E}_T (the classifying topos) such that T-models in any Grothendieck topos \mathcal{E} correspond naturally to geometric morphisms \mathcal{E} \to \mathcal{E}_T.

Theorem 3: Internal Logic of a Topos

Every topos \mathcal{E} has an internal language — a dependent type theory (the Mitchell-Bénabou language) — such that a statement is internally true iff its interpretation as a morphism factors through \mathsf{true}: 1 \to \Omega. Proofs in the internal language correspond to morphisms in \mathcal{E}.

Worked Examples

In Set, Omega = {false, true} = {0, 1} (the two-element set of truth values).
$\Omega = \{\bot, \top\} = \{0, 1\}$
The truth arrow true: 1 -> Omega picks out the element top: true(*) = top.
$\mathsf{true}: * \mapsto \top$
For S \subseteq A, the characteristic function chi_S: A -> Omega is the indicator function: chi_S(a) = top if a \in S, else bot.
$\chi_S(a) = \begin{cases} \top & a \in S \\ \bot & a \notin S \end{cases}$
The pullback of true: 1 -> Omega along chi_S recovers S as a subobject of A: chi_S^{-1}(top) = S.

Answer: In Set: Omega = {0,1}, true = top. The characteristic morphism of S \subseteq A is the indicator function chi_S: A -> {0,1}. This is the universal example of a subobject classifier.

Practice Problems

Difficulty 9/10

Explain how universal quantification \forall x: A. P(x) is interpreted as a right adjoint in a categorical logic framework.

Difficulty 10/10

Prove that in a cartesian closed category, the currying bijection Hom(A x B, C) \cong Hom(A, C^B) is natural in all three variables.

Difficulty 10/10

What is the classifying topos of the theory of flat modules over a commutative ring R, and what does it classify?

Common Mistakes

Common Mistake

Thinking the Curry-Howard correspondence only applies to propositions-as-types, not to morphisms in a category.

The full Curry-Howard-Lambek correspondence is three-way: propositions = types = objects, proofs = programs = morphisms, proof normalization = program evaluation = categorical composition.

Common Mistake

Assuming all toposes satisfy classical logic.

Most naturally occurring toposes (sheaf toposes, functor categories) have intuitionistic internal logic. Classical logic requires Omega to be Boolean, which holds in Set but not in general.

Historical Background

Categorical logic originated with Lawvere's 1963 dissertation, which interpreted quantifiers as adjoint functors. Lambek and Scott extended this to a full correspondence between typed lambda calculi and cartesian closed categories (Curry-Howard-Lambek). Lawvere and Tierney's development of elementary toposes (1969-1970) showed that topos logic is a natural generalization of set-theoretic logic. The theory matured through Makkai-Reyes and Pitts, culminating in modern developments connecting homotopy type theory to infinity-toposes.

1963
Lawvere's thesis: quantifiers as adjoint functors
F. William Lawvere
1969
Lawvere-Tierney: elementary toposes as generalized universes of sets
F. William Lawvere, Myles Tierney
1980
Lambek-Scott: Cartesian closed categories and typed lambda calculus
Joachim Lambek, Phil Scott
2013
Homotopy Type Theory book connects type theory to higher toposes
Vladimir Voevodsky

Summary

Categorical logic identifies logical systems with categorical structures: CCCs with lambda calculi, Heyting categories with intuitionistic logic, elementary toposes with higher-order intuitionistic logic.
The subobject classifier Omega in a topos plays the role of the set of truth values; characteristic morphisms classify subobjects.
Quantifiers \forall and \exists are right and left adjoints to substitution (pullback along a morphism), making logic intrinsically categorical.
The classifying topos of a geometric theory T represents T-models: geometric morphisms E -> E_T correspond to T-models in E.
Classical logic corresponds to Boolean Omega; non-Boolean toposes model intuitionistic logic, showing the logical content of geometric variation.

References

BookLambek, J. & Scott, P.J. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986.
BookJohnstone, P.T. Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press, 2002.
BookAwodey, S. Category Theory. Oxford University Press, 2010.