Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logic and Concepts in the 2-category of Topoi

Ivan Di Liberti, Lingyuan Ye

TL;DR

This work develops a modular framework using Kan injectivity in the 2-category Topoi to axiomatize fragments of geometric logic, encoding semantic prescriptions via WRInj(H) and a lax-idempotent pseudomonad T^H. It links semantics, syntax, and classifying topoi through Diaconescu-type results, presenting explicit correspondences for fragments such as essentially algebraic, disjunctive, regular, and coherent logic. The paper demonstrates that algebras for T^H admit classifying topoi and a conceptual completeness phenomenon, providing a unified, modular account of classical logical fragments within topos theory. It also offers a program for future exploration of formal category theory in Topoi, including deeper connections to syntactic sites, doctrines, and abstract logic.

Abstract

We use Kan injectivity to axiomatise concepts in the 2-category of topoi. We showcase the expressivity of this language through many examples, and we establish some aspects of the formal theory of Kan extension in this 2-category (pointwise Kan extensions, fully faithful morphisms, etc.). We use this technology to introduce fragments of geometric logic, and we accommodate essentially algebraic, disjunctive, regular, and coherent logic in our framework, together with some more exotic examples. We show that each fragment $\mathcal{H}$ in our sense identifies a lax-idempotent (relative) pseudomonad $\mathsf{T}^{\mathcal{H}}$ on $\mathsf{lex}$, the $2$-category of finitely complete categories. We show that the algebras for $\mathsf{T}^{\mathcal{H}}$ admit a notion of classifying topos, for which we deliver several Diaconescu-type results. The construction of classifying topoi allows us to define conceptually complete fragments of geometric logic.

Logic and Concepts in the 2-category of Topoi

TL;DR

This work develops a modular framework using Kan injectivity in the 2-category Topoi to axiomatize fragments of geometric logic, encoding semantic prescriptions via WRInj(H) and a lax-idempotent pseudomonad T^H. It links semantics, syntax, and classifying topoi through Diaconescu-type results, presenting explicit correspondences for fragments such as essentially algebraic, disjunctive, regular, and coherent logic. The paper demonstrates that algebras for T^H admit classifying topoi and a conceptual completeness phenomenon, providing a unified, modular account of classical logical fragments within topos theory. It also offers a program for future exploration of formal category theory in Topoi, including deeper connections to syntactic sites, doctrines, and abstract logic.

Abstract

We use Kan injectivity to axiomatise concepts in the 2-category of topoi. We showcase the expressivity of this language through many examples, and we establish some aspects of the formal theory of Kan extension in this 2-category (pointwise Kan extensions, fully faithful morphisms, etc.). We use this technology to introduce fragments of geometric logic, and we accommodate essentially algebraic, disjunctive, regular, and coherent logic in our framework, together with some more exotic examples. We show that each fragment in our sense identifies a lax-idempotent (relative) pseudomonad on , the -category of finitely complete categories. We show that the algebras for admit a notion of classifying topos, for which we deliver several Diaconescu-type results. The construction of classifying topoi allows us to define conceptually complete fragments of geometric logic.

Paper Structure

This paper contains 34 sections, 63 theorems, 90 equations, 2 tables.

Table of Contents

  1. The framework of Kan injectivity
  2. Kan injectivity
  3. A trivial example: geometric logic
  4. A pet example: essentially algebraic logic
  5. A full example: propositional logic
  6. Universals in the 2-category of topoi
  7. A proarrow equipment
  8. On the role of embeddings
  9. On the role of corepresentable surjections
  10. All concepts are Kan extensions
  11. Filtered colimits, a tautological example
  12. Terminal object and Totally Connected Topoi
  13. Groupoidal points
  14. Preorder points
  15. Logic as concept
  16. ...and 19 more sections

Key Result

Theorem 1

Every logic $\mathcal{H}$ has an associated lax-idempotent (relative) pseudomonad $\mathsf{T}^{\mathcal{H}}$ defined over $\mathsf{lex}$. There is a logic $\mathcal{H}_{\text{flat}}$ whose associated $\mathsf{T}^{\mathcal{H}_{\text{flat}}}$ precisely the free pretopos construction over a lex categor

Theorems & Definitions (191)

  • Theorem : \ref{['constr:fromlotodoc']} and \ref{['prop:synofcoh']}
  • Theorem : \ref{['constr:classtopos']} and \ref{['diaconescu']}
  • Theorem : \ref{['chargeom']}, \ref{['class:essalg']}, \ref{['class:prop']}
  • Proposition : \ref{['prop:ranemiffweak']}
  • Theorem : \ref{['thm:cohalgebra']}
  • Definition : The $2$-category of topoi
  • Definition
  • Lemma 1.1.1
  • proof
  • Lemma 1.1.2
  • ...and 181 more