Conceptual completeness for subgeometric logics

Titel: Conceptuele Volledigheid voor Subgeometrische Logica's
Auteurs: Ivan Di Liberti, Umberto Tarantino, en Lingyuan Ye

1. Probleem en Motivatie

Het artikel behandelt het begrip conceptuele volledigheid binnen het kader van subgeometrische logica's (fragmenten van geometrische logica). Traditioneel wordt conceptuele volledigheid, zoals vastgesteld door Makkai voor coherente eerste-orde logica [Mak87], geïnterpreteerd als een reconstructietheorema: de syntaxis van een theorie kan worden teruggewonnen uit de semantiek (de categorie van modellen), mits deze laatste is voorzien van extra structuur (specifiek, een "ultrastructuur" afgeleid van ultraproducten).

De auteurs identificeren een beperking in deze traditionele visie: deze leunt zwaar op verzet-gebaseerde semantiek en het opleggen van extra structuur (ultrastructuur) aan categorieën van modellen. Bovendien vereisten eerdere benaderingen om conceptuele volledigheid voor verschillende fragmenten van logica te bewijzen vaak onafhankelijke, ad-hoc technieken voor elk fragment. Het artikel streeft naar:

1. Het herformuleren van conceptuele volledigheid als een puur syntactisch fenomeen, specifiek als een dualiteit tussen theorieën en hun klassificerende topoi, in plaats van een reconstructie vanuit verzet-gebaseerde modellen.
2. Het bieden van een modulair kader om conceptuele volledigheid voor diverse subgeometrische logica's te bewijzen zonder te vertrouwen op Makkai's oorspronkelijke reconstructietheorema of het opleggen van kunstmatige structuren aan de semantiek.
3. Het verhelderen van de relatie tussen deze nieuwe syntactische notie en Makkai's traditionele semantische reconstructie, met name onder de aanname van volledigheid ten opzichte van verzet-gebaseerde modellen.

2. Methodologie en Kader

De auteurs bouwen voort op het kader van rechter Kan-injectiviteit in de 2-categorie van topoi ($\mathbf{Topoi}$), zoals ontwikkeld in hun eerdere werk [DLY25].

• Logica's als klassen van morfismen: Een logica $\mathcal{H}$ wordt gedefinieerd als een klasse van geometrische morfismen tussen topoi. Een topos $\mathcal{X}$ "behoort formeel tot" $\mathcal{H}$ als deze (zwak) rechter Kan-injectief is met betrekking tot $\mathcal{H}$-morfismen. Dit vangt het idee dat de gegeneraliseerde punten van de topos de door de logica voorgeschreven structuur bezitten.
• Syntactische Categorieën en Klassificerende Topoi:
  • Voor een topos $\mathcal{X}$ die formeel in $\mathcal{H}$ zit, wordt de syntactische categorie $\text{Syn}_{\mathcal{H}}(\mathcal{X})$ gedefinieerd als de categorie van geometrische morfismen $\mathcal{X} \to \text{Set}[\mathcal{O}]$ (waarbij $\text{Set}[\mathcal{O}]$ de object-classifier is).
  • Aan $\mathcal{H}$ is verbonden een monade van syntaxis $T_{\mathcal{H}}$ op de categorie van kleine, eindelijk complete categorieën ($\mathbf{Lex}$).
  • De klassificerende topos $\text{Cl}_{\mathcal{H}}(A)$ wordt geconstrueerd voor een $T_{\mathcal{H}}$-algebra $A$.
• Definitie van Conceptuele Volledigheid: Een begrensde logica $\mathcal{H}$ is conceptueel volledig als de 2-functor $\text{Cl}_{\mathcal{H}}: \text{Alg}(T_{\mathcal{H}})^{\text{op}} \to \mathbf{WRInj}(\mathcal{H})$ 2-volledig faithful is.
• Kerninzicht: De auteurs tonen aan dat conceptuele volledigheid equivalent is aan de stelling dat de conjunctie $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$ een reflectie is (dat wil zeggen, de counit is een equivalentie). Dit betekent dat elke $T_{\mathcal{H}}$-algebra essentieel de syntactische categorie is van zijn klassificerende topos. Deze formulering ontkoppelt het concept van verzet-gebaseerde modellen en richt zich op de relatie tussen syntaxis (algebra's) en syntaxis-gebaseerde semantiek (klassificerende topoi).

3. Belangrijke Bijdragen en Resultaten

A. Karakterisering van Conceptuele Volledigheid

Het artikel stelt vast dat een logica $\mathcal{H}$ conceptueel volledig is dan en slechts dan als, voor elke kleine $T_{\mathcal{H}}$-algebra $A$, de inbedding $A \hookrightarrow \text{Syn}_{\mathcal{H}}(\text{Cl}_{\mathcal{H}}(A))$ een equivalentie van categorieën is (Corollary 2.2.3). Dit herkadert het probleem als de vraag of de syntactische categorie van de klassificerende topos de oorspronkelijke algebra terugwint.

B. Bewijs van Conceptuele Volledigheid voor Vier Logica's

Met behulp van een Reductielemma (Proposition 3.1.2) bewijzen de auteurs de conceptuele volledigheid voor vier specifieke logica's door ze te identificeren met bekende doctrines en door te tonen dat hun syntactische categorie's de algebra's terugwinnen. De bewijzen maken gebruik van specifieke subklassen van morfismen (sublogica's) om de analyse te vereenvoudigen:

1. Coherente Logica ($\mathcal{H}_{\text{flat}}$): Bewezen conceptueel volledig. De auteurs tonen aan dat de doctrine $T_{\mathcal{H}_{\text{flat}}}$ samenvalt met de vrije pretopos-constructie. Zij karakteriseren de syntactische categorie van een coherente topos als de volledige subcategorie van coherente objecten, waarmee de oorspronkelijke pretopos wordt teruggewonnen.
2. Reguliere Logica ($\mathcal{H}_{\text{matte}}$): Bewezen conceptueel volledig. De doctrine komt overeen met de vrije (Barr-)exacte categorie-constructie. Er wordt aangetoond dat de syntactische categorie bestaat uit reguliere objecten.
3. Essentieel Algebraïsche Logica met Falsum ($\mathcal{H}_{\text{dom}}$): Bewezen conceptueel volledig. De doctrine komt overeen met de vrije lex categorie met een strikt initiële object. Het bewijs behelst het analyseren van dichte inbeddingen en het aantonen dat objecten in de syntactische categorie retracten zijn van representabelen.
4. Finietair Disjunctieve Logica ($\mathcal{H}_{\text{pure}}$): Bewezen conceptueel volledig. De doctrine komt overeen met de vrije lextensieve categorie-constructie. Het bewijs maakt gebruik van "pure inbeddingen" en de join van een categorie met zijn Booleaanse algebra van decidabele subterminale objecten.

Deze resultaten bieden nieuwe karakteriseringen voor deze logica's die niet rusten op Makkai's oorspronkelijke theorem [Mak87].

C. Conservatief Ingebedde Logica's

Het artikel introduceert het begrip conservatief ingebedde logica's (Sectie 4). Een logica is conservatief ingebed als de conjunctie $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$ idempotent is.

• Resultaat: Elke conceptueel volledige logica is een conservatief ingebedde logica.
• Betekenis: Deze eigenschap heeft een bewijs-theoretische interpretatie: de inclusie van de theorie van de syntactische categorie in de theorie van de klassificerende topos is conservatief. Dit verbindt de semantische notie van conceptuele volledigheid direct met bewijs-theoretische conservativiteit.

D. Relatie met Makkai's Theorem

In Sectie 5 verzoenen de auteurs hun syntactische definitie met Makkai's traditionele semantische reconstructietheorema voor coherente logica.

• Kader: Zij maken gebruik van de theorie van virtuele ultracategorieën (uit [Saa25, Ham25, vGMT26]) om semantische voorschriften te formaliseren.
• Equivalentie: Zij demonstreren dat voor coherente logica hun notie van conceptuele volledigheid equivalent is aan Makkai's resultaat (Corollary 5.3.3).
• Mechanisme: De equivalentie houdt stand onder de aanname dat de klassificerende topoi genoeg punten hebben (volledigheid ten opzichte van verzet-gebaseerde modellen). De auteurs breken het resultaat af in:
  1. Een syntactisch component: De logica is conceptueel volledig in hun zin (dualiteit tussen algebra's en klassificerende topoi).
  2. Een semantisch component: De equivalentie tussen klassificerende topoi en ultracategorieën van verzet-gebaseerde modellen (geïnduceerd door de "genoeg punten" aanname).
• Generalisatie: Zij definiëren "conceptuele volledigheid à la Makkai" voor algemene logica's (Definitie 5.4.1) en bewijzen dat deze equivalent is aan hun syntactische notie indien de logica genoeg verzet-gebaseerde modellen heeft (Theorem 5.4.2).

4. Betekenis en Claims

Het artikel claimt een nieuw bewijs-theoretisch licht op conceptuele volledigheid te werpen.

• Modulariteit: Het biedt een verenigd kader (via Kan-injectiviteit) om conceptuele volledigheid over verschillende subgeometrische logica's te bestuderen, wat de noodzaak voor ad-hoc technieken vermindert.
• Ontkoppeling van Verzet-gebaseerde Semantiek: De primaire definitie van conceptuele volledigheid wordt gepresenteerd als een eigenschap van de logica zelf (een dualiteit tussen theorieën en klassificerende topoi), onafhankelijk van verzet-gebaseerde modellen. De verbinding met Makkai's theorem wordt getoond als een consequentie van volledigheid ten opzichte van verzet-gebaseerde modellen, niet als de definitie zelf.
• Herstel van Klassieke Resultaten: Het artikel slaagt erin Makkai's oorspronkelijke theorem voor coherente logica te herstellen als een speciaal geval waarbij de syntactische dualiteit samenvalt met de semantische reconstructie via ultracategorieën.
• Conservativiteit: Het stelt vast dat conceptuele volledigheid een sterke conservativiteitseigenschap impliceert, waarmee model-theoretische eigenschappen aan bewijs-theoretische worden gekoppeld.

De auteurs blijven bescheiden over de reikwijdte en merken op dat hoewel zij conceptuele volledigheid voor verschillende fragmenten hebben bewezen, de vraag of alle fragmenten van geometrische logica conceptueel volledig zijn, open blijft, en dat de karakterisering van de kolom $\mathbf{WRInj}_{pw}(\mathcal{H})$ in hun samenvattende tabel aan toekomstig onderzoek wordt overgelaten. Zij merken ook op dat hun huidige voorbeelden "onder" het coherente fragment liggen, hoewel zij vermoeden dat de theorie breder van toepassing is.