🧮Topos Theory Unit 11 – Internal Logic and Mitchell–Bénabou Language

Key Concepts

• Internal logic provides a way to reason about objects and morphisms within a topos using intuitionistic logic
• Mitchell–Bénabou language (also known as the internal language of a topos) formalizes the internal logic of a topos
  • Allows for expressing properties and constructions in a topos using a typed language similar to first-order logic
• Topoi serve as generalized models of set theory that allow for the interpretation of intuitionistic logic
• The internal logic of a topos is constructed using the structure of the topos itself (subobject classifier, exponential objects, and finite limits)
• Logical operations in a topos (conjunction, disjunction, implication, and quantifiers) are defined using categorical constructions
• The soundness and completeness of the internal logic with respect to the topos semantics establish a strong connection between the syntax and semantics of the language
• Applications of internal logic include reasoning about sheaves, geometric morphisms, and the construction of new topoi from existing ones

Foundations of Internal Logic

• Internal logic arises from the observation that a topos has a structure rich enough to interpret intuitionistic first-order logic
• The subobject classifier $\Omega$ in a topos plays a crucial role in defining the internal logic
  • Morphisms from an object $A$ to $\Omega$ correspond to subobjects of $A$, which can be seen as "predicates" or "properties" of $A$
• Exponential objects in a topos allow for the interpretation of function types and lambda abstraction in the internal language
• Finite limits in a topos (pullbacks and terminal object) are used to interpret conjunction, existential quantification, and substitution in the internal logic
• The internal logic of a topos is intuitionistic, meaning that the law of excluded middle and the axiom of choice may not hold in general
• Intuitionistic logic allows for a constructive approach to mathematics, where proofs are seen as algorithms or constructions rather than mere existence statements

Mitchell–Bénabou Language Basics

• The Mitchell–Bénabou language is a typed language that extends the simply typed lambda calculus with additional constructs for reasoning about objects and morphisms in a topos
• Types in the language correspond to objects in the topos, while terms correspond to morphisms
• The language includes basic types such as the terminal type $1$ and the subobject classifier type $\Omega$
• Function types $A \to B$ represent exponential objects in the topos, allowing for the interpretation of lambda abstraction and application
• The language also includes product types $A \times B$ and sum types $A + B$, corresponding to categorical products and coproducts, respectively
• Dependent types, such as $\prod_{x:A} B(x)$ and $\sum_{x:A} B(x)$, allow for the expression of more complex properties and constructions in the topos
• The language includes a typing judgment $\Gamma \vdash t : A$, which asserts that the term $t$ has type $A$ in the context $\Gamma$

Syntax and Semantics

• The syntax of the Mitchell–Bénabou language specifies the well-formed terms and formulas of the language
  • Includes rules for variable binding, lambda abstraction, application, pairing, and projection
• The semantics of the language is given by interpreting types as objects in the topos and terms as morphisms between those objects
• The interpretation of a type $A$ in a topos $\mathcal{E}$ is denoted by $\llbracket A \rrbracket_{\mathcal{E}}$, which is an object in $\mathcal{E}$
• The interpretation of a term $t$ of type $A$ in a context $\Gamma$ is a morphism $\llbracket \Gamma \vdash t : A \rrbracket_{\mathcal{E}} : \llbracket \Gamma \rrbracket_{\mathcal{E}} \to \llbracket A \rrbracket_{\mathcal{E}}$
• Soundness of the language ensures that well-typed terms are interpreted as morphisms in the topos, while completeness ensures that every morphism in the topos can be represented by a term in the language
• The interpretation of the language in a topos is compatible with the categorical structure of the topos (composition, identities, and universal properties)

Logical Operations in Topoi

• Logical operations in a topos are defined using categorical constructions, allowing for the interpretation of intuitionistic first-order logic
• Conjunction $A \wedge B$ is interpreted as the product of subobjects, corresponding to the categorical pullback
• Disjunction $A \vee B$ is interpreted as the union of subobjects, which can be constructed using the coproduct and the subobject classifier
• Implication $A \Rightarrow B$ is interpreted as the exponential object $B^A$, representing the internal hom between subobjects
• Universal quantification $\forall x:A. P(x)$ is interpreted using the right adjoint to the pullback functor, corresponding to the internal product $\prod_{x:A} P(x)$
• Existential quantification $\exists x:A. P(x)$ is interpreted using the left adjoint to the pullback functor, corresponding to the internal sum $\sum_{x:A} P(x)$
• The interpretation of logical operations in a topos satisfies the axioms of intuitionistic first-order logic, providing a sound and complete semantics for the internal logic

Applications in Category Theory

• Internal logic and the Mitchell–Bénabou language provide a powerful tool for reasoning about objects and morphisms in a topos
• Sheaf theory: The internal logic can be used to express properties of sheaves and to construct new sheaves from existing ones
  • For example, the internal language can be used to define the notion of a locally constant sheaf and to prove that the category of locally constant sheaves is equivalent to the category of sets
• Geometric morphisms: The internal logic can be used to study geometric morphisms between topoi, which are functors that preserve the categorical structure and the internal logic
  • The internal language can be used to express properties of geometric morphisms, such as the notion of a surjective geometric morphism or an essential geometric morphism
• Construction of new topoi: The internal logic can be used to construct new topoi from existing ones, such as the classifying topos of a geometric theory or the topos of sheaves on a site
  • The internal language provides a way to express the axioms of a geometric theory and to reason about models of the theory in a topos

Advanced Topics and Extensions

• Higher-order logic: The Mitchell–Bénabou language can be extended to higher-order logic by allowing quantification over function types and power object types
  • This extension allows for the expression of more complex properties and constructions in a topos, such as the notion of a complete topos or a cocomplete topos
• Heyting-valued models: The internal logic of a topos can be used to construct Heyting-valued models of set theory, where the truth values are taken from a complete Heyting algebra
  • These models provide a way to study independence results and to construct new models of set theory with specific properties
• Realizability topoi: Realizability topoi are a class of topoi that are constructed from a partial combinatory algebra (PCA) and provide a computational interpretation of the internal logic
  • The internal language of a realizability topos can be used to study the computational content of mathematical proofs and to extract programs from proofs
• Topos-theoretic approaches to physics: The internal logic of a topos has been applied to the study of quantum mechanics and quantum field theory
  • The use of a topos allows for a more constructive and intuitionistic approach to quantum theory, avoiding some of the paradoxes and conceptual difficulties of the standard formulation

Common Pitfalls and Misconceptions

• Confusing internal logic with external logic: It is important to distinguish between the internal logic of a topos, which is intuitionistic, and the external logic used to reason about the topos itself, which is typically classical
  • Some properties that hold in the external logic may not hold in the internal logic, and vice versa
• Assuming that all topoi are models of classical logic: While every topos is a model of intuitionistic logic, not every topos is a model of classical logic
  • The law of excluded middle and the axiom of choice may fail in some topoi, such as the topos of sheaves on a non-trivial topological space
• Neglecting the role of the subobject classifier: The subobject classifier is a crucial ingredient in the construction of the internal logic of a topos
  • Failing to consider the properties of the subobject classifier can lead to incorrect reasoning about the internal logic
• Misinterpreting the meaning of logical connectives: The logical connectives in the internal logic of a topos may have different properties than their classical counterparts
  • For example, the double negation of a proposition may not imply the original proposition, and the law of excluded middle may not hold for all propositions
• Overlooking the constructive nature of internal logic: The internal logic of a topos is inherently constructive, meaning that proofs in the internal logic can be seen as algorithms or constructions
  • This constructive aspect is important for applications in computer science and the extraction of programs from proofs