PaperlayerView exact revision on arXiv

Source-linked AI summary

Logics vs doctrines, a mirror symmetry

Ivan Di Liberti, Umberto Tarantino, Lingyuan Ye

arXiv:2610.29771v2math.CTcs.LOmath.LO

TL;DR

The paper addresses how doctrines relate to fragments of geometric logic, amid unsettled definitions of doctrine and a syntax gap for the fragment framework. It proposes a working doctrine definition and establishes a Galois connection, then develops the resulting mirror symmetry and studies reflection through conceptual completeness.

  • Problem

    The notion of doctrine lacks a precise, unanimous definition, and the geometric-logic fragment framework has no naturally corresponding syntax.

    Source: Fragments of geometric logic · p. 3, §1.2.1 · p. 6

  • Method

    The paper proposes a working definition of doctrine and relates doctrines and geometric-logic fragments through two constructions forming a Galois connection.

    Source: §1.2.1 · p. 8, §2 · p. 12

  • Results

    The two constructions give a Galois connection between doctrines and logics, with size restrictions on both sides.

    Source: §2 · p. 12

  • Takeaways & Limitations

    Passing from a doctrine to its reflection gives a reflective embedding of algebra 2-categories, characterized under conceptual completeness in the coherent-logic case study.

    Source: Contribution and structure of the paper · p. 4

    The chosen notion excludes some 2-categories of theories, including categories with attributes and examples from type-theory semantics.

    Source: §1.2.1 · p. 6

Abstract

from arXiv · show

We study the relationship between doctrines, encoding 2-categories of theories in predicate logic, and fragments of geometric logic, defined through Kan injectivity in the 2-category of topoi. After a brief historical account of the notion of doctrine, we propose our working definition. Our main result then establishes a Galois connection between doctrines and subgeometric logics. This connection suggests a mirror symmetry between the world of doctrines and the world of logics, in which constructions and results on either side admit counterparts on the other. We develop this symmetry through constructions of syntactic categories and classifying topoi in both settings, recovering the familiar examples from categorical logic. We prove paired Diaconescu-type theorems and give symmetric universal characterisations of the two closure operators induced by the Galois connection. Finally, we show that passing from a doctrine to its closure induces a reflection between the corresponding 2-categories of algebras, and we relate this reflection to conceptual completeness.

Introduction

The paper fixes a working meaning of doctrine and connects it to fragments of geometric logic, then develops their correspondence and mirror symmetry.

There is doctrine and doctrine.

  • The paper treats doctrines as lax-idempotent pseudomonads on Lex, retaining a logical perspective in which their algebras represent theories.This framework recovers Reg, Coh, Disj, and Logoi as examples.Source: There is doctrine and doctrine · pp. 2–3

Fragments of geometric logic.

  • The geometric-logic fragment framework lacks a naturally corresponding syntax, while each fragment induces a doctrine whose algebras are its theories.The induced doctrine also encodes the logical operations of the fragment's syntactic categories.Source: Fragments of geometric logic · p. 3

Contribution and structure of the paper.

  • The paper also proves technical results showing that inclusions of doctrines induce forgetful functors between their algebra 2-categories.These results appear in its first section.Source: Contribution and structure of the paper · p. 3
  • The paper establishes a Galois correspondence between logics and doctrines, realized by assigning a doctrine to each logic and a logic to each doctrine.The correspondence is subject to appropriate size restrictions.Source: Contribution and structure of the paper · pp. 3–4
  • The paper develops a mirror symmetry in which constructions and results on logics and doctrines have counterparts, including syntactic categories, classifying topoi, and paired Diaconescu-like results.The paper relates the corresponding syntactic categories and classifying topoi.Source: Contribution and structure of the paper · p. 4
  • The two closure operators receive symmetric universal characterisations through classifying topoi on the logic side and syntactic categories on the doctrine side.These characterisations concern HTH and THT, respectively.Source: Contribution and structure of the paper · p. 4
  • Passing from a doctrine to its reflection yields a reflective embedding of the corresponding algebra 2-categories, with the image characterized under conceptual completeness in the coherent-logic case study.The characterization assumes conceptual completeness for the logic HT.Source: Contribution and structure of the paper · p. 4

AI Declaration.

  • The authors report using AI only to retrieve existing papers and correct language, not to obtain ideas, statements, or results.Source: AI Declaration · p. 4

1. Logics and doctrines

This section defines logics via Kan-injective topoi and introduces doctrines tied to lex-colimit completions, clarifying terminology and the role of density computed in CAT. It also orders doctrines by pointwise inclusion and describes the induced forgetful 2-functors between their categories of algebras.

1. Logics and doctrines

  • Inclusions of doctrines induce forgetful 2-functors between their 2-categories of algebras.Source: §1 · p. 5

1.1. Logics.

  • A logic is a class of geometric morphisms, and topoi formally in it are (weakly) right Kan-injective with respect to those morphisms.The framework identifies fragments of geometric logic through semantic prescriptions on categories of models.Source: §1.1 · p. 5

1.2. Doctrines.

  • The paper reserves “doctrine” for a logical fragment, distinguishing it from indexed-poset doctrines that represent individual theories.The authors describe the terminology as an ontological clash and note that a coherent hyperdoctrine represents a theory within coherent logic.Source: §1.2 · p. 6

1.2.1. Our notion of doctrine.

  • A doctrine is a lax-idempotent relative pseudomonad over Lex ↪ LEX whose values embed as full subcategories of presheaves and whose unit corestricts Yoneda.The definition is equivalent to requiring fully faithful units, pointwise left Kan extensions along them in CAT, and density in CAT; it excludes some 2-categories of theories, including categories with attributes.Source: §1.2.1 · pp. 6, 8
  • Every doctrine globalises to a lex-colimit completion, and every such completion is the globalisation of a unique doctrine.The paper also characterises qualifying submonads of the small-presheaf pseudomonad as lex-weight completions.Source: §1.2.1 · p. 7
  • An algebra for a doctrine is a category admitting the specified left Kan extensions along unit functors, and algebra morphisms preserve them.Small algebras can equivalently be described by unit functors that admit left adjoints.Source: §1.2.1 · p. 9

1.2.2. Essentially algebraic theories with pseudofalsum.

  • The least-subterminal-object pseudomonad is dense in LEX but not in CAT, showing that density in LEX alone does not characterize doctrines.Its algebras correspond to lex categories with a least subterminal object, or essentially algebraic theories extended with a pseudofalsum; the paper retains the stricter notion to match full geometric rules.Source: §1.2.2 · pp. 9–10

1.2.3. Base change and morphisms of doctrines.

  • Because a general theory of morphisms of doctrines is not yet available, the authors introduce a natural order sufficient for their results.Source: §1.2.3 · p. 10
  • T ⊆ T′ iff the specified left Kan extensions along their doctrine embeddings exist in LEX for each C; these extensions compute the inclusions T(C) → T′(C).Source: §1.2.3 · p. 11
  • When T ⊆ T′, every functor from a small category C to a T′-algebra A extends by left Kan extension to a T-algebra morphism T(C) → A.Source: §1.2.3 · p. 11
  • An inclusion T ⊆ T′ induces a forgetful 2-functor ALG(T′) → ALG(T), recovering Coh → Reg, Pretop → Coh, and Geom → Coh.Source: §1.2.3 · p. 12

2. A Galois connection

This section presents the antitone Galois connection between bounded logics and bounded doctrines, which organizes their correspondence between syntactic categorical structure and right Kan extension preservation, and gives examples that are not fixed points of the connection.

2.1. From logics to doctrines.

  • A logic H determines a doctrine TH(C) of H-injective morphisms from Psh(C) to Set[O], recovering exact-category and pretopos doctrines from regular and coherent logic.Source: §2.1 · p. 12

2.2. From doctrines to logics.

  • A doctrine T determines the logic HT of geometric morphisms whose direct images are T-algebra morphisms, recovering regular and coherent logic from regular-category and coherent-category doctrines.Source: §2.2 · p. 13
  • The connection links doctrine enlargement to conceptual completeness: coherent functors preserve existing finite coproducts and effective coequalisers, and coherent categories admitting them are pretopoi.The authors leave further development of this link to future work.Source: §2.2 · p. 13

F Psh(TC) TC

  • For a smallness-preserving doctrine T, HT consists exactly of morphisms along which the embeddings ΣηC preserve right Kan extensions, and HT is saturated.Source: §2.2 · p. 13, F Psh(TC) TC · pp. 14–15

2.3. The Galois connection between logics and doctrines.

  • For bounded H, H ⊆ HTH, TH is bounded, and h ∈ HTH exactly when every morphism between H-injectives preserves right Kan extensions along h.Source: §2.3 · pp. 17–18
  • For bounded logics and bounded doctrines, H ↦ TH and T ↦ HT form an antitone Galois connection, with T ⊆ THT as its unit.The adjunction is established for the bounded subclasses of both posets.Source: §2.3 · p. 18
  • Coherent logic Hflat and the pretopos doctrine Tpretop are mutual fixpoints: Tpretop = THflat and Hflat = HTpretop.Source: §2.3 · p. 18
  • The β-map logic Hβ is not a fixpoint, and THβ coincides with Tpretop.The text cites [DLTY26, Thm. 3.2.5] for the coincidence.Source: §2.3 · p. 18
  • The coherent-category doctrine Tcoh is not a fixpoint: HTcoh = Hflat, so it is not TH for any logic H.Tcoh is presented as a proper subdoctrine of Tpretop.Source: §2.3 · p. 18
  • All logics and doctrines considered below are assumed to be bounded.Source: §2.3 · p. 18

3. Mirror symmetry

The paper develops a mirror symmetry between logics and doctrines: constructions and results on the logic side have counterparts on the doctrine side, with syntactic categories more intrinsic to logics and classifying topoi more intrinsic to doctrines.

3. Mirror symmetry

  • The framework pairs constructions and interactions across logics and doctrines, including a doctrine-side counterpart to the logic-side Diaconescu-type theorem.The paper presents these pairs as evidence of a broader mirror symmetry.Source: §3 · p. 19

3.1. Syntactic categories.

  • The syntactic-category construction is native to logics, and the H-syntactic-category 2-functor lands in Alg(TH).For doctrines, the corresponding T-syntactic-category 2-functor lands in Alg(THT).Source: §3.1 · p. 20

3.2. Classifying topoi.

  • The doctrine-side classifying-topos 2-functor lands in WRInj(HT), and its associated topology is subcanonical.For a small T-algebra, the corestricted Yoneda embedding into its classifying topos is a morphism of T-algebras.Source: §3.2 · p. 21
  • Classifying topoi of small T-algebras are HT-injective.Their canonical embeddings into presheaf topoi serve as HT-presentations.Source: §3.2.1 · pp. 22–23

3.3. Diaconescu through the looking glass.

  • Paired Diaconescu-type theorems give 2-adjunctions connecting algebras and injective topoi on the logic and doctrine sides.For doctrines, the correspondence includes ALG(T)(A, E) ≃ Topoi(E, ClT(A)).Source: §3.3 · p. 24

4. Mise en abyme

The paper characterizes the two closure operators induced by the logic–doctrine correspondence through symmetric largest-extension properties: one uses classifying topoi, the other syntactic categories.

4. Mise en abyme

  • The full tour along the Galois connection yields symmetric universal characterizations of HTH and THT.These characterizations provide a starting point for studying the connection's fixpoints.Source: §4 · p. 25

4.1. HTH is the logic of H-classifying topoi.

  • HTH is the largest extension H′ of H for which the H-classifying-topos functor factors through WRInj(H′).Equivalently, HTH is characterized as the logic of H-classifying topoi.Source: §4.1 · p. 25

4.2. THT is the doctrine of T-syntactic categories.

  • THT is the largest extension T′ of T for which the T-syntactic-category functor factors through Alg(T′).This characterizes THT as the doctrine of T-syntactic categories.Source: §4.2 · p. 26

5. Reflecting on conceptual completeness

This section extends the reflection from coherent categories to doctrines and induced doctrines, connecting it to conceptual completeness and showing how it can be computed syntactically when the associated logic is conceptually complete. It characterizes conceptually complete T-algebras through Morita-equivalences and their relation to reflected THT-algebras, including their coincidence when HT is conceptually complete and the coherent case characterization of pretopoi.

5.1. The left adjoint exists.

  • For any inclusion T ⊆ T′, the forgetful 2-functor Alg(T′) → Alg(T) has a left 2-adjoint, constructed by closing each T-algebra inside ClT(A); the construction also works for large codomains.The left adjoint sends A to the smallest T′-subalgebra of ClT(A) containing A.Source: §5.1 · pp. 28–29

5.2. THT is a quotient of T.

  • For each small T-algebra A, the inclusion T(A) → THT(A) is a pseudoepimorphism, and the forgetful 2-functor Alg(THT) → Alg(T) is 2-fully faithful.Thus Alg(THT) embeds as a reflective sub-2-category of Alg(T).Source: §5.2 · pp. 29, 31

5.3. A syntactic description of concepts.

  • A doctrine T is called conceptually complete when SynT is essentially surjective; HT is complete if H is, and HT is complete if T is.The authors leave further development of this doctrinal notion and its relation to conceptual completeness for future work.Source: §5.3 · pp. 31–32
  • HT is conceptually complete exactly when the left 2-adjoint to Alg(THT) → Alg(T) is computed by SynHTClT; for coherent logic, this describes pretopos completion inside the coherent classifying topos.The theorem identifies conceptual completeness with the explicit syntactic formula for the reflection.Source: §5.3 · p. 32
  • Among coherent categories, pretopoi are exactly those that admit no proper conservative extensions, giving a classical categorical characterization of conceptual completeness.A coherent functor from a pretopos inducing an equivalence of categories is itself an equivalence.Source: §5.3 · p. 33
  • A small T-algebra is conceptually complete when every Morita-equivalence from it is an equivalence of categories.The definition’s model-equivalence condition ranges over every topos, rather than only Set; the difference vanishes with suitable completeness for set-based models, in particular in the coherent case.Source: §5.3 · p. 33
  • Every conceptually complete T-algebra is a THT-algebra, even without the assumption that HT is conceptually complete.The converse holds under that assumption.Source: §5.3 · pp. 33–34
  • If HT is conceptually complete, a small T-algebra is conceptually complete exactly when it lies in the image of Alg(THT) → Alg(T).In the coherent case, this says pretopoi are precisely the conceptually complete coherent categories, also in the set-based sense.Source: §5.3 · p. 34
Loading 2610.29771v2…