Fusions of One-Variable First-Order Modal Logics

Cet article établit que la fusion indépendante de logiques modales du premier ordre à une variable préserve la complétude de Kripke et la décidabilité sans égalité, mais pas avec égalité ou constantes non rigides, tout en fournissant une condition suffisante générale pour le transfert de ces propriétés via une interprétation comme fusion de logiques modales propositionnelles partageant une modalité S5.

L'essentiel

Imaginez que la logique est une boîte à outils remplie de règles pour raisonner correctement. Certains outils sont simples (comme la logique propositionnelle, qui gère des phrases comme « Il pleut » ou « Il ne pleut pas »), tandis que d'autres sont plus complexes et permettent de parler de personnes, d'objets et de leurs propriétés (la logique du premier ordre).

Les auteurs de cet article, Roman Kontchakov, Dmitry Shkatov et Frank Wolter, s'intéressent à ce qui se passe quand on essaie de fusionner deux de ces boîtes à outils différentes pour en créer une seule, plus puissante.

Voici une explication simple de leurs découvertes, utilisant des analogies du quotidien.

1. Le concept de « Fusion » : Mariage sans mélange de cuisine

Imaginez deux cuisiniers, l'un expert en cuisine italienne (Logique A) et l'autre en cuisine japonaise (Logique B).

• La fusion consiste à mettre leurs deux cuisines côte à côte dans un grand restaurant.
• La règle d'or : Le cuisinier italien ne touche pas aux ingrédients japonais, et le cuisinier japonais ne touche pas aux ingrédients italiens. Ils ne créent pas de nouvelles recettes qui mélangent les deux (pas de « pizza au sashimi »).

Dans le monde de la logique, cela signifie qu'on combine deux systèmes de règles sans créer de nouvelles règles qui mélangeraient leurs opérateurs spéciaux.

2. Le cas simple : Sans égalité (Le monde des « Chapeaux »)

Les auteurs commencent par un cas où l'on ne demande pas aux objets d'être « égaux » ou identiques. C'est comme si on parlait de chapeaux : « Il y a un chapeau rouge » ou « Il y a un chapeau bleu ».

• Le résultat magique : Si vous prenez deux systèmes logiques qui fonctionnent bien séparément (ils sont « complets » et « décidables », c'est-à-dire qu'on peut toujours dire si une phrase est vraie ou fausse), leur fusion fonctionne aussi bien !
• L'analogie : Si vous avez deux jeux de règles de société qui sont amusants et clairs, les mettre ensemble dans une grande boîte sans mélanger les règles donne un super jeu combiné. Tout reste prévisible.
• La petite exception : Il y a une chose qui ne passe pas toujours : la propriété de « modèle fini ». Imaginez que pour prouver qu'une phrase est fausse, vous avez besoin d'un exemple avec un nombre infini de chapeaux. Dans le cas de la fusion, même si les jeux séparés n'avaient besoin que de petits exemples, le jeu combiné pourrait exiger une infinité d'exemples pour prouver une erreur. C'est comme si le restaurant combiné avait besoin d'un stock infini d'ingrédients pour prouver qu'une recette est impossible.

3. Le cas difficile : Avec égalité et comptage (Le monde des « Jumeaux »)

Ensuite, les auteurs ajoutent l'égalité et la possibilité de compter. C'est comme si on disait : « Il y a exactement un chapeau rouge » ou « Ce chapeau est le même que celui-ci ».

• Le désastre : Ici, la fusion devient un cauchemar. Même si les deux cuisines séparées sont simples et gérables, une fois fusionnées avec la notion d'égalité, le système devient indécidable.
• L'analogie : C'est comme si, en ajoutant la règle « ce chapeau est le même que celui-là », on permettait aux cuisiniers de créer des recettes infiniment complexes qui ressemblent à des équations mathématiques impossibles à résoudre (les équations diophantiennes). On ne peut plus jamais être sûr de dire « oui » ou « non » à une question. C'est comme essayer de prédire si un labyrinthe infini a une sortie : parfois, il n'y a pas de réponse possible.
• Le verdict : Si vous mélangez la logique avec l'égalité et des constantes non rigides (des objets qui peuvent changer d'identité d'un monde à l'autre), vous perdez la capacité de décider automatiquement si une affirmation est vraie.

4. La solution de secours : Le modus S5 (Le « Grand Hall »)

Pour sauver la situation, les auteurs proposent une astuce. Ils regardent la logique non plus comme des objets, mais comme des mondes reliés par une relation spéciale appelée S5.

• L'analogie : Imaginez un grand hall (le modus S5) où tout le monde se voit tous (une relation d'équivalence). Si les deux cuisiniers partagent ce même grand hall pour communiquer, alors la fusion redevient gérable !
• Le résultat : Si les deux systèmes logiques acceptent ce « Grand Hall » (des modèles homogènes), alors on peut garantir que leur fusion restera décidable et complète. C'est comme si le fait de partager un même espace de discussion commun empêchait les cuisiniers de créer des recettes trop folles.

En résumé

1. Sans égalité : Fusionner deux logiques simples donne une logique simple. C'est une fusion réussie.
2. Avec égalité : Fusionner deux logiques simples devient un monstre indécidable. C'est une fusion catastrophique.
3. L'astuce : Si les logiques partagent une structure commune de type « S5 » (un grand hall de connexions), on peut sauver la mise et garder la logique gérable.

Cet article est donc une carte routière pour les ingénieurs de la logique : il leur dit exactement quand ils peuvent combiner leurs outils sans risquer de créer un système impossible à maîtriser, et quand ils doivent absolument éviter de mélanger certaines pièces.

Résumé technique

Voici un résumé technique détaillé de l'article « Fusions of One-Variable First-Order Modal Logics » (Fusions de logiques modales du premier ordre à une variable), rédigé en français.

1. Problématique et Contexte

L'article s'inscrit dans le domaine de la logique modale combinée, une aire de recherche active visant à déterminer comment les propriétés des logiques composantes sont préservées lors de leur fusion. La fusion est une méthode de combinaison où les logiques sont réunies sans introduire d'axiomes mixant leurs opérateurs modaux ni imposer de contraintes sémantiques reliant leurs relations d'accessibilité distinctes.

Il est bien établi que pour les logiques modales propositionnelles classiques, la fusion préserve des propriétés cruciales telles que la complétude de Kripke, la décidabilité, la propriété du modèle fini (FMP) et l'interpolation de Craig.

L'objectif principal de cet article est d'étudier dans quelle mesure ces résultats de préservation s'étendent aux logiques modales du premier ordre à une variable, un fragment souvent mieux comporté computationnellement que les logiques du premier ordre complètes. Les auteurs examinent deux cas principaux :

1. Les logiques sans égalité.
2. Les logiques avec égalité et constantes non rigides (ou quantificateurs de comptage).

Le problème central est de déterminer si la décidabilité et la complétude de Kripke sont préservées lors de la fusion de ces logiques, et si la propriété du modèle fini (FMP) est conservée.

2. Méthodologie

Les auteurs utilisent une approche combinant des techniques de modèles quasi (quasimodels), des constructions de modèles spécifiques (modèles « cactus ») et des réductions de problèmes indécidables.

• Technique des Quasimodèles et Modèles Cactus : Pour les logiques sans égalité, la preuve repose sur l'extension de la construction de modèles « cactus » (initialement utilisée pour les logiques propositionnelles) au cadre du premier ordre à une variable. Cette méthode permet de représenter finiment un nombre infini d'éléments du domaine via des « types » et des « quasi-états ».
• Modèles Homogènes : Pour la partie propositionnelle partageant un modale S5, les auteurs introduisent la notion de modèles E-homogènes. Un modèle est E-homogène si, pour toute classe d'équivalence E, chaque formule est soit non satisfaite, soit satisfaite dans un nombre infini (cardinal $\kappa$) de mondes de cette classe.
• Réductions d'Indécidabilité : Pour démontrer les résultats de non-préservation avec l'égalité, les auteurs encodent des équations diophantiennes et des machines de Minsky dans les logiques fusionnées. Cela permet de prouver l'indécidabilité en montrant que la satisfiabilité dans la fusion équivaut à la résolution de problèmes arithmétiques indécidables.
• Correspondance avec les Logiques Propositionnelles : Les auteurs exploitent le fait que le fragment à une variable sans égalité est isomorphe à la logique modale propositionnelle S5. Ils étudient ainsi les fusions de logiques propositionnelles partageant un opérateur S5 commun.

3. Résultats Clés

Les résultats sont divisés en deux catégories principales selon la présence ou l'absence d'égalité.

A. Logiques sans Égalité (Théorème A)

Pour les fusions de logiques modales du premier ordre à une variable sans égalité (sous sémantique à domaines constants ou expansifs) :

• Préservation : La complétude de Kripke et la décidabilité (tant pour la conséquence locale que globale) sont préservées.
• Propriété du Modèle Fini (FMP) :
  • La FMP est préservée pour la conséquence locale.
  • La FMP n'est pas préservée pour la conséquence globale. En fait, pour toute fusion non triviale, la conséquence globale échoue à avoir la propriété du modèle fini, même sous sémantique à domaines constants.

B. Logiques avec Égalité (Théorème B)

Dès que l'égalité est introduite, accompagnée de constantes non rigides (ou de quantificateurs de comptage comme $\exists=1$), les résultats de préservation s'effondrent :

• Indécidabilité : La décidabilité et l'axiomatisation récursive ne sont pas préservées. La fusion de logiques décidables peut devenir indécidable.
• Conséquence Globale : Pour la sémantique à domaines constants, la conséquence globale est indécidable pour toutes les fusions non triviales.
• Nuance importante : Les auteurs soulignent que cela ne signifie pas que toutes les logiques à une variable avec égalité sont indécidables. Des systèmes standards (comme K polymodal ou S5) restent décidables. L'indécidabilité émerge spécifiquement de la combinaison (fusion) de ces logiques.

C. Fusions Propositionnelles Partageant un S5 (Théorème C)

Les auteurs établissent une condition suffisante générale pour les logiques propositionnelles partageant un opérateur S5 ($\Box_E$) :

• Si les logiques composantes admettent des modèles E-homogènes, alors leur fusion préserve la complétude de Kripke et la décidabilité (locale et globale).
• Cette condition s'applique aux (semi)commutateurs avec S5 et aux produits de logiques modales avec S5.
• Contrairement au cas sans égalité, la propriété du modèle fini n'est pas transférée par cette méthode.

4. Signification et Implications

• Frontière de la Décidabilité : L'article identifie une frontière fine entre la décidabilité et l'indécidabilité dans les logiques modales du premier ordre. L'ajout de l'égalité et de la capacité à compter (via des constantes non rigides) dans un contexte de fusion suffit à briser la décidabilité, même si les composants individuels sont décidables.
• Limites de la Fusion : Contrairement au cas propositionnel, la fusion n'est pas une méthode « robuste » pour les logiques du premier ordre à une variable lorsqu'elle inclut l'égalité. Cela met en garde contre l'application naïve des résultats de fusion propositionnelle aux fragments du premier ordre.
• Outils Techniques : L'extension de la construction de modèles cactus et l'introduction des modèles E-homogènes fournissent de nouveaux outils puissants pour analyser la sémantique des logiques modales combinées.
• Fragments Monodiques : L'article aborde également les fragments monodiques (formules avec au plus une variable libre). Il montre que la décidabilité ne se transfère pas nécessairement du fragment à une variable avec égalité vers des fragments monodiques plus expressifs basés sur des fragments décidables du premier ordre (comme le fragment à deux variables avec comptage), résolvant ainsi un problème ouvert.

Conclusion

En résumé, cet article démontre que la fusion de logiques modales du premier ordre à une variable préserve la complétude et la décidabilité uniquement en l'absence d'égalité. Dès que l'égalité et le comptage sont autorisés, la fusion peut engendrer des systèmes indécidables. Ces résultats nuancent considérablement l'espoir d'une généralisation simple des propriétés de fusion propositionnelle aux logiques du premier ordre et ouvrent la voie à de nouvelles recherches sur les conditions suffisantes pour la préservation de la décidabilité dans des contextes plus complexes.