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 through the lens of 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 |
| + | — | Coproduct | Categorical sum |
| → | U+2192 | Morphism/Exponential | Arrow or function space |
| 1 | — | Terminal | True / Unit |
| 0 | — | Initial | False / Empty |
| Ω | U+03A9 | Subobject classifier | Object of truth values |
| Bᴬ | — | Exponential | Internal hom |
| ∘ | U+2218 | Composition | Morphism composition |
| ≅ | U+2245 | Isomorphism | Equivalent objects |
| ⊣ | U+22A3 | Adjunction | Adjoint functors |
| Hom | — | Hom-set | Morphisms between |
Metatheory. Completeness: a theory is consistent iff it has a model in some topos. Every topos models intuitionistic HOL; Boolean toposes model classical logic. The internal/external distinction: external statements about the topos vs internal statements in its logic. Classifying toposes: every geometric theory has a classifying topos. Presheaf toposes are always well-behaved; sheaf toposes capture richer structure.
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. High abstraction: requires category theory background. Internal language can obscure computational content. Not all mathematicians accept topos-theoretic foundations. Specific computations may be easier in set theory. The generality comes at the cost of concreteness. Different toposes behave very differently; intuitions don't always transfer.
© 2026 Lingenic LLC