Categorical Logic
Origin. F. William Lawvere pioneered categorical logic (1960s), showing logical systems correspond to categorical structures. The topos concept (Grothendieck for algebraic geometry, Lawvere-Tierney for logic) provides a universe for mathematics beyond sets. Unifies logic, type theory, and geometry. Foundational for Homotopy Type Theory.
Models. Logic formulated inside category theory. Propositions as objects, proofs as morphisms, connectives as universal constructions. Different logics arise from different categorical structures: cartesian closed categories for lambda calculus, toposes for intuitionistic higher-order logic, *-autonomous categories for linear logic.
Formalism.
Categories as logic:
| Logical Concept | Categorical Structure |
|---|---|
| Proposition | Object |
| Proof A → B | Morphism A → B |
| True (⊤) | Terminal object 1 |
| False (⊥) | Initial object 0 |
| A ∧ B | Product A × B |
| A ∨ B | Coproduct A + B |
| A → B | Exponential Bᴬ |
| ∀x:A.P(x) | Right adjoint to pullback |
| ∃x:A.P(x) | Left adjoint to pullback |
Cartesian closed categories (CCC): Products and exponentials. Model simply typed lambda calculus.
- Terminal: 1
- Products: A × B with projections π₁, π₂
- Exponentials: Bᴬ with eval : Bᴬ × A → B and currying
Toposes: CCC plus:
- Subobject classifier Ω: truth values are morphisms to Ω
- Power objects: ΩA represents subobjects of A Models intuitionistic higher-order logic. Every topos has internal logic.
Internal language: Any topos has an internal type theory. Interpret types as objects, terms as morphisms, propositions as subobjects. Reasoning internally = reasoning about all toposes uniformly.
Examples:
- Set (category of sets): classical logic
- Sh(X) (sheaves on space X): intuitionistic logic, continuity
- G-Set (sets with group action): equivariant logic
- Eff (effective topos): realizability, computable functions
Functorial semantics: A theory T (signature + axioms) has a classifying category C[T]. Models of T in category E = functors C[T] → E preserving structure.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| × | U+00D7 | Product | Categorical product, interpreting ∧ |
| → | U+2192 | Morphism / Exponential | Arrow or function space |
| ∧ | U+2227 | Conjunction | Interpreted by the product |
| ∨ | U+2228 | Disjunction | Interpreted by the coproduct |
| ⊤ | U+22A4 | Verum | Interpreted by the terminal object 1 |
| ⊥ | U+22A5 | Falsum | Interpreted by the initial object 0 |
| ∀ | U+2200 | Universal quantifier | Right adjoint to pullback along projection |
| ∃ | U+2203 | Existential quantifier | Left adjoint to pullback along projection |
| Ω | U+03A9 | Omega / Subobject classifier | Object of truth values |
| π | U+03C0 | Pi / Projection | Product projections π₁, π₂ |
| ∘ | U+2218 | Composition | Morphism composition |
| ≅ | U+2245 | Isomorphism | Equivalent objects |
| ⊣ | U+22A3 | Adjunction | Adjoint functors |
| ᴬ | U+1D2C | Modifier letter capital A | Exponent in the exponential Bᴬ |
| β | U+03B2 | Beta | Beta-conversion, equated with composition in the CCC |
| η | U+03B7 | Eta | Eta-conversion, equated with uniqueness of currying |
| + | — | Coproduct | Categorical sum |
| 1 | — | Terminal | True / Unit |
| 0 | — | Initial | False / Empty |
| Bᴬ | — | Exponential | Internal hom, interpreting implication |
| Hom | — | Hom-set | Morphisms between two objects |
| C[T] | — | Classifying category | Syntactic category of a theory T |
| Sh(X) | — | Sheaf topos | Sheaves on a space, an intuitionistic model |
Metatheory. The subject is a sequence of internal-language theorems, each an equivalence between a class of theories and a class of categories. Lawvere, "Adjointness in Foundations" (1969), identified quantifiers as adjoints to substitution and equality as left adjoint to the diagonal, subject to the Beck–Chevalley condition. Lambek (1980) and Lambek–Scott (1986) proved that simply typed lambda theories and cartesian closed categories are equivalent as categories, so the free CCC on a set of base types is the term model modulo βη; Lambek–Scott likewise made intuitionistic higher-order type theories equivalent to elementary toposes. Seely (1989) matched intuitionistic linear logic with symmetric monoidal closed categories and classical linear logic with *-autonomous categories. Soundness and completeness follow in each case from the syntactic category: a theory is consistent iff its classifying category is non-degenerate, and every geometric theory has a classifying topos with a generic model (Makkai and Reyes, 1977). Friedman (1975) proved that the full type hierarchy over an infinite set is complete for βη-equality, while Statman (1979) showed deciding that equality is not elementary recursive, so a complete semantics need not give feasible decision procedures.
Applies to. Foundations of mathematics (topos as alternative to set theory). Programming language semantics. Homotopy Type Theory (∞-toposes). Synthetic differential geometry. Quantum logic. Database theory (presheaves as data migration). Sheaves in algebraic geometry and topology.
Limitations. The internal-language correspondences are only as strict as the syntax, and syntax is stricter than categories: substitution composes on the nose while pullback is functorial only up to canonical isomorphism, so the naive interpretation of dependent type theory in a locally cartesian closed category is not well defined. Curien (1993) and Hofmann (1994) resolved this by strictification, but the coherence problem is real and recurs for every structure with a substitution calculus. Categorical semantics is intuitionistic by default: subobject lattices are Heyting, not Boolean, and by Diaconescu's theorem the internal axiom of choice forces Booleanness, so classical reasoning is a restriction rather than an addition. Completeness with respect to a class of categories does not deliver full abstraction or full completeness — models routinely contain morphisms that are not denotations of any term, which is why the full abstraction problem for PCF needed game semantics rather than a CCC. Classifying constructions depend on smallness: a classifying topos exists for geometric theories over a small signature, and the geometric fragment excludes implication and universal quantification, so first-order theories are not classified. Reading propositions as objects also loses the distinction between proofs whenever the category is a poset.
© 2026 Lingenic LLC