A General Theory of Propositional Modal Bundled Modalities

1. Problématique

Les modalités groupées (bundled modalities) consistent à encoder un concept complexe (comme « quelqu'un sait », « désaccord dans un groupe » ou « croyance sans connaissance ») dans la sémantique d'un seul opérateur modal. Bien qu'il existe une littérature substantielle sur des opérateurs concrets spécifiques (ex. : la non-contingence $\Delta\phi$, la fausse croyance, etc.), il manque une théorie unifiée pour comprendre leur expressivité et leur axiomatisation.

Les défis majeurs identifiés par les auteurs sont :

• L'absence d'une méthode uniforme pour définir les bisimulations adaptées à ces opérateurs, ce qui rend souvent l'étude de leur expressivité difficile.
• L'absence d'une approche systématique pour l'axiomatisation (complétude) de ces logiques, obligeant les chercheurs à développer des modèles canoniques radicalement différents pour chaque cas, même lorsque les logiques partagent des propriétés structurelles similaires.
• La difficulté à généraliser les résultats de complétude des modèles de Kripke vers des sémantiques plus abstraites pour ces opérateurs complexes.

2. Méthodologie

Les auteurs proposent une approche structurée en plusieurs étapes :

1. Sémantique de Voisinage Unifiée : Ils interprètent la sémantique des modalités groupées comme une forme spécialisée de sémantique de voisinage. Pour un terme de groupe $\tau$, ils définissent une fonction de voisinage générée $Nbh_M(w, \tau)$ qui capture les conditions minimales de satisfaction et de falsification d'une formule $\phi$ pour que l'opérateur $\#\phi$ soit vrai.
2. Définition Uniforme des Bisimulations : En s'appuyant sur cette structure de voisinage, ils définissent une bisimulation groupée ($\tau$-bisimulation). Cette définition généralise les bisimulations de voisinage existantes mais s'adapte spécifiquement aux structures générées par les termes de groupe.
3. Classe des Bundles Convexes : Ils identifient une classe particulière de modalités groupées, appelées bundles convexes. Une bundle est convexe si l'ensemble des paires de sous-ensembles (satisfaction/falsification) qui satisfont la condition de vérité forme un ensemble convexe (si $Z_1 \subseteq Z_3 \subseteq Z_2$ et $Z_1, Z_2$ sont valides, alors $Z_3$ l'est aussi). Ils montrent que la plupart des opérateurs étudiés dans la littérature appartiennent à cette classe ou en sont des duaux.
4. Sémantique de Voisinage Convexe : Pour axiomatiser ces bundles, ils introduisent une sémantique intermédiaire appelée sémantique de voisinage convexe, utilisant des modèles avec deux fonctions de voisinage ($N^+$ et $N^-$) et des modèles « cœurs » (core models).
5. Stratégie de Complétude : Ils appliquent une stratégie en deux étapes :
   • Construction de modèles canoniques pour les logiques de voisinage convexe.
   • Utilisation de théorèmes de représentation pour transformer ces modèles de voisinage abstraits en modèles de Kripke concrets (S5, KD45, S4.2, etc.) qui préservent la vérité.

3. Contributions Clés

• Théorie Générale de l'Expressivité :

  • Définition uniforme des bisimulations pour n'importe quel terme de groupe.
  • Preuve de la propriété de Hennessy-Milner pour ces bisimulations (sur des modèles image-finis), établissant que l'équivalence bisimilaire coïncide avec l'équivalence logique.
  • Introduction de la notion de convexité pour les bundles, permettant de simplifier les bisimulations (bisimulation convexe) et de mieux caractériser l'expressivité.

• Cadre d'Axiomatisation Unifié :

  • Définition de la logique minimale CONV pour les logiques de voisinage convexe.
  • Démonstration que les modèles canoniques construits pour CONV sont automatiquement des « modèles cœurs », facilitant les preuves de complétude.
  • Établissement de correspondances canoniques entre des axiomes spécifiques (ex. : $4'$, $5$, $Cn$) et des propriétés de frames (symétrie, réflexivité, serialité, bornes de cardinalité).

• Résultats de Représentation :

  • Preuve que les modèles de voisinage convexes satisfaisant certaines propriétés peuvent être représentés par des modèles de Kripke standards (S5, KD45, S4.2, S4F). Cela permet de transférer les résultats de complétude de la sémantique de voisinage vers la sémantique de Kripke.

4. Résultats Principaux (Études de Cas)

Les auteurs appliquent leur cadre général pour fournir des axiomatisations complètes (nouvelles dans la littérature) pour trois cas concrets :

1. « Quelqu'un sait » (Someone Knows) :

   • Opérateur : $\bigvee_{a \in A} \Box_a \phi$.
   • Cadre : Modèles S5.
   • Résultat : Axiomatisation complète de la logique sur les modèles S5 en utilisant les axiomes de CONV étendus par des axiomes de réflexivité, de transitivité et de bornes de cardinalité.

2. « Désaccord dans un groupe » (Disagreement in Group) :

   • Opérateur : $\bigvee_{a,b \in A} (\Box_a \phi \land \Box_b \neg \phi)$.
   • Cadre : Modèles KD45 (logique de croyance).
   • Résultat : Axiomatisation complète utilisant des axiomes adaptés à la sérialité et à la symétrie des relations de croyance.

3. « Croyance sans connaissance » (Belief without Knowledge) :

   • Opérateur : $B\phi \land \neg K\phi$ (équivalent à $\Diamond\Box\phi \land \Diamond\neg\phi$ sur S4.2).
   • Cadre : Modèles S4.2 et S4F.
   • Résultat : Axiomatisation complète pour ces classes de modèles, incluant des axiomes spécifiques pour gérer l'interaction entre la connaissance et la croyance (ex. : axiome $DE\#$).

5. Signification et Perspectives

• Unification : Ce travail fournit le premier cadre théorique unifié capable de traiter une large gamme de modalités groupées, remplaçant des approches ad hoc par une méthode systématique.
• Nouveauté Technique : L'introduction de la sémantique de voisinage convexe et des modèles cœurs offre un terrain d'étude intermédiaire riche entre la logique modale minimale et la logique modale monotone, permettant des distinctions fines (ex. : entre les axiomes $4'$ et $4''$) qui s'effacent dans les logiques normales.
• Impact : La méthode proposée ouvre la voie à l'automatisation de la découverte d'axiomes et de théorèmes de complétude pour de nouvelles modalités groupées.
• Travaux Futurs : Les auteurs suggèrent d'étendre la théorie des bisimulations (notamment les théorèmes de saturation), de développer des théorèmes de correspondance de type Sahlqvist pour les logiques de voisinage convexe, et d'approfondir la théorie générale de ces logiques convexes.

En résumé, cet article établit les fondations d'une théorie générale pour les modalités groupées, résolvant des problèmes ouverts de longue date concernant leur bisimulation et leur axiomatisation, et offrant de nouveaux outils pour l'analyse logique de concepts épistémiques complexes.