💻 computer science

Hyperformalism for Relevant Modal Logics

Cet article étend le concept d'hyperformalisme aux logiques modales pertinentes en introduisant l'MPos-hyperformalisme, en prouvant que la logique faible B-Box possède cette propriété, en étudiant sa clôture sous des substitutions non uniformes spécifiques, en affinant la propriété de partage de variables, et en définissant K-MPos comme le sous-logic MPos-hyperformel le plus grand de la logique modale classique K.

Auteurs originaux : Thomas Macaulay Ferguson (Rensselaer Polytechnic Institute), Shay Allen Logan (Kansas State University)

Publié 2026-07-01

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Thomas Macaulay Ferguson (Rensselaer Polytechnic Institute), Shay Allen Logan (Kansas State University)

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 vous êtes un bibliothécaire strict dans une bibliothèque de la logique. Dans cette bibliothèque, chaque livre (ou formule) est composé de phrases construites à partir de blocs de base appelés « atomes » (comme $p$ , $q$ , $r$ ).

L'ancienne méthode : La règle uniforme

Traditionnellement, les bibliothécaires suivaient une règle simple : la Substitution Uniforme.
Si un livre dit : « S'il se passe $p$ , alors $p$ se passe de nouveau », et que vous décidez de remplacer la lettre $p$ par le mot « Pluie », vous devez remplacer chaque occurrence de $p$ par « Pluie ».

Avant : S'il pleut, il pleut.
Après : S'il pleut, il pleut.
Vous ne pouvez pas changer un seul $p$ en « Pluie » et l'autre en « Neige ». Ils sont traités comme étant exactement la même chose, partout.

La nouvelle idée : L'hyperformalisme

Les auteurs de cet article introduisent une façon beaucoup plus flexible, une façon « hyper », d'organiser la bibliothèque appelée Hyperformalisme.

Imaginez un bibliothécaire spécial qui observe où un mot apparaît dans une phrase. Ils réalisent que deux occurrences de la même lettre peuvent en réalité accomplir des tâches différentes selon leur emplacement.

L'analogie : Pensez à un mot apparaissant dans une phrase comme une personne portant un chapeau différent selon l'endroit où elle se tient dans une pièce.
- Si $p$ se tient seul, il porte un « Chapeau Rouge ».
- Si $p$ se tient à l'intérieur d'une boîte (un énoncé conditionnel du type « Si... alors... »), il porte un « Chapeau Bleu ».
- Si $p$ se tient à l'intérieur d'une boîte, elle-même à l'intérieur d'une autre boîte, il porte un « Chapeau Vert ».

Dans une logique Hyperformale, le bibliothécaire dit : « Parce que le $p$ au Chapeau Rouge est à un endroit différent du $p$ au Chapeau Vert, ils sont en fait des personnes différentes ». Vous pouvez remplacer le $p$ au Chapeau Rouge par « Pluie » et le $p$ au Chapeau Vert par « Neige » sans enfreindre les règles de la bibliothèque.

Cet approche fonctionne extrêmement bien pour les Logiques Rélevantes (les logiques qui exigent que la partie « si » d'une phrase ait un rapport réel avec la partie « alors »).

Ajouter la « Boîte » (Logique Modale)

L'article pousse cette idée plus loin en ajoutant la Logique Modale (la logique de la « nécessité » ou de la « possibilité », représentée par le symbole de la boîte $\square$ ).

Dans la logique standard, $\square p$ signifie « Il est nécessaire que $p$ ».
Les auteurs se demandent : « Le système des "chapeaux" fonctionne-t-il lorsque nous avons ces boîtes ? »

Ils définissent un nouveau système appelé MPos-hyperformalisme. Ici, le « chapeau » (ou la position) d'une lettre dépend de :

Le nombre de boîtes à l'intérieur desquelles elle se trouve.
Qu'elle soit du côté gauche ou droit d'un énoncé « Si/Alors ».
Qu'elle soit niée (à l'intérieur d'un « Non »).

La grande découverte (Théorème 2.1) :
Les auteurs prouvent qu'une logique très spécifique et très faible appelée $B_\square$ est « MPos-hyperformale ».

Ce que cela signifie : Dans cette logique, vous pouvez traiter chaque occurrence d'une lettre comme un individu unique basé sur son emplacement exact dans la structure de la phrase. Si une phrase est un théorème valide, elle restera valide même si vous remplacez différentes occurrences de la même lettre par des mots complètement différents, tant que vous respectez leurs « chapeaux » (positions).

La règle du « Partage de Variables »

Les logiques rélevantes ont une règle d'or : le Partage de Variables.

La Règle : Dans un énoncé valide de type « Si $A$ , alors $B$ », $A$ et $B$ doivent partager au moins un ingrédient commun (une variable). Vous ne pouvez pas dire « Si la lune est faite de fromage, alors je suis une pomme de terre » car ils ne partagent rien.
Le Twist : Grâce au système des « chapeaux », les auteurs ont découvert que l'ingrédient partagé doit porter le même type de chapeau.
- Si $p$ est partagé, il doit porter le même nombre de boîtes dans la partie « Si » et dans la partie « Alors ».
- Cela crée une version très stricte et précise de la rélevance.

Le « Grand Champion » de la logique : $K_{MPos}$

L'article introduit également une nouvelle logique appelée $K_{MPos}$ .

Considérez $K$ comme la bibliothèque « Classique », qui est immense et autorise presque tout.
Les auteurs se sont demandé : « Quel est le plus grand possible segment de la bibliothèque Classique qui suit toujours nos règles de "Chapeau" (Hyperformalisme) ? »
Ils l'ont trouvé : $K_{MPos}$ .

Pourquoi $K_{MPos}$ est-elle spéciale ?

C'est la plus grande : Elle contient tous les énoncés possibles qui respectent les règles du « Chapeau ».
Elle est sûre : Contrairement à certaines autres logiques « rélevantes » qui ne sont que de la logique classique sur laquelle on a plaqué un « tamis » (un filtre), $K_{MPos}$ est construite de fond en comble pour être cohérente.
Elle ne casse pas : Les auteurs prouvent que cette logique est transitive.
- Analogie : Si « Si A alors B » est vrai, et que « Si B alors C » est vrai, alors « Si A alors C » est certainement vrai. Certaines logiques « rélevantes » bizarres brisent cette chaîne, mais $K_{MPos}$ la maintient intacte.

Conclusion des auteurs

Les auteurs disent essentiellement :
« Nous avons montré que l'approche des "différents chapeaux" (MPos-hyperformalisme) fonctionne parfaitement pour les logiques rélevantes faibles comme $B_\square$ . Mais si vous voulez la logique la plus forte et la plus robuste qui respecte toujours ces règles, ne vous contentez pas de $B_\square$ . Tournez-vous vers $K_{MPos}$ ».

Ils mettent au défi les autres logiciens : « Si vous préférez les anciennes logiques plus faibles, vous devez nous donner une bonne raison. Si votre raison ne concerne pas le "partage de variables" ou la "classicité", alors vous passez peut-être à côté de la supériorité de $K_{MPos}$ ».

En bref : L'article construit un nouveau système hautement organisé pour la logique où l'emplacement d'un mot détermine son identité, prouve que ce système fonctionne pour certains types de logiques, puis trouve la version « ultime » de ce système qui est plus forte et plus fiable que les tentatives précédentes.

Résumé Technique : Hyperformalisme pour les Logiques Modales Relevant

Problème et Contexte
L'article traite de l'analyse des logiques de la pertinence (relevant logics) à travers le prisme de l'hyperformalisme, une propriété par laquelle une logique reste fermée sous les substitutions non uniformes. Dans les logiques formelles standards, les formules atomiques sont traitées comme indépendantes via la substitution uniforme. L'hyperformalisme étend cette indépendance, permettant de traiter des occurrences distinctes d'un même atome comme indépendantes si elles apparaissent dans des contextes syntaxiques suffisamment différents (par exemple, à des « profondeurs » différentes ou sous différents opérateurs modaux). L'hyperformalisme a été appliqué avec succès aux logiques de la pertinence non modales (telles que $B$ et $DR$), révélant de fortes propriétés de partage de variables et identifiant de nouvelles logiques de la pertinence ; toutefois, son application aux logiques modales de la pertinence demeure peu explorée. Les auteurs cherchent à étendre ces techniques au cadre modal, en investiguant spécifiquement comment la présence de l'opérateur modal $\square$ interagit avec les substitutions non uniformes et le partage de variables.

Méthodologie
Les auteurs emploient une combinaison de techniques de preuve et de sémantique pour analyser les logiques modales de la pertinence :

Cadre Syntactique (MPos) : Les auteurs définissent un ensemble de positions, $MPos = \{l, r, n, b\}^*c$ , où $l$ et $r$ désignent les branches gauche et droite des conditionnels, $n$ désigne la négation, et $b$ désigne la portée de l'opérateur modal $\square$ .
Substitutions : Ils définissent les substitutions MPos comme des fonctions $\sigma: MPos \times At \to L$ qui respectent la structure des formules. Crucialement, ces substitutions traitent les atomes à différentes positions comme indépendants, sous réserve de contraintes de « fidélité » spécifiques (par exemple, $\sigma_{xnn}(p) = \sigma_x(p)$ pour préserver les propriétés de la double négation).
Analyse Prouvante : L'article analyse la logique modale de la pertinence de base $B^\square$ (formée en ajoutant les axiomes $C$ et la règle $RM$ à la logique de la pertinence $B$ ). Il prouve la clôture sous les substitutions MPos par induction sur les dérivations.
Extensions : Les auteurs définissent des relations d'équivalence sur $MPos$ correspondant aux axiomes modaux $T, 4, K,$ et $RN$. Ils étudient les logiques résultantes $B^\square_S$ et leur clôture sous les correspondantes $MPos_S$ -substitutions.
Caractérisation Sémantique : Pour caractériser la plus grande sous-logique hyperformale de la logique modale classique $K$ $K$ (notée $KMPos$), les auteurs introduisent :
- Assignations MPosK : Des fonctions $\alpha: Mpos \times W \times At \to \{0, 1\}$ sur des cadres de Kripke, où les valeurs de vérité varient selon l'indice de position.
- Tableaux Analytiques : Un système de tableaux avec des nœuds $\langle x, \omega, A, i \rangle$ suivant les positions ( $x$ ), les mondes ( $\omega$ ), les formules ( $A$ ) et les valeurs de vérité ( $i$ ).
Modèles Canoniques : La complétude est établie via la construction d'ensembles de branches maximaux, témoins et cohérents avec le tableau, ainsi que leurs modèles canoniques correspondants.

Contributions Clés et Résultats

Hyperformalisme MPos de $B^\square$ :
- Théorème 2.1 : La logique de base $B^\square$ est prouvée être MPos-hyperformale. La preuve démontre que les axiomes ( $C$ ) et les règles ($RM$) du système préservent la démontrabilité sous les substitutions MPos.
- Partage de Variables : En conséquence, $B^\square$ satisfait la propriété de partage de variables MPos. Si $A \to B$ est un théorème, il existe une variable partagée $p$ telle que la position de $p$ dans $A$ et $B$ est équivalente sous la relation $\sim_{nn}$ (différant seulement par des paires de négations).
- Corollaire 2.6 : Une conséquence spécifique est que tout théorème $A \to B$ dans $B^\square$ partage une variable imbriquée dans le même nombre d'opérateurs $\square$ dans l'antécédent et le conséquent.
Extensions de $B^\square$ :
- Théorème 2.7 : Pour tout sous-ensemble $S \subseteq \{T, 4, K, RN\}$ , la logique $B^\square_S$ est $MPos_S$ -hyperformale, où $MPos_S$ incorpore des relations d'équivalence reflétant les axiomes modaux spécifiques (par exemple, $xby \sim_4 xbby$ pour l'axiome 4).
- Partage de Variables Affiné : Ces extensions produisent des propriétés de partage de variables affinées. Par exemple, dans $B^\square_{\{4\}}$ , les variables partagées doivent avoir le même « mode » (extensionnel ou intensionnel), éliminant de fait le décompte des opérateurs $\square$ de la condition de partage.
Caractérisation de $KMPos$ :
- Les auteurs définissent $KMPos$ comme la plus grande sous-logique hyperformale de la logique modale classique $K$ .
- Caractérisation Sémantique : $KMPos$ est caractérisée par la validité dans des cadres de Kripke équipés d'assignations MPosK.
- Caractérisation par Tableau : Un système de tableau sain et complet est fourni pour $KMPos$.
- Théorème 3.6 : $KMPos$ est équivalente à l'ensemble des formules $A$ telles que pour une certaine substitution injective-jusqu'à-fidélité $\iota$ , $\iota(A)$ est un théorème de $K$ . Cela confirme que $KMPos$ est le sous-ensemble maximal de $K$ clos sous les substitutions MPos.
- Partage de Variables : Le Théorème 3.9 établit que $KMPos$ possède la propriété de partage de variables.
Transitivité et Nature de $KMPos$ :
- Théorème 4.1 : $KMPos$ est transitive. Les auteurs soutiennent qu'à la différence des approches de type « tamis syntaxique » (syntactic sieve) de la pertinence (qui échouent souvent à la transitivité), $KMPos$ évite de telles pathologies car elle est définie par une propriété de clôture plutôt que par un filtre statique sur les théorèmes classiques.

Signification et Revendications
L'article affirme que l'hyperformalisme est un outil puissant pour analyser les logiques modales de la pertinence, capable de révéler de fortes propriétés de partage de variables même dans des systèmes faibles comme $B^\square$ . Cependant, les auteurs soutiennent que $B^\square$ n'est pas la logique la plus forte possédant ces caractéristiques.

La signification primaire réside dans l'introduction et la caractérisation de $KMPos$. Les auteurs posent que $KMPos$ représente la « plus grande » logique modale de la pertinence en ce sens qu'elle est la sous-logique maximale de la logique classique $K$ qui est close sous les substitutions MPos. Ils affirment que $KMPos$ offre des avantages sémantiques et prouvants par rapport à $B^\square$ et aux autres logiques modales de la pertinence traditionnelles. Plus précisément, ils soutiennent que $KMPos$ n'est pas simplement un « tamis syntaxique » (terme péjoratif pour les logiques définies par le simple filtrage des théorèmes classiques) car elle est transitive et définie par une propriété de clôture robuste.

L'article conclut en contestant la préférence pour les logiques modales de la pertinence « traditionnelles » (comme $B^\square$ ) au profit de $KMPos$. Les auteurs suggèrent que, sauf raisons spécifiques de préférer les premières, les chercheurs devraient considérer $KMPos$, car elle conserve les caractéristiques désirables de partage de variables tout en étant une sous-logique maximale de la logique classique $K$ . L'article reconnaît qu'une caractérisation axiomatique de $KMPos$ demeure un problème ouvert, notant que de telles logiques ont historiquement résisté à l'axiomatisation récursive.