Lindström Maximality for Fitting's Finite Heyting-Valued Modal Logic with Exact Truth Tests

Résumé technique : Maximalité de Lindström pour la logique modale de Fitting à valeurs de Heyting finie avec tests de vérité exacte

Énoncé du problème
L'article traite de la caractérisation du pouvoir expressif des logiques modales à plusieurs valeurs, spécifiquement la logique modale de Fitting sur une algèbre de Heyting ($L$) finie et fixe. Bien que des théorèmes de maximalité de type Lindström existent pour la logique modale classique et pour les logiques à plusieurs valeurs sur des chaînes MTL (algèbres linéairement ordonnées) finies, un résultat correspondant faisait défaut pour le cas non linéaire. Des travaux antérieurs par Badia et Olkhovikov ont établi la maximalité sur les chaînes MTL finies en utilisant l'unique prédécesseur immédiat de l'élément haut (1) pour séparer les valeurs désignées des valeurs non désignées. Cette approche échoue pour les algèbres de Heyting arbitraires, qui peuvent manquer de linéarité et d'un unique coatome sous 1. Le problème central est de déterminer si la présentation de la logique de Fitting par Maruyama — qui utilise des tests de vérité unaires exacts ($T_\ell$) plutôt que des constantes de vérité primitives pour toutes les valeurs — conserve sa maximalité parmi ses extensions abstraites sans supposer que l'algèbre est une chaîne.

Méthodologie
L'auteur emploie une approche de modélisation adaptée aux théorèmes de Lindström classiques et à plusieurs valeurs. La méthodologie consiste en :

1. Définition de la logique de base : Utilisation de la version de Maruyama de la logique de Fitting ($FML_L$) sur des cadres de Kripke nets (crisp), où les formules prennent des valeurs dans une algèbre de Heyting finie $L$. Le langage inclut des tests de vérité exacte $T_\ell$ tels que $T_\ell \phi$ vaut 1 si et seulement si $\phi$ vaut $\ell$.
2. Introduction d'opérateurs booléens dérivés : Pour remplacer le mécanisme de séparation dépendant de la chaîne, l'auteur définit des tests à valeurs booléennes :
   • $D\phi := T_1\phi$ (Vrai si $\phi$ est désigné/égal à 1).
   • $N\phi := T_0(T_1\phi)$ (Vrai si $\phi$ est non désigné/non égal à 1).
   • Une modalité existentielle dérivée $\Diamond_1 \phi := T_0(\Box N\phi)$, qui exprime l'existence d'un état accessible où $\phi$ a la valeur 1.
3. Extensions abstraites : L'article considère des extensions abstraites $\mathcal{L}$ de $FML_L$ qui satisfont trois propriétés de modélisation : la compacité, la propriété d'union de Tarski et l'invariance forte par bisimulation.
4. Saturation et déploiement (Unravelling) : La preuve construit des extensions élémentaires saturées en utilisant des techniques de déploiement. Elle s'appuie sur la modalité dérivée $\Diamond_1$ pour définir des « types successeurs » et utilise la compacité et la propriété d'union de Tarski pour construire des modèles où ces types sont réalisés.
5. Le Lemme de Décision : Une étape critique implique un « Lemme de Décision » qui utilise la paire $(D\psi, N\psi)$ pour séparer toute nouvelle formule hypothétique de la logique de base. Cela remplace l'argument du « prédécesseur immédiat de 1 » utilisé dans les preuves basées sur les chaînes.

Contributions clés et résultats

• Théorème de maximalité de Lindström : Le résultat principal (Théorème 1) stipule que pour toute algèbre de Heyting finie $L$ fixée, la version de la logique de Fitting de Maruyama est maximale par rapport au pouvoir d'expression de 1 parmi toutes ses extensions abstraites qui sont compactes, possèdent la propriété d'union de Tarski et sont invariantes par bisimulation forte.
• Suppression de l'hypothèse de linéarité : L'article généralise avec succès le résultat de maximalité des algèbres (chaînes MTL) vers la classe plus large des algèbres de Heyting finies quelconques. La preuve démontre que les tests de vérité exacte fournissent un pouvoir de séparation suffisant sans nécessiter d'ordre linéaire ou de coatome distingué.
• Définissabilité de la valeur exacte : En conséquence du théorème de maximalité (Corollaire 1), l'article prouve que pour toute formule $\phi$ dans une extension $\mathcal{L}$ et toute valeur $\ell \in L$, l'ensemble des modèles pointés où $\phi$ prend la valeur exacte $\ell$ est définissable par une formule dans la logique de base $FML_L$. Plus précisément, la « fibre de valeur exacte » est définissable, bien que l'article note que cela n'implique pas nécessairement l'existence d'une formule unique dans $FML_L$ reproduisant la pleine sémantique $L$-valuée de $\phi$.
• Propriété de Hennessy-Milner pour les modèles saturés : L'article établit que pour les modèles saturés de $FML_L$, l'équivalence modale implique la bisimulation, étendant ainsi les phénomènes standards de Hennessy-Milner à ce contexte à plusieurs valeurs.

Signification et affirmations
L'article prétend combler une lacune dans la littérature concernant les limites expressives des logiques modales à plusieurs valeurs sur des algèbres non linéaires. En démontrant que les tests de vérité exacte ($T_\ell$) produisent des paires de décision booléennes ($D\phi, N\phi$) capables de séparer les valeurs désignées des valeurs non désignées, l'auteur montre que les contraintes structurelles de l'algèbre sous-jacente (spécifiquement la linéarité) ne sont pas nécessaires pour la maximalité de Lindström.

La signification réside dans :

1. Généralisation : Étendre la portée des théorèmes de Lindström au-delà du cadre restrictif des chaînes finies vers la classe plus large des algèbres de Heyting finies.
2. Identification du mécanisme : Identifier les tests à valeurs booléennes dérivés des tests de vérité exacte comme le mécanisme crucial pour la séparation des valeurs et les arguments de saturation dans les contextes non linéaires.
3. Définissabilité : Établir que la logique de base est suffisamment expressive pour définir les fibres de valeur exacte de toute formule dans une extension « raisonnable », renforçant ainsi la robustesse de la présentation de Maruyama.

L'auteur reste modeste quant aux directions futures, notant des questions ouvertes telles que la possibilité d'affaiblir la propriété d'union de Tarski, la manière de traiter les relations d'accessibilité $L$-valuées (floues), et si les définitions séparées de valeur exacte peuvent être unifiées en une seule formule reproduisant la pleine sémantique.