💻 computer science

A Proof-Theoretic Approach to the Semantics of Classical Linear Logic

Cet article propose une approche proof-théorique de la sémantique du fragment multiplicatif-additif de la logique linéaire classique en étendant la sémantique par extension de base (BeS) pour caractériser les preuves via la notion de support de base.

Auteurs originaux : Victor Barroso-Nascimento, Ekaterina Piotrovskaya, Elaine Pimentel

Publié 2026-03-03

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Victor Barroso-Nascimento, Ekaterina Piotrovskaya, Elaine Pimentel

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que la logique est comme un grand supermarché où les idées sont des produits.

Dans la logique classique (celle qu'on apprend à l'école), si vous prenez une pomme, vous pouvez la copier à l'infini ou la jeter sans problème. C'est comme si les produits étaient magiques : vous pouvez en avoir autant que vous voulez ou les oublier.

Mais dans la Logique Linéaire, c'est différent. Ici, chaque produit est une ressource précieuse. Si vous prenez une pomme pour faire un gâteau, elle est consommée. Vous ne pouvez pas la copier, ni la jeter. Elle doit être utilisée exactement une fois. C'est comme cuisiner avec des ingrédients réels : si vous utilisez un œuf, il n'est plus dans le frigo.

Le Problème : Comment donner du sens à ces règles ?

Les mathématiciens ont deux façons habituelles d'expliquer comment fonctionne ce supermarché logique :

La méthode "Carte au trésor" (Sémantique modèle) : On regarde si une phrase est vraie ou fausse dans un monde imaginaire.
La méthode "Preuve" (Sémantique de la preuve) : On regarde si l'on peut construire une preuve solide, étape par étape, pour arriver à la conclusion.

Ce papier propose une nouvelle façon de voir les choses, appelée Sémantique par Extension de Base (BeS).

L'Analogie de la "Boîte à Outils" (La Base)

Imaginez que vous avez une boîte à outils (ce qu'ils appellent une "Base"). Cette boîte contient des règles de base pour des objets simples (comme "il pleut", "je suis à Londres").

Dans la logique classique, pour dire qu'une phrase complexe est "vraie", on ne regarde pas si elle est vraie dans un monde imaginaire. On demande : "Si j'utilise cette phrase comme outil dans ma boîte, est-ce que je peux construire une preuve de l'absurde (une contradiction) ?"

C'est un peu comme un jeu de détective :

Si vous avez une hypothèse (par exemple, "Il pleut"), vous la mettez dans votre boîte.
Ensuite, vous essayez de voir si, en utilisant cette hypothèse, vous pouvez prouver que "tout est faux" (une contradiction).
Si vous y arrivez, cela signifie que votre hypothèse est solide et valide dans ce système.

La Grande Révolution de ce Papier

Jusqu'à présent, cette méthode fonctionnait très bien pour la logique "intuitionniste" (qui est très stricte et constructive, comme un artisan qui ne fait rien sans preuve). Mais pour la Logique Linéaire Classique (qui permet de dire "non" et de faire des raisonnements par l'absurde), c'était très difficile à expliquer avec cette méthode.

Les auteurs de ce papier ont trouvé une astuce géniale, simple comme bonjour :

Ils ont dit : "Pour passer de la logique constructive à la logique classique, il suffit de changer une seule petite règle."

Au lieu de demander : "Peut-on prouver n'importe quelle phrase atomique ?"
Ils demandent : "Peut-on prouver l'absurde (le symbole ⊥) ?"

C'est comme si, dans le jeu de construction, au lieu de demander "Peux-tu construire une tour ?", on demandait "Peux-tu faire s'effondrer la tour ?". Si vous pouvez prouver que tout s'effondre grâce à une hypothèse, alors cette hypothèse est validée dans le monde classique.

Pourquoi est-ce important ?

C'est plus simple : Au lieu de créer des règles compliquées pour chaque type de logique, ils montrent que la logique classique n'est qu'une version "restreinte" de la logique constructive. C'est comme si la logique classique était un jeu où l'on a moins d'informations à fournir pour gagner.
C'est un pont : Cela aide à comprendre que la différence entre "prouver quelque chose" (constructif) et "prouver que le contraire est faux" (classique) n'est pas une différence de nature, mais de quantité d'information. La logique classique demande moins d'effort pour prouver quelque chose, mais elle est tout aussi valide.
Pour l'informatique : La logique linéaire est utilisée pour gérer les ressources dans les ordinateurs (mémoire, processeur). Comprendre comment ces règles fonctionnent aide à créer des logiciels plus sûrs et plus efficaces.

En résumé

Ce papier dit essentiellement : "Ne vous inquiétez pas, la logique classique n'est pas un monstre étranger. C'est juste la logique linéaire habituelle, mais avec une petite astuce : on ne cherche plus à prouver que quelque chose est 'vrai', on cherche à prouver que son contraire mène à une catastrophe (une contradiction). Et cette petite astuce suffit à tout expliquer !".

C'est une belle démonstration que parfois, pour comprendre un système complexe, il suffit de changer légèrement la question que l'on se pose.

1. Problématique et Contexte

La logique linéaire (LL) est un système logique sensible aux ressources, raffinant la logique classique et intuitionniste en interdisant la copie et l'effacement arbitraires des formules (sauf via les modales exponentielles). La sémantique de la LL est traditionnellement présentée de deux manières :

Sémantique de modèle (ex. : sémantique de phases, espaces de cohérence) : associe des formules à des ensembles de contextes ou attribue du sens directement aux preuves.
Sémantique par la théorie de la preuve (Proof-Theoretic Semantics - PtS) : définit la signification des opérateurs logiques par leurs règles d'inférence.

Le défi majeur abordé dans cet article est l'extension de la Sémantique par Extension de Base (Base-Extension Semantics - BeS) au cas classique de la logique linéaire (MALL : Multiplicative-Additive Linear Logic).

La BeS, développée initialement pour la logique intuitionniste (par Sandqvist), définit la validité d'une formule par rapport à une « base » (un ensemble de règles atomiques).
Dans les systèmes classiques, la notion de vérité bivalente pose problème en PtS. De plus, la logique linéaire introduit une complexité structurelle (multisets au lieu d'ensembles) et des connectifs classiques (comme le par ` et le zéro 0) qui ne se prêtent pas facilement aux définitions intuitionnistes standards.
L'objectif est de fournir une sémantique purement déductive pour MALL, évitant les modèles externes, tout en gérant la négation classique et la structure des ressources.

2. Méthodologie

Les auteurs adoptent une approche de sémantique par extension de base (BeS) adaptée aux systèmes sous-structuraux classiques. La méthodologie repose sur les piliers suivants :

Le concept de Base (Base) : Une base $\mathcal{B}$ est un ensemble de règles d'inférence portant uniquement sur des formules atomiques (et le constant $\bot$ ). Contrairement aux approches antérieures, les règles sont fixées dans un style de calcul des séquents (avec des contextes explicites) et incluent $\bot$ comme un atome manipulable.
La relation de Support ( $\Vdash$ ) : La validité d'une formule $\phi$ n'est pas définie par la vérité dans un modèle, mais par le fait qu'elle est « supportée » par une base. La relation $\Gamma \Vdash_{\mathcal{B}} \phi$ est définie inductivement.
L'approche par la réfutabilité (Falsity) : Pour capturer la nature classique, les auteurs ne définissent pas $\bot$ comme « jamais valide ». Au lieu de cela, ils traitent $\bot$ comme un atome fixe. La clause pour les atomes $p$ est reformulée : $p$ est supportée si, pour toute extension de la base, toute déduction de $\bot$ à partir de $p$ implique une déduction de $\bot$ à partir du contexte de support.
Restriction Uniforme : La contribution centrale est l'observation que les conditions de preuve classiques peuvent être obtenues à partir des conditions intuitionnistes par une restriction uniforme : au lieu de demander la dérivabilité d'une proposition atomique arbitraire $p$ $p$ , on exige systématiquement la construction d'une preuve de $\bot$ $⊥$ (le faux).
- Exemple pour le tensoriel ( $\otimes$ ) :
  - Intuitionniste : $\Vdash \phi \otimes \psi$ si pour tout contexte, si $\phi, \psi \Vdash p$ alors $\dots \Vdash p$ .
  - Classique (MALL) : $\Vdash \phi \otimes \psi$ si pour tout contexte, si $\phi, \psi \Vdash \bot$ alors $\dots \Vdash \bot$ .

3. Contributions Clés

Première sémantique BeS pour les systèmes sous-structuraux classiques : L'article présente la première définition complète de la sémantique BeS pour le fragment multiplicatif-additif de la logique linéaire classique (MALL).
Caractérisation de la preuve classique par restriction : Les auteurs démontrent que la sémantique classique de MALL peut être vue comme une restriction simple et uniforme de la sémantique intuitionniste, où la cible de la réfutation est toujours $\bot$ . Cela clarifie le lien entre vérité classique et conditions de preuve constructive.
Traitement des connectifs classiques : La définition gère élégamment les connectifs problématiques de la LL classique, notamment le par (`) et le zéro (0), en utilisant la structure des règles d'introduction et d'élimination adaptées à la logique linéaire.
Base de simulation (Simulation Base) : Pour la preuve de complétude, les auteurs construisent une base de simulation spécifique qui mappé chaque sous-formule à un atome unique, permettant de simuler les règles de déduction naturelle de MALL au sein du système atomique.

4. Résultats Principaux

Les auteurs établissent deux théorèmes fondamentaux prouvant la robustesse de leur cadre sémantique :

Théorème de Correction (Soundness) : Si une formule est dérivable dans le système de déduction naturelle de MALL ( $\Gamma \vdash_{MALL} \phi$ ), alors elle est valide selon la sémantique BeS proposée ( $\Gamma \Vdash \phi$ ). La preuve repose sur une réductio ad absurdum sémantique et montre que chaque règle d'inférence préserve la relation de support.
Théorème de Complétude : Si une formule est valide selon la sémantique BeS ( $\Gamma \Vdash \phi$ $Γ ⊩ ϕ$ ), alors elle est dérivable dans MALL ( $\Gamma \vdash_{MALL} \phi$ $Γ ⊢_{M A LL} ϕ$ ).
- La preuve utilise une base de simulation $U$ construite à partir d'une application atomique injective. Elle montre que si $\Gamma \Vdash \phi$ , alors dans cette base spécifique, les atomes correspondant aux formules permettent de reconstruire une dérivation formelle de $\Gamma \vdash \phi$ .
Corollaire de Normalisation Sémantique : Un résultat surprenant est que la complétude peut être prouvée sans utiliser de procédures de réduction syntaxique complexes. Cela implique l'existence d'une dérivation où les applications des règles d'élimination ( $\otimes E, \oplus E, 0 E, ` E$ ) ont des prémisses mineures de forme $\bot$ . Cela offre une nouvelle perspective sur la normalisation des preuves classiques.

5. Signification et Implications

Nature de la Preuve Classique : L'article soutient l'idée que la preuve classique n'est pas fondamentalement différente de la preuve constructive, mais en est une restriction quantitative. La preuve classique exige moins d'informations (elle se contente de prouver l'incohérence $\bot$ plutôt que de construire un objet spécifique), ce qui explique pourquoi l'extraction algorithmique de preuves classiques est possible mais affaiblie.
Unification Logique : La démonstration que les conditions de preuve pour la conjonction ( $\&$ ) sont identiques en logique classique et intuitionniste (contrairement aux connectifs multiplicatifs) renforce les thèses de l'« écumenisme logique ».
Futur de la Recherche : Bien que l'article se concentre sur MALL, les auteurs suggèrent que leur méthode est généralisable aux modales exponentielles ( $!$ et $?$ ) de la logique linéaire complète. Ils proposent des clauses sémantiques conjecturales pour ces modales, ouvrant la voie à une sémantique BeS complète pour la logique linéaire classique.

En résumé, cet article réussit à ancrer la logique linéaire classique dans un cadre sémantique purement déductif, démontrant que la complexité des systèmes classiques peut être maîtrisée par une restriction élégante des conditions de preuve intuitionnistes, sans recourir à des modèles externes.