14.4 Logic in topoi and sheaf theory

Topoi, categories that mimic sets, have an internal logic akin to intuitionistic logic. This logic is built using the subobject classifier and other topos structures, allowing for powerful reasoning within the category.

Sheaf theory and topoi are deeply connected. Every topos is equivalent to a category of sheaves on a site, and the internal logic of a sheaf topos relates closely to the site's logic, offering applications in various mathematical fields.

Internal Logic and Sheaf Theory in Topoi

Logic and structure of topoi

• A topos is a category that behaves like the category of sets with a terminal object, pullbacks, exponentials, and a subobject classifier
• The internal logic of a topos is a higher-order intuitionistic logic that satisfies all the axioms of intuitionistic logic, but not necessarily classical logic (law of excluded middle and axiom of choice may not hold)
• The subobject classifier $\Omega$ plays the role of a truth-value object where morphisms from an object $A$ to $\Omega$ correspond to subobjects of $A$
• The internal logic of a topos is constructed using the subobject classifier and other topos-theoretic structures (exponentials, pullbacks)

Topoi and sheaf theory connection

• A sheaf is a functor $F: C^{op} \to \mathbf{Set}$ where for each open cover $\{U_i\}$ of an object $U$ in $C$, the diagram induced by restriction maps is an equalizer
• The category of sheaves on a site $(C, J)$ forms a topos $\mathbf{Sh}(C, J)$ where $C$ is a category with a Grothendieck topology $J$ specifying which families of morphisms are "covering families"
• Every topos is equivalent to the category of sheaves on some site (Giraud-Diaconescu theorem)
• The internal logic of a topos of sheaves is closely related to the logic of the site with the subobject classifier in $\mathbf{Sh}(C, J)$ being the sheafification of the presheaf of sieves

Internal language of topoi

• Formulas in the internal language of a topos are built from terms using logical connectives and quantifiers
  • Terms are interpreted as morphisms in the topos
  • Predicates are interpreted as subobjects (morphisms into the subobject classifier)
• Logical connectives are interpreted using the structure of the subobject classifier:
  1. $\top$ is the maximal subobject
  2. $\bot$ is the minimal subobject
  3. $\phi \wedge \psi$ is the pullback of $\phi$ and $\psi$
  4. $\phi \vee \psi$ is their pushout
  5. $\phi \Rightarrow \psi$ is the exponential $\psi^\phi$
• Quantifiers are interpreted using adjoints to substitution functors:
  • For a morphism $f: A \to B$, $\exists_f$ is the left adjoint to $f^*$
  • $\forall_f$ is the right adjoint
• The interpretation of a formula $\phi(x)$ with a free variable $x$ of type $A$ is a subobject of $A$

Applications of topos logic

• The internal logic can reason about sheaves and their properties (a sheaf is injective iff it satisfies a certain internal logic formula)
• Many constructions in sheaf theory can be expressed using the internal logic (sheafification, sheaf of sections)
• The internal logic of a topos can study models of various theories:
  • The effective topos is a model of synthetic domain theory
  • The Zariski topos of a scheme encodes its Zariski geometry
• Topos-theoretic methods have applications in algebraic geometry, mathematical physics, and computer science where the internal logic provides a powerful reasoning tool