Technische Samenvatting: Doctrinale Semantiek van Gerichte Eerste-orde Logica

1. Probleemstelling

Het artikel adresseert de uitdaging om gerichte gelijkheid te formaliseren binnen een logisch raamwerk. Waar Lawvere's categorische perspectief klassieke gelijkheid succesvol karakteriseerde als een linkeradjunct aan contractie, rust deze aanpak op symmetrie. In gerichte type-theorie, waar types worden geïnterpreteerd als categorieën (of preordeningen) in plaats van groepoïden (of verzamelingen), wordt gelijkheid een asymmetrische relatie (bijvoorbeeld een herschrijving $a \to b$ of een orde $a \le b$).

De kernmoeilijkheid ligt in het hanteren van variatie (polariteit). In een gerichte setting kan een variabele in een "negatieve" positie verschijnen (contravariant, bijvoorbeeld de bron van een morfisme) of in een "positieve" positie (covariant, bijvoorbeeld het doel). Standaard logische regels voor gelijkheid (reflexiviteit en de J-regel/eliminatie) falen in deze context omdat ze impliciet symmetrie aannemen of toestaan dat variabelen tegelijkertijd in beide polariteiten verschijnen op manieren die symmetrie zouden afleiden ($a \le b \vdash b \le a$), wat ongeldig is in gerichte logica. Eerdere pogingen tot gerichte type-theorie worstelen vaak met deze polariteitsbeperkingen, met name in de context van proof-irrelevante logica (waar gelijkheid een propositie is, en niet een type met meerdere bewoners).

2. Methodologie

De auteurs ontwikkelen een gerichte eerste-orde logica (dFOL) en haar doctrinale semantiek door Lawvere's raamwerk van hyperdoctrines te generaliseren.

Syntaxis: Gepolariseerde Contexten

De syntaxis introduceert een gepolariseerde context $[\Theta \mid \Delta \mid \Gamma]$, die variabelen partitioneert in drie verzamelingen op basis van hun variatie:

• $\Theta$ (Negatief): Variabelen die uitsluitend in contravariante posities verschijnen.
• $\Gamma$ (Positief): Variabelen die uitsluitend in covariante posities verschijnen.
• $\Delta$ (Dinaturaal): Variabelen die in beide posities verschijnen (of toegestaan zijn om zo behandeld te worden).

Kernsyntactische kenmerken omvatten:

• Gerichte Gelijkheid ($\le_A$): Een primitieve relatie $s \le_A t$ waarbij $s$ getypeerd is in de negatieve context en $t$ in de positieve context.
• Gepolariseerde Implicatie: De implicatie $\psi \Rightarrow \phi$ wisselt de polariteit van de context voor $\psi$ om (verplaatsend van links naar rechts van de toonstaf), wat de contravariantie van het eerste argument weerspiegelt.
• Gepolariseerde Kwantoren: Kwantoren ($\forall^p, \exists^p$) zijn geïndexeerd op polariteit $p \in \{-, \Delta, +\}$ om de variatie van de gebonden variabele te volgen.
• Substitutieregels: Een gespecialiseerd substitutiemechanisme (Definitie 2.7) behandelt het herindexeren van termen over gepolariseerde contexten, waarbij wordt gegarandeerd dat dinaturale variabelen consistent worden gesubstitueerd.

Semantiek: Gerichte Doctrines

De semantiek wordt gevangen via gerichte doctrines, een generalisatie van Lawvere's doctrines.

• Basis Categorie: In plaats van een standaard categorie van types, is de basis een polarisatie-categorie $ndp(\mathcal{C})$, waarvan de objecten drietallen $(\Theta, \Delta, \Gamma)$ zijn en morfismen de variatiestructuur respecteren.
• Gefibereerde Structuur: Een functor $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ mapt gepolariseerde contexten naar posets van proposities.
• Kernvoorwaarden:
  • Geen-Dinaturaal-Variatie (ndv): Een voorwaarde die garandeert dat dinaturale variabelen in predicaten uitsluitend voortkomen uit het samenvoegen van positieve en negatieve variabelen, waardoor "derde" soorten variatie worden voorkomen.
  • Relatieve Adjuncties: Gerichte gelijkheid wordt niet gekarakteriseerd als een standaard linkeradjunct, maar als een linkerrelatieve adjunct aan een contractie-achtige operatie die twee variabelen van tegenovergestelde polariteit samenvoegt tot één enkele dinaturale variabele. Dit vangt de syntactische beperking die het afleiden van symmetrie verhindert.
  • Gepolariseerde Implicatie: Gekarakteriseerd als een relatieve co-adjunct.

3. Belangrijkste Bijdragen

1. Syntaxis van dFOL: Een precies natuurlijk deductiesysteem voor eerste-orde logica met gerichte gelijkheid, met een rigoureus systeem van polariteiten geïnspireerd op dinaturaliteit. Dit systeem verbiedt expliciet de afleiding van symmetrie voor gerichte gelijkheid, terwijl standaard logische connectieven behouden blijven.
2. Karakterisering van Gerichte Gelijkheid: Het artikel generaliseert Lawvere's "gelijkheid als linkeradjunct" naar gerichte gelijkheid als linkerrelatieve adjunct. Dit biedt een precieze categorische universele eigenschap voor gerichte gelijkheid die rekening houdt met de asymmetrie van de relatie.
3. Gerichte Doctrines: De introductie van gerichte doctrines als een semantisch raamwerk. De auteurs bewijzen dat de syntaxis van dFOL sound en compleet is met betrekking tot deze semantiek.
4. Preorde-Completiteit: Een specifiek compleetheidsresultaat wordt bewezen voor het klassieke fragment van dFOL met betrekking tot het standaardmodel van preordeningen ($\mathbf{Preord}$). Dit stelt vast dat elke entailment die geldig is in alle preorde-modellen, afleidbaar is in de syntaxis.
5. Hantering van Polariteit: Het artikel demonstreert hoe variatie kan worden beheerd in een proof-irrelevante setting, onderscheidend van proof-relevante gerichte type-theorieën (zoals die in $\mathbf{Cat}$) door het gebruik van posetale fibraties en poset-waardige vezels.

4. Resultaten

• Soundness en Completiteit: De auteurs vestigen een bi-adjunctie tussen de categorie van theorieën ($\mathbf{Theory}$) en de 2-categorie van gerichte doctrines ($\mathbf{DDoctrine}$). Dit impliceert dat dFOL de interne taal is van gerichte doctrines.
• Completiteit voor Preordeningen: Met behulp van een Henkin-achtige constructie aangepast voor gepolariseerde contexten, bewijst het artikel dat het klassieke fragment van dFOL compleet is met betrekking tot het model van preordeningen. De constructie definieert het domein van het model als de verzameling van gesloten termen, geordend door de afleidbaarheid van gerichte gelijkheid ($\le_A$).
• Afgeleide Regels: Het systeem ondersteunt afgeleide regels voor transitiviteit, reflexiviteit en congruentie van gerichte gelijkheid, evenals interactieregels tussen gepolariseerde kwantoren en implicatie.
• Tegenvoorbeelden: Het artikel illustreert dat symmetrie ($a \le b \vdash b \le a$) niet afleidbaar is, en het preorde-model dient als een tegenmodel voor dergelijke afleidingen.

5. Betekenis en Claims

Het artikel claimt de werken van Lawvere over de rol van variatie en hom-functoren in de logica te bevorderen. Specifiek:

• Het biedt een precieze syntactische en semantische karakterisering van gerichte gelijkheid in een proof-irrelevante setting, waardoor een gat wordt gedicht tussen klassieke logica en gerichte type-theorie.
• Het generaliseert het concept van gelijkheid als een adjunct naar het gerichte geval via relatieve adjuncties, en biedt een nieuw categorisch hulpmiddel voor het begrijpen van gerichte structuren.
• Het demonstreert dat gerichte logica kan worden behandeld met standaard logische technieken (zoals Henkin-completiteit) door polariteiten zorgvuldig te beheren via gepolariseerde contexten, in plaats van complexe geometrische of hoger-categorische machinery te vereisen.
• Het werk wordt gepositioneerd als een fundamentele stap voor redeneren over herschrijfsystemen en gerichte fenomenen (processen, transities) binnen een logisch raamwerk, onderscheiden van de proof-relevante benaderingen van Homotopie Type-theorie.

De auteurs stellen expliciet dat hun focus ligt op de proof-irrelevante case, gerechtvaardigd door de aard van herschrijflogica (waar een herschrijving óf plaatsvindt óf niet) en het gebruik van posetale fibraties in categorische logica. Zij claimen niet de volledige complexiteit van afhankelijke gerichte type-theorie op te lossen, maar bieden een robuuste basis voor het eerste-orde, preorde-gebaseerde geval.