A Proof-theoretic Semantics for Intuitionistic Linear Logic

Probleem
Bewijs-theoretische semantiek (P-tS) streeft ernaar om betekenis te verlenen aan logische expressies door middel van het begrip bewijs in plaats van waarheid. Terwijl Sandqvist succesvol een basis-extensie semantiek (B-eS) heeft vastgesteld voor Intuïtionistische Propositielogica (IPL), en Gheorghiu, Gu, en Pym dit hebben uitgebreid naar het multiplicatieve fragment van de Intuïtionistische Lineaire Logica (IMLL), bleef een volledige P-tS voor de volledige Intuïtionistische Lineaire Logica (ILL) ongrijpbaar. De primaire uitdaging ligt in het substructurele karakter van ILL, dat algemene verzwakking (weakening) en contractie verbiedt, en de inclusie van additieve connectieven en de exponentiële modaliteit (!). Bestaande benaderingen worstelen met het behandelen van de interactie tussen deze kenmerken binnen een basis-extensie kader. Specifiek is het definiëren van een ondersteuningsrelatie die de hulpbron-gevoelige aard van ILL respecteert en tegelijkertijd de inferentiële inhoud van het "bang"-connectief (!) correct vangt — een modale operator die strikte afleidingen vereist — een aanzienlijke moeilijkheid. Bovendien vertrouwen standaard natuurlijke deductie systemen voor ILL vaak op ad-hoc zijvoorwaarden met betrekking tot contextdeling (additiviteit) en het aantal premissen, die moeilijk te formaliseren zijn binnen de rigide, niet-schematische structuur die vereist is voor atomaire regels in B-eS.

Methodologie
Het artikel stelt een nieuwe basis-extensie semantiek voor ILL voor door twee belangrijke technische hindernissen aan te pakken: de formalisering van natuurlijke deductie regels zonder schematische context-metavariabelen, en de definitie van een ondersteuningsrelatie die additiviteit en modaliteit behandelt.

1. Herformulering van Natuurlijke Deductie: De auteur introduceert een nieuwe syntaxis voor het natuurlijke deductie systeem NILL met behulp van "additieve boxen" (aangeduid met accolades {...}) en "modale boxen" (aangeduid met semantische haken J...K).

   • Additieve Boxen: Deze markeren gedeelde contexten, waardoor het systeem additieve connectieven (zoals & en ⊕) en regels met variabele premissen (zoals ⊤I en 0E) kan representeren zonder te vertrouwen op willekeurige context-metavariabelen. Dit maakt een systematische behandeling van additiviteit mogelijk waarbij afleidingen binnen een box dezelfde multiset van open aannames delen.
   • Modale Boxen: Deze worden gebruikt om de promotie-regel (Prom) te karakteriseren. De regel wordt hergedefinieerd zodat vereist wordt dat de conclusie volgt uit een context waar alle aannames conclusies zijn van regels die alleen modale boxen boven hen bevatten. Dit vangt de strikte afleidingsvereiste van de exponentiële modaliteit zonder expliciet naar het ! connectief te verwijzen in de structurele definitie van de regel.
   • De auteur bewijst dat dit nieuwe systeem equivalent is aan de standaard sequent-stijl NILL (Theorema 2.7).

2. Atomaire Afleidbaarheid en Ondersteuningsrelatie:

   • Atomaire Regels: De semantiek definieert atomaire regels als triples bestaande uit een multiset van additieve boxen, een enkele additieve box (de conclusie), en een atoom. Dit weerspiegelt de structuur van de geherformuleerde natuurlijke deductie regels.
   • Basis Extensie: Een basis $B$ is een verzameling van dergelijke atomaire regels. De afleidbaarheidsrelatie $\vdash_B$ wordt inductief gedefinieerd, waarbij de multiplicatieve splitsing van contexten en de additieve sharing via de box-structuur worden afgehandeld.
   • Ondersteuningsrelatie ($\Vdash_B^L$): De kern van de semantische definitie breidt de ondersteuningsrelatie uit naar ILL. Cruciaal is dat de clausule voor de exponentiële modaliteit !ϕ niet louter als een structurele regel wordt gedefinieerd, maar als een conditie op de validiteit van $\phi$ over basis-extensies heen. Specifiek geldt $\Vdash_B^L !\phi$ indien voor elke extensie $C$ van $B$, als $\phi$ een "stelling" is van $C$ (d.w.z. $\Vdash_D^\emptyset \phi$ voor alle $D \supseteq C$), dan de hulpbron gebruikt kan worden.
   • Behandeling van Modaliteit: Het artikel introduceert het concept van "persistente atomen" in de basis, die overeenkomen met formules van de vorm !ϕ. Deze atomen spelen een rol analoog aan het ! connectief in de afleidbaarheidsrelatie, waardoor de semantiek onderscheid kan maken tussen standaard aannames en aannames die kunnen worden verzwakt of gecontracteerd.

Belangrijkste Bijdragen

• Een Volledige B-eS voor ILL: Het artikel presenteert de eerste basis-extensie semantiek die de volledige Intuïtionistische Lineaire Logica dekt, inclusief additieve connectieven en de exponentiële modaliteit.
• Systematische Behandeling van Additiviteit: Door de introductie van additieve boxen biedt de auteur een methode om contextdeling en regels met variabele premissen te behandelen zonder ad-hoc zijvoorwaarden of expliciete context-metavariabelen. Dit biedt een schonere, meer uniforme representatie van inferentiefiguren.
• Modale Box Karakterisering: De herdefinitie van de promotie-regel met behulp van modale boxen biedt een structurele karakterisering van de exponentiële modaliteit die onafhankelijk is van de specifieke connectief-syntaxis, wat de integratie in het basis-extensie kader vergemakkelijkt.
• Inferentiële Rekening van !: Het artikel biedt een gedetailleerde discussie over de inferentiële inhoud van het ! connectief. Het beargumenteert dat de semantiek de modale aard van ! vangt door het te behandteren als een conditie op de validiteit van de onderliggende formule over basis-extensies heen, waardoor het aspect van "necessitatie" van de modaliteit effectief wordt geïnternaliseerd.
• Correctheid en Volledigheid: De auteur bewijst dat de voorgestelde semantiek zowel correct als volledig is ten opzichte van het natuurlijke deductie systeem NILL. Het volledigheidsbewijs behelst het construeren van een "simulatiebasis" $N$ waar atomaire regels de inferentie-regels van NILL nabootsen, en een plattekkingskaart die ILL formules naar atomen vertaalt.

Resultaten

• Theorema 2.7: Vestigt de equivalentie tussen de standaard sequent-stijl afleidbaarheid ($\vdash$) en de nieuwe box-gebaseerde afleidbaarheid ($\vdash^*$).
• Theorema 5.1 (Correctheid): Bewijst dat als een sequent bewijsbaar is in NILL, het geldig is in de voorgestelde semantiek ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$).
• Theorema 6.1 (Volledigheid): Bewijst dat als een sequent geldig is in de semantiek, het bewijsbaar is in NILL ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$).
• Theorema 4.15: Demonstreert dat de specifieke (Inf) clausule die wordt gebruikt voor het behandelen van hypothesen met ! equivalent is aan een algemenere (Gen-Inf) clausule, wat de specifieke behandeling van modale hypothesen valideert.
• Corollary 4.11 & 4.12: Vestigen structurele eigenschappen met betrekking tot de interactie van ! met de ondersteuningsrelatie, waarbij wordt aangetoond dat als $\phi$ geldig is, dan ook !ϕ geldig is, en dat !Γ !ϕ ondersteunt als het $\phi$ ondersteunt.

Significantie
Het artikel beweert een aanzienlijk gat in de bewijs-theoretische semantiek te vullen door de basis-extensie benadering uit te breiden van IPL en IMLL naar de volledige ILL. De auteur merkt op dat hoewel Gheorghiu, Gu, en Pym succesvol het multiplicatieve fragment hebben behandeld, de toevoeging van additieven en de exponentiële modaliteit aanzienlijke nieuwe mechanismen vereiste. Het werk is significant vanwege zijn intrinsieke bewijs-theoretische benadering van modaliteit, en biedt een manier om het "bang" connectief niet alleen als een structurele regel te begrijpen, maar als een conditie op de validiteit van formules binnen het basis-extensie kader. De auteur erkent bescheiden dat de oplossing voor het behandelen van de promotie-regel en additiviteit "enigszins gecompliceerd" is, maar noodzakelijk om een schone, systematische representatie van inferentiefiguren te bereiken. Verder benadrukt het artikel de moeilijkheid om Sandqvist's IPL semantiek direct in dit ILL framework in te bedden, wat de generalisatie van de mapping tussen de twee een open probleem laat voor toekomstig onderzoek. Het werk suggereert dat de huidige benadering van modaliteiten in P-tS diepe metafysische of structurele inzichten kan vereisen die pas net beginnen te worden geadresseerd.