A Proof-theoretic Semantics for Intuitionistic Linear Logic

Problème
La sémantique de type théorique de la preuve (P-tS) vise à conférer un sens aux expressions logiques à travers la notion de preuve plutôt que de vérité. Alors que Sandqvist a établi avec succès une sémantique de base-extension (B-eS) pour la logique propositionnelle intuitionniste (LPI), et que Gheorghiu, Gu et Pym ont étendu cela au fragment multiplicatif de la logique linéaire intuitionniste (ILL), une P-tS complète pour l'ILL entière est restée insaisissable. Le défi principal réside dans la nature substructurelle de l'ILL, qui interdit la faiblesse et la contraction générales, ainsi que dans son inclusion des connecteurs additifs et de la modalité exponentielle (!). Les approches existantes peinent à gérer l'interaction entre ces caractéristiques au sein d'un cadre de base-extension. Plus précisément, définir une relation de support qui respecte la nature sensible aux ressources de l'ILL tout en capturant correctement le contenu inférentiel du connecteur « bang » (!) — un opérateur modal exigeant des dérivations strictes — présente des difficultés significatives. De plus, les systèmes de déduction naturelle standards pour l'ILL reposent souvent sur des conditions de côté ad hoc concernant le partage de contexte (additivité) et le nombre de prémisses, qui sont difficiles à formaliser dans la structure rigide et non schématique requise pour les règles atomiques dans la B-eS.

Méthodologie
L'article propose une nouvelle sémantique de base-extension pour l'ILL en abordant deux obstacles techniques majeurs : la formalisation des règles de déduction naturelle sans métavariables de contexte schématiques, et la définition d'une relation de support qui gère l'additivité et la modalité.

1. Reformulation de la déduction naturelle : L'auteur introduit une nouvelle syntaxe pour le système de déduction naturelle NILL utilisant des « boîtes additives » (notées par des accolades {...}) et des « boîtes modales » (notées par des crochets sémantiques J...K).

   • Boîtes additives : Elles délimitent les contextes partagés, permettant au système de représenter les connecteurs additifs (comme & et ⊕) et les règles avec des prémisses variables (comme ⊤I et 0E) sans dépendre de métavariables de contexte arbitraires. Cela permet un traitement systématique de l'additivité où les dérivations à l'intérieur d'une boîte partagent le même multiset d'hypothèses ouvertes.
   • Boîtes modales : Elles sont utilisées pour caractériser la règle de Promotion (Prom). La règle est redéfinie pour exiger que la conclusion découle d'un contexte où toutes les hypothèses sont des conclusions de règles contenant uniquement des boîtes modales au-dessus d'elles. Cela capture l'exigence de dérivation stricte de la modalité exponentielle sans faire explicitement référence au connecteur ! dans la définition structurelle de la règle.
   • L'auteur prouve que ce nouveau système est équivalent au NILL standard de style séquentiel (Théorème 2.7).

2. Dérivabilité atomique et relation de support :

   • Règles atomiques : La sémantique définit les règles atomiques comme des triplets consistant en un multiset de boîtes additives, une boîte additive unique (la conclusion), et un atome. Cela reflète la structure des règles de déduction naturelle reformulées.
   • Extension de base : Une base $B$ est un ensemble de telles règles atomiques. La relation de dérivabilité $\vdash_B$ est définie de manière inductive, gérant la division multiplicative des contextes et le partage additif via la structure des boîtes.
   • Relation de support ($\Vdash_B^L$) : La définition sémantique centrale étend la relation de support à l'ILL. Crucialement, la clause pour la modalité exponentielle !ϕ est définie non pas simplement comme une règle structurelle, mais comme une condition sur la validité de $\phi$ à travers les extensions de base. Spécifiquement, $\Vdash_B^L !\phi$ est vrai si, pour toute extension $C$ de $B$, si $\phi$ est un « théorème » de $C$ (c'est-à-dire $\Vdash_D^\emptyset \phi$ pour tout $D \supseteq C$), alors la ressource peut être utilisée.
   • Gestion de la modalité : Le papier introduit le concept d'« atomes persistants » dans la base, qui correspondent à des formules de la forme !ϕ. Ces atomes jouent un rôle analogue au connecteur ! dans la relation de dérivabilité, permettant à la sémantique de distinguer les hypothèses standards de celles qui peuvent être affaiblies ou contractées.

Contributions clés

• Une B-eS complète pour l'ILL : Le papier présente la première sémantique de base-extension couvrant l'intégralité de la logique linéaire intuitionniste, incluant les connecteurs additifs et la modalité exponentielle.
• Traitement systématique de l'additivité : En introduisant les boîtes additives, l'auteur fournit une méthode pour gérer le partage de contexte et les règles à prémisses variables dans la déduction naturelle sans conditions de côté ad hoc ou métavariables de contexte explicites. Cela offre une représentation plus propre et plus uniforme des figures d'inférence.
• Caractérisation par boîte modale : La redéfinition de la règle de Promotion à l'aide de boîtes modales fournit une caractérisation structurelle de la modalité exponentielle qui est indépendante de la syntaxe spécifique du connecteur, facilitant son intégration dans le cadre de base-extension.
• Compte inférential de ! : Le papier propose une discussion détaillée sur le contenu inférentiel du connecteur !. Il soutient que la sémantique capture la nature modale de ! en le traitant comme une condition sur la validité de la formule sous-jacente à travers les extensions de base, internalisant efficacement l'aspect de « nécessitation » de la modalité.
• Correction et complétude : L'auteur prouve que la sémantique proposée est à la fois correcte et complète par rapport au système de déduction naturelle NILL. La preuve de complétude implique la construction d'une « base de simulation » $N$ où les règles atomiques miment les règles d'inférence de NILL, et une application d'aplatissement qui traduit les formules ILL en atomes.

Résultats

• Théorème 2.7 : Établit l'équivalence entre la dérivabilité de style séquentiel standard ($\vdash$) et la nouvelle dérivabilité basée sur les boîtes ($\vdash^*$).
• Théorème 5.1 (Correction) : Prouve que si un séquent est prouvable dans NILL, il est valide dans la sémantique proposée ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$).
• Théorème 6.1 (Complétude) : Prouve que si un séquent est valide dans la sémantique, il est prouvable dans NILL ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$).
• Théorème 4.15 : Démontre que la clause (Inf) spécifique utilisée pour traiter les hypothèses avec ! est équivalente à une clause (Gen-Inf) plus générale, validant le traitement spécifique des hypothèses modales.
• Corollaire 4.11 & 4.12 : Établissent des propriétés structurelles concernant l'interaction de ! avec la relation de support, montrant que si $\phi$ est valide, alors !ϕ est valide, et que !Γ supporte !ϕ s'il supporte $\phi$.

Signification
Le papier affirme combler une lacune importante dans la sémantique de type théorique de la preuve en étendant l'approche de base-extension de la LPI et de l'IMLL vers l'ILL complète. L'auteur note que bien que Gheorghiu, Gu et Pym aient réussi à gérer le fragment multiplicatif, l'ajout des additifs et de la modalité exponentielle a nécessité de nouveaux mécanismes substantiels. Le travail est significatif par son approche intrinsèquement théorique de la preuve de la modalité, offrant un moyen de comprendre le connecteur « bang » non seulement comme une règle structurelle, mais comme une condition sur la validité des formules au sein du cadre de base-extension. L'auteur reconnaît modestement que la solution pour gérer la règle de promotion et l'additivité est « quelque peu alambiquée » mais nécessaire pour parvenir à une représentation propre et systématique des figures d'inférence. De plus, le papier souligne la difficulté d'imbriquer directement la sémantique de Sandqvist pour la LPI dans ce cadre d'ILL, laissant la généralisation de la mise en correspondance entre les deux comme un problème ouvert pour des études futures. Le travail suggère que l'approche actuelle des modalités en P-tS peut nécessiter des intuitions métaphysiques ou structurelles profondes qui commencent à peine à être abordées.