Most Properties are Undecidable for Transitive Tense Logics

Résumé technique : La plupart des propriétés sont indécidables pour les logiques de la temporalité transitives

Énoncé du problème
L'article traite de la décidabilité algorithmique des propriétés logiques au sein du treillis des logiques de la temporalité transitives, noté $NExtK4t$. Bien que la décidabilité des propriétés (telles que la complétude de Kripke, la propriété du modèle fini et la décidabilité elle-même) soit bien étudiée pour les logiques unimodales et les logiques de la temporalité linéaire, le statut de ces propriétés dans la classe intermédiaire des logiques de la temporalité transitives demeure une question ouverte critique. Plus précisément, les auteurs cherchent à savoir si l'interaction naturelle entre les modalités du futur ($\Box$) et du passé ($\blacksquare$) dans les cadres transitifs rend le problème de la décision pour ces propriétés indécidable. Des travaux antérieurs de Chagrov et Shehtman ont établi l'indécidabilité de la tabularité et de la consistance dans $NExtK4t$, mais la décidabilité de la complétude de Kripke, de la propriété du modèle fini (FMP) et de la décidabilité générale restait non résolue.

Méthodologie
Les auteurs adaptent une technique de réduction initialement développée par Chagrov pour les logiques unimodales, en l'étendant au cadre bimodal des logiques de la temporalité. La méthode centrale consiste à construire une réduction calculable du problème de l'accessibilité des machines de Minsky (un problème connu comme étant indécidable, équivalent au problème de l'arrêt pour les machines de Turing) vers le problème de la décision pour des propriétés logiques spécifiques.

1. Encodage de la machine de Minsky : Les auteurs utilisent une machine de Minsky $M$ avec deux registres et une configuration spécifique $c_0 = \langle s, n, m \rangle$ telle que l'ensemble des configurations atteignables est indécidable.
2. Construction du cadre général : Un cadre général spécifique $\mathcal{F} = (W, R, A)$ est construit. Le domaine $W$ encode les configurations atteignables de $M$ aux côtés de points auxiliaires ($a_i, b_i, c_i$) représentant les valeurs des registres et une structure de « compteur ». La relation d'accessibilité $R$ est définie pour simuler les transitions de la machine de Minsky ainsi que les opérations d'incrémentation et de décrémentation sur les registres.
3. Construction de formules : Les auteurs définissent un ensemble de formules sans variables ($\phi_{c_n}, \phi_{a_n}, \phi_{b_n}$) qui identifient de manière unique des points spécifiques dans le cadre $\mathcal{F}$. Ils définissent ensuite les formules $\psi_A, \psi_B$ et leurs successeurs pour simuler les opérations $+1$ et $-1$ sur les registres.
4. Construction de la logique : Pour toute configuration $c = \langle t, k, l \rangle$, une logique $L(c)$ est définie comme une extension de $K4t$. Cette logique inclut :
   • Des axiomes ($Ax_M$) encodant les règles de transition de la machine de Minsky.
   • Un axiome conditionnel reliant la configuration initiale à la configuration cible $c$.
   • Une formule spécifique $\alpha$ (dérivée d'une logique tabulaire) et une formule « piège » $\phi_0$ conçues pour garantir que si la configuration cible n'est pas atteignable, la logique résultante est incomplète au sens de Kripke et indécidable.

Contributions clés et résultats
L'article établit un critère général (Théorème 3.5) pour l'indécidabilité des propriétés dans $NExtK4t$. Le théorème stipule que si une propriété $P$ est contenue dans l'union de la complétude de Kripke ($KC$) et de la décidabilité ($DEC$), et qu'il existe une formule $\alpha$ telle que $K4t \oplus \alpha \in P$ mais que le cadre $\mathcal{F}$ construit ne valide pas $\alpha$, alors $P$ est indécidable.

En appliquant ce théorème, les auteurs prouvent les résultats suivants (Corollaire 3.13) :

• Les ensembles de formules suivants sont indécidables dans $NExtK4t$ :
  1. La complétude de Kripke.
  2. La canonicité.
  3. La définissabilité du premier ordre.
  4. La propriété du modèle fini (FMP).
  5. La tabularité locale.
  6. La tabularité.
  7. La décidabilité (de la logique elle-même).
  8. La coïncidence avec une logique tabulaire fixée.
  9. La consistance (plus précisément, le complément, l'inconsistance, est indécidable).

De plus, via la Proposition 2.2, les auteurs notent que puisque $K4t$ est une extension de $Kt$ (la logique de la temporalité minimale), ces résultats d'indécidabilité s'étendent au treillis $NExtKt$.

Signification et revendications
L'article affirme résoudre le statut de décidabilité de propriétés logiques majeures pour les logiques de la temporalité transitives, démontrant que « la plupart des propriétés sont indécidables » dans cette classe. La signification réside dans la clarification de la manière dont l'interaction des modalités affecte la décidabilité :

• Contraste avec le temps linéaire : Alors que les propriétés sont décidables dans le treillis des flux de temps linéaires ($NExtLint$), l'introduction de la transitivité sans linéarité ($NExtK4t$) conduit à l'indécidabilité.
• Contraste avec les logiques unimodales : Les résultats soulignent que l'application de la carte d'extension de la temporalité minimale ne préserve pas des propriétés comme la complétude de Kripke ou la FMP, rendant le cas bimodal fondamentalement différent et plus complexe que le cas unimodal ($NExtK4$).
• Schéma général : L'article fournit un schéma de preuve général pour établir l'indécidabilité dans les logiques de la temporalité en réduisant l'accessibilité des machines de Minsky à des propriétés logiques, comblant ainsi une lacune laissée par les travaux précédents qui ne pouvaient pas transférer directement les résultats d'indécidabilité unimodale au cadre de la temporalité en raison de la non-injectivité de la carte d'extension de la temporalité.

Les auteurs concluent que les interactions des modalités dans les logiques de la temporalité transitives rendent le problème de décision pour les propriétés strictement plus difficile que dans les logiques de la temporalité linéaires et suggèrent que pour des propriétés comme la complétude de Kripke, l'indécidabilité dans un treillis unimodal implique probablement l'indécidabilité dans son extension de temporalité minimale, bien que cela reste une conjecture pour des travaux futurs.