Résumé Technique : Sémantique de l'Inférence-Comportement pour tous les connecteurs $\text{All}^*$ dans les calculs de séquents bidimensionnels

1. Énoncé du Problème

L'article traite d'un défi central de la Sémantique de l'Inférence (P-tS) : comment fournir des explications sémantiques invariantes par rapport au sens pour les connecteurs logiques à travers différents systèmes logiques (par exemple, les logiques classique, intuitionniste, linéaire et duale-intuitionniste). Les approches traditionnelles, telles que la Sémantique Modèle-Théorique (M-tS) et la Sémantique de l'Extension de Base (B-eS), souffrent souvent de « globalisme », où le changement de logique nécessite un changement du sens des connecteurs (par exemple, le « et » classique versus le « et » intuitionniste). Cela conduit à une situation où les désaccords logiques sont réduits à de simples ruptures de communication dues à des définitions divergentes, plutôt qu'à des désaccords substantiels sur des concepts partagés.

Le problème spécifique que cet article aborde est l'absence d'une mise en œuvre technique systématique de la Sémantique de l'Inférence-Comportement (I-bS), une approche récente proposée par Nagler [Nag26]. Bien que l'I-bS offre un cadre prometteur pour isoler le « comportement inférentiel minimal » d'un connecteur afin de définir son sens, elle manquait auparavant d'une évaluation technique complète à travers l'espace des règles de connecteurs possibles. L'article vise à valider l'I-bS en l'appliquant à un ensemble vaste et non structuré de connecteurs candidats pour déterminer lesquels, s'il y en a, possèdent des sens minimaux distincts indépendamment de règles structurelles spécifiques (comme l'affaiblissement ou la contraction).

2. Méthodologie

L'étude emploie une approche rigoureuse et pilotée par les données pour mesurer le « sens » des connecteurs sur la base de leur usage inférentiel dans un cadre minimal.

2.1 Objet d'enquête : $\text{All}^*$Connectives

Les auteurs définissent le champ d'investigation comme étant les $\text{All}^*$connecteurs : des paires de règles opérationnelles formulables dans des calculs de séquents bidimensionnels soumis aux contraintes suivantes :

• Règles Opérationnelles : Doivent être séparées, explicites et symétriques (Définition 3).
• Contraintes : Au plus deux séquents de prémisses et au plus deux formules actives par règle.
• Espace Total : Cela produit exactement 10 816 paires de règles syntaxiquement uniques (combinaisons de formes de prémisses et de positions de formules actives).

2.2 Environnement de Test : Relation de Dérivabilité Minimale

Pour isoler le sens d'un connecteur des caractéristiques structurelles de logiques spécifiques, les auteurs utilisent un calcul de fond minimal consistant en :

• Identité ($Id_{pr}$) : Restreinte aux formules primitives uniquement.
• Coupe ($Cut_{cd}$) : Une règle de Coupe différenciant le contexte.
• Hypothèses Structurelles : Le calcul suppose l'Échange (multisets) mais exclut l'Affaiblissement et la Contraction. Cela représente le « noyau de la logique sous-structurale » commun à de nombreuses logiques.

2.3 Dispositif de Mesure : Comportement d'Inférence

La métrique centrale est le comportement d'inférence, défini comme le motif syntaxique qu'un connecteur présente lors de la preuve de sa définissabilité au sein du calcul minimal.

• Critères de Définissabilité : Suivant Belnap [Bel62], un connecteur est définissable si son ajout au calcul résulte en une extension conservatrice (aucun nouveau théorème sans le connecteur) et une unicité (le connecteur est déterminé de manière unique à un isomorphisme près).
• Clause Sémantique : Le « sens » d'un connecteur est identifié comme sa paire de règles opérationnelles minimale qui produit le profil de comportement d'inférence minimal (la liste la plus courte de positions de composants occupées par le connecteur et ses formules actives lors d'une preuve de définissabilité).

2.4 Génération et Analyse des Données

Les auteurs filtrent systématiquement les 10 816 candidats :

1. Filtre 1 (Formulabilité) : Toutes les 10 816 paires de règles.
2. Filtre 2 (Conservativité) : Prouver l'élimination de la Coupe pour les cas positifs et construire des contre-exemples pour les cas non conservatifs. Cela réduit l'ensemble à 376 connecteurs conservatifs.
3. Filtre 3 (Unicité) : Établir l'interdérivabilité horizontale et verticale. Cela réduit encore l'ensemble à 150 connecteurs définissables de manière unique.
4. Analyse de Minimalité : Parmi les 150 connecteurs définissables, les auteurs distinguent les connecteurs « minimaux » des « bloatnectives » (connecteurs équivalents avec des redondances syntaxiques). En appliquant des critères de minimalité de type de prémisse (plus faible cardinalité de séquents de prémisses), ils isolent les clauses sémantiques véritablement minimales.

3. Contributions Clés et Résultats

3.1 Identification de 21 Connecteurs Minimalement Significatifs

Le résultat principal est l'identification de exactement 21 connecteurs minimalement significatifs. Ceux-ci correspondent à des constantes logiques familières et leurs converses/inverses, mais avec des distinctions précises entre les versions additives (lattice) et multiplicatives (groupe) :

• Nullaires : Bas ($\bot$) et Haut ($\top$).
• Unaires : Deux formes de négation (Intuitionniste $\neg$ et Duale-Intuitionniste $\sim$), et une négation converse « triviale ».
• Binaires :
  • Conjonction : Additive ($\sqcap$) et Multiplicative ($\otimes$).
  • Disjonction : Additive ($\sqcup$) et Multiplicative ($\oplus$).
  • Implication : Droite Additive ($\rightsquigarrow$), Droite Multiplicative ($\to$), Gauche Additive, et Gauche Multiplicative.
  • Converses et Inverses : Chacun des éléments ci-dessus possède des clauses sémantiques distinctes pour leurs converses (permutation des composants) et leurs inverses.

3.2 Clauses Sémantiques et Cadres

L'article fournit des clauses sémantiques explicites (paires de règles minimales) pour chacun des 21 connecteurs. Crucialement, il démontre que ces sens sont indépendants de la logique. Par exemple, la clause sémantique de la conjonction multiplicative ($\otimes$) est la même qu'elle apparaisse dans la Logique Linéaire, la Logique Classique ou la Logique Intuitionniste. Les différences dans la manière dont ces connecteurs se comportent dans les logiques complètes (par exemple, l'équivalence de $\otimes$ et $\sqcap$ dans la Logique Classique) sont attribuées aux ressources structurelles (comme la Contraction et l'Affaiblissement) plutôt qu'à un changement du sens central du connecteur.

3.3 Interrelations Sémantiques entre Logiques

L'étude cartographie la compatibilité sémantique de ces 21 connecteurs à travers diverses logiques :

• Logique Classique (LK) : Conflue les versions additives et multiplicatives de la conjonction, de la disjonction et de l'implication. Elle conflue également les deux formes de négation.
• Logique Intuitionniste (LJ) : Est compatible avec les versions additives de la conjonction et de la disjonction, ainsi qu'avec l'implication « droite », mais ne capture que la moitié du sens de la négation classique (spécifiquement $\neg_{min}$, excluant $\sim_{min}$).
• Logique Duale-Intuitionniste (LDJ) : Capture l'autre moitié de la négation classique ($\sim_{min}$) et les duales des autres connecteurs.
• Logique Linéaire (LL) : Distingue les 21 connecteurs, les traitant comme sémantiquement distincts.

3.4 Validation de l'I-bS

L'article affirme valider l'I-bS en démontrant que, lorsqu'elle est appliquée à une recherche aveugle et exhaustive de règles possibles sans biais vers une logique spécifique, la théorie converge naturellement vers exactement les connecteurs standards trouvés dans les systèmes logiques établis. Le fait que le « bruit » (les 10 795 autres paires de règles) est filtré comme non définissable ou non minimal sert de « test de cohérence » pour la théorie.

4. Signification et Revendications

L'article positionne ses conclusions comme une vérification du cadre de la Sémantique de l'Inférence-Comportement. Sa signification réside dans :

1. Indépendance de la Logique : Il fournit une méthode pour définir les sens des connecteurs qui sont invariants à travers différentes logiques. Changer la logique (par exemple, ajouter l'Affaiblissement) ne change pas le sens du connecteur ; cela change seulement le contexte structurel dans lequel le connecteur opère.
2. Résolution du Changement de Sens : Il offre une explication sémantique de la raison pour laquelle les logiques classique et intuitionniste semblent en désaccord. Elles ne sont pas nécessairement en désaccord sur le sens de « et » ou de « ou » ; elles diffèrent plutôt sur quels connecteurs minimaux elles permettent d'interagir et quelles règles structurelles elles autorisent. Par exemple, le « et » classique est une conflation de deux sens minimaux distincts ($\otimes$ et $\sqcap$), tandis que le « et » intuitionniste est strictement $\sqcap$.
3. Frugalité Ontologique : L'approche ne nécessite aucun modèle ou base externe, s'appuyant uniquement sur le noyau sous-structural du système de preuve.
4. Exhaustivité : En couvrant l'intégralité de l'espace des règles formulables sous les contraintes données, l'article affirme avoir fourni une taxonomie complète des sens de connecteurs minimaux dans les calculs de séquents bidimensionnels.

Les auteurs restent modestes quant à la portée de l'étude, notant que les résultats sont relatifs aux contraintes spécifiques (deux prémisses, deux formules actives, calcul minimal spécifique) et que des travaux futurs pourraient explorer les calculs multidimensionnels, la quantification ou des relations de dérivabilité minimale alternatives. Cependant, dans le cadre défini, l'article affirme que l'I-bS réussit à isoler les sens primitifs des connecteurs logiques.