Overview
Research in categorical logic analyzes the relationship between doctrines—formulated to encode 2-categories of theories in predicate logic—and fragments of geometric logic defined via Kan injectivity within the 2-category of topoi. The primary result establishes a Galois connection between doctrines and subgeometric logics, identifying a mirror symmetry wherein constructions and results in one setting admit direct counterparts in the other.
Research Context
The investigation addresses categorical formulations of logical theories. It begins with a historical account of the notion of doctrine before establishing a working definition. Under this framework, doctrines model 2-categories of theories in predicate logic, whereas fragments of geometric logic are specified through Kan injectivity in the 2-category of topoi.
Approach
The authors construct a formal bridge between the doctrine-theoretic and logic-theoretic frameworks:
- Formulating an operative definition of doctrine grounded in the historical development of the concept.
- Constructing a Galois connection that links doctrines directly to subgeometric logics.
- Developing parallel constructions of syntactic categories and classifying topoi across both domains to instantiate the mirror symmetry.
- Deriving universal characterisations for closure operators and analyzing the behavior of the associated 2-categories of algebras.
Findings
The established Galois connection yields several structural results across both domains:
- Mirror Symmetry: Constructions and theoretical results concerning doctrines and subgeometric logics admit counterpart formulations across both sides of the Galois connection.
- Recovery of Established Examples: Parallel constructions of syntactic categories and classifying topoi recover familiar benchmark examples from categorical logic.
- Paired Diaconescu-Type Theorems: The authors prove paired Diaconescu-type theorems corresponding to each setting.
- Symmetric Universal Characterisations: Symmetric universal characterisations are provided for the two closure operators induced by the Galois connection.
- Algebraic Reflections and Conceptual Completeness: Moving from a doctrine to its closure induces a reflection between the corresponding 2-categories of algebras, which is shown to relate directly to conceptual completeness.
Why This Matters
The framework systematizes the relationship between predicate logic theories and geometric logic fragments, embedding classifying topoi and syntactic categories into a unified mirror symmetry while connecting algebraic reflections to conceptual completeness.