Most Properties are Undecidable for Transitive Tense Logics

Technische Zusammenfassung: Die meisten Eigenschaften sind unentscheidbar für transitive Tense-Logiken

Problemstellung
Die Arbeit befasst sich mit der algorithmischen Entscheidbarkeit logischer Eigenschaften innerhalb des Gitters der transitiven Tense-Logiken, bezeichnet als $NExtK4t$. Während die Entscheidbarkeit von Eigenschaften (wie Kripke-Vollständigkeit, die endliche Modell-Eigenschaft und die Entscheidbarkeit selbst) für unimodale Logiken und lineare Tense-Logiken gut untersucht ist, bleibt der Status dieser Eigenschaften in der intermediären Klasse der transitiven Tense-Logiken eine kritische offene Frage. Insbesondere untersuchen die Autoren, ob die natürliche Interaktion zwischen der Zukunft ($\Box$) und der Vergangenheit ($\blacksquare$) der Modalitäten in transitiven Rahmen die Entscheidbarkeit der Eigenschaftsprobleme für transitive Tense-Logiken unentscheidbar macht. Vorherige Arbeiten von Chagrov und Shehtman etablierten die Unentscheidbarkeit von Tabularität und Konsistenz in $NExtK4t$, aber die Entscheidbarkeit von Kripke-Vollständigkeit, der endlichen Modell-Eigenschaft (FMP) und der allgemeinen Entscheidbarkeit blieb ungeklärt.

Methodik
Die Autoren adaptieren eine Reduktionstechnik, die ursprünglich von Chagrov für unimodale Logiken entwickelt wurde, und erweitern sie auf den bimodalen Kontext von Tense-Logiken. Die Kernmethode besteht darin, eine berechenbare Reduktion vom Erreichbarkeitsproblem von Minsky-Maschinen (ein bekanntes unentscheidbares Problem, das äquivalent zum Halteproblem für Turing-Maschinen ist) auf das Entscheidungsproblem für spezifische logische Eigenschaften zu konstruieren.

1. Minsky-Maschinen-Kodierung: Die Autoren verwenden eine Minsky-Maschine $M$ mit zwei Registern und einer spezifischen Konfiguration $c_0 = \langle s, n, m \rangle$, sodass die Menge der erreichbaren Konfigurationen unentscheidbar ist.
2. Konstruktion eines allgemeinen Rahmens: Ein spezifischer allgemeiner Rahmen $\mathcal{F} = (W, R, A)$ wird konstruiert. Die Domäne $W$ kodiert die erreichbaren Konfigurationen von $M$ neben Hilfspunkten ($a_i, b_i, c_i$), die die Registerwerte und eine „Zähler“-Struktur repräsentieren. Die Erreichbarkeitsrelation $R$ wird definiert, um die Übergänge der Minsky-Maschine und die Inkrement-/Dekrement-Operationen auf den Registern zu simulieren.
3. Formelkonstruktion: Die Autoren definieren eine Menge von variablenfreien Formeln ($\phi_{c_n}, \phi_{a_n}, \phi_{b_n}$), die spezifische Punkte im Rahmen $\mathcal{F}$ eindeutig identifizieren. Weiterhin definieren sie die Formeln $\psi_A, \psi_B$ und deren Nachfolger, um die $+1$- und $-1$-Operationen auf den Registern zu simulieren.
4. Logikkonstruktion: Für jede Konfiguration $c = \langle t, k, l \rangle$ wird eine Logik $L(c)$ als eine Erweiterung von $K4t$ definiert. Diese Logik umfasst:
   • Axiome ($Ax_M$), welche die Übergangsregeln der Minsky-Maschine kodieren.
   • Ein konditionales Axiom, das die Anfangskonfiguration mit der Zielkonfiguration $c$ verknüpft.
   • Eine spezifische Formel $\alpha$ (abgeleitet aus einer tabularen Logik) und eine „Trap“-Formel $\phi_0$, die dazu dienen, sicherzustellen, dass die resultierende Logik Kripke-unvollständig und unentscheidbar ist, falls die Zielkonfiguration nicht erreichbar ist.

Wesentliche Beiträge und Ergebnisse
Die Arbeit etabliert ein allgemeines Kriterium (Theorem 3.5) für die Unentscheidbarkeit von Eigenschaften in $NExtK4t$. Das Theorem besagt, dass, wenn eine Eigenschaft $P$ in der Vereinigung von Kripke-Vollständigkeit ($KC$) und Entscheidbarkeit ($DEC$) enthalten ist und es eine Formel $\alpha$ gibt, so dass $K4t \oplus \alpha \in P$, der konstruierte Rahmen $\mathcal{F}$ jedoch $\alpha$ nicht validiert, dann ist $P$ unentscheidbar.

Durch Anwendung dieses Theorems beweisen die Autoren die folgenden Ergebnisse (Korollar 3.13):

• Die folgenden Mengen von Formeln sind unentscheidbar in $NExtK4t$:
  1. Kripke-Vollständigkeit.
  2. Kanonizität.
  3. Prädikatenlogische Definierbarkeit.
  4. Die endliche Modell-Eigenschaft (FMP).
  5. Lokale Tabularität.
  6. Tabularität.
  7. Entscheidbarkeit (der Logik selbst).
  8. Übereinstimmung mit einer fixen tabularen Logik.
  9. Konsistenz (speziell ist das Komplement, die Inkonsistenz, unentscheidbar).

Darüber hinaus stellen die Autoren über Proposition 2.2 fest, dass diese Unentscheidbarkeitsergebnisse, da $K4t$ eine Erweiterung von $Kt$ (der minimalen Tense-Logik) ist, auch auf das Gitter $NExtKt$ übertragbar sind.

Bedeutung und Behauptungen
Die Arbeit behauptet, den Entscheidungsstatus wesentlicher logischer Eigenschaften für transitive Tense-Logiken gelöst zu haben, indem sie zeigt, dass „die meisten Eigenschaften unentscheidbar sind“ in dieser Klasse. Die Bedeutung liegt in der Klärung, wie die Interaktion der Modalitäten die Entscheidbarkeit beeinflusst:

• Kontrast zur linearen Zeit: Während Eigenschaften im Gitter der linearen Zeitflüsse ($NExtLint$) entscheidbar sind, führt die Einführung von Transitivität ohne Linearität ($NExtK4t$) zu Unentscheidbarkeit.
• Kontrast zu unimodalen Logiken: Die Ergebnisse verdeutlichen, dass die minimale Tense-Erweiterungskarte keine Eigenschaften wie Kripke-Vollständigkeit oder FMP erhält, was den bimodalen Fall fundamental anders und komplexer macht als den unimodalen Fall ($NExtK4$).
• Allgemeines Schema: Die Arbeit liefert ein allgemeines Beweisschema zur Etablierung von Unentscheidbarkeit in Tense-Logiken, indem sie die Erreichbarkeit von Minsky-Maschinen auf logische Eigenschaften reduziert, und füllt damit eine Lücke, die durch vorangegangene Arbeiten hinterlassen wurde, welche die Unentscheidbarkeit unimodaler Ergebnisse aufgrund der Nicht-Injektivität der Tense-Erweiterungskarte nicht direkt auf den Tense-Kontext übertragen konnten.

Die Autoren kommen zu dem Schluss, dass die Interaktionen der Modalitäten in transitiven Tense-Logiken das Entscheidungsproblem für Eigenschaften strenger macht als in linearen Tense-Logiken, und legen nahe, dass für Eigenschaften wie die Kripke-Vollständigkeit die Unentscheidbarkeit in einem unimodalen Gitter wahrscheinlich die Unentscheidbarkeit in seiner minimalen Tense-Erweiterung impliziert, was jedoch eine Vermutung für zukünftige Arbeiten bleibt.