On Modal Logics of Full Products of Neighborhood Frames

Technische Zusammenfassung: Über modale Logiken voller Produkte von Nachbarschaftsrahmen

Problemstellung
Die Arbeit befasst sich mit der Charakterisierung der modalen Logiken, die mit „vollen Produkten“ von Nachbarschaftsrahmen assoziiert sind. Während die Logik von Produkten für Kripke-Rahmen und topologische Räume (speziell für Systeme wie $S4$ und $D4$) gut verstanden ist, ist das Verhalten voller Produkte im Kontext schwächerer, nicht-normaler modaler Logiken weniger erforscht.

In der Standard-Kripke-Semantik führt das volle Produkt zweier Rahmen eine dritte Erreichbarkeitsrelation (die synchrone Relation) neben den horizontalen und vertikalen Relationen ein. Diese Struktur validiert typischerweise starke Interaktionsprinzipien wie Kommutativität ($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) und Konvergenz. Im Gegensatz dazu erlaubt die Nachbarschaftssemantik, welche die Kripke-Semantik generalisiert und als Spezialfall die topologische Semantik einschließt, die Konstruktion von Produkten, in denen diese Interaktionsprinzipien nicht notwendigerweise gelten.

Das spezifische Problem, das angegangen wird, ist die präzise Axiomatisierung des vollen Nachbarschaftsprodukts für die Logiken $T$ (reflexiv) und $D$ (seriell). Die Autoren untersuchen die tri-modale Logik, die durch die Klasse der vollen Produkte von Nachbarschaftsrahmen erzeugt wird, welche $T$ oder $D$ validieren, ausgestattet mit drei Nachbarschaftsfunktionen: horizontal ($\square_1$), vertikal ($\square_2$) und produktbezogen ($\square$).

Methodik
Die Autoren verwenden eine Kombination aus semantischer Analyse und Vollständigkeitsbeweisen mittels gebundener Morphismen.

1. Definitionen und untere Schranken:
   Das Papier definiert das volle Nachbarschaftsprodukt $X \times^+_n Y$ zweier Nachbarschaftsrahmen $X$ und $Y$. Diese Struktur enthält horizontale und vertikale Nachbarschaftsfunktionen (abgeleitet aus den Komponentennrahmen) sowie eine Produkt-Nachbarschaftsfunktion (generiert aus Produkten von Nachbarschaften der Komponenten).
   Die Autoren bestimmen die unteren Schranken für die Logiken $T \times^+_n T$ und $D \times^+_n D$, indem sie valide Axiome identifizieren. Sie führen das Interaktionsaxiom $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$ ein. Sie zeigen, dass die Logiken $T_3^m = T \otimes T \otimes T + (mix)$ und $D_3^m = D \otimes D \otimes D + (mix)$ in den Logiken der jeweiligen vollen Produkte enthalten sind.

2. Vollständigkeit über unendliche Bäume:
   Um die oberen Schranken (d. h. dass die Produktlogiken in $T_3^m$ und $D_3^m$ enthalten sind) zu beweisen, konstruieren die Autoren spezifische unendliche Kripke-Rahmen:

   • $T^{r,m}_{\omega,\omega,\omega}$: Ein reflexiver, unendlich verzweigter Baum mit den Relationen $R, R_1, R_2$, welche $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$ erfüllen.
   • $T^{i,m}_{\omega,\omega,\omega}$: Ein irreflexives Gegenstück.
     Sie beweisen, dass $T_3^m$ bezüglich $T^{r,m}_{\omega,\omega,\omega}$ und $D_3^m$ bezüglich $T^{i,m}_{\omega,\omega,\omega}$ soundness und complete sind. Dies beruht auf der endlichen Modell-Eigenschaft (FMP) dieser Logiken, die mittels Filtrationstechniken etabliert wurde, welche die Interaktionsbedingung $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$ bewahren.

3. Konstruktion von Nachbarschaftsrahmen und gebundene Morphismen:
   Eine kritische technische Hürde ist, dass die Nachbarschaftsrahmen, die zur Falsifizierung von Interaktionsaxiomen wie Kommutativität erforderlich sind, nicht direkt aus Kripke-Rahmen abgeleitet werden können (da Kripke-induzierte Nachbarschaftsrahmen Kommutativität bewahren). Um dies zu umgehen, konstruieren die Autoren spezifische Nachbarschaftsrahmen $N^r_\omega$ und $N^i_\omega$ basierend auf „pseudo-unendlichen Sequenzen“ (Sequenzen natürlicher Zahlen, die schließlich ein spezielles Symbol $\star$ werden). Diese Rahmen besitzen Nachbarschaften, die unendliche streng fallende Ketten bilden, wodurch sichergestellt wird, dass kein Zustand eine kleinste Nachbarschaft besitzt, was notwendig ist, um Kripke-ähnliche Eigenschaften zu brechen.
   Schließlich definieren die Autoren einen surjektiven gebundenen Morphismus vom vollen Produkt dieser Nachbarschaftsrahmen ($N^r_\omega \times^+_n N^r_\omega$) auf den Nachbarschaftsrahmen, der durch den Baum $T^{r,m}_{\omega,\omega,\omega}$ induziert wird. Dieser Morphismus beweist, dass jede auf dem Baum wahre Formel auch auf dem Produkt wahr ist, wodurch die obere Schranke etabliert wird.

Wesentliche Beiträge und Ergebnisse
Der primäre Beitrag des Papers ist die exakte Axiomatisierung der vollen Nachbarschaftsprodukte für die Logiken $T$ und $D$:

• Theorem 1.4:

  • $T \times^+_n T = T \otimes T \otimes T + (mix)$
  • $D \times^+_n D = D \otimes D \otimes D + (mix)$

  Hierbei bezeichnet $\otimes$ die Fusion von Logiken, und $(mix)$ ist das Interaktionsaxiom $\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$.

• Unterscheidung von topologischen Semantiken:
  Das Papier hebt eine entscheidende Divergenz zwischen topologischer Semantik und allgemeiner Nachbarschaftssemantik hervor. In der topologischen Semantik (die zu reflexiven Rahmen korrespondiert) ist das Axiom $(sub) = \square p \to \square_1 p \land \square_2 p$ auf vollen Produkten gültig. Die Autoren zeigen, dass über $S4 \otimes S4 \otimes S4$ die Axiome $(sub)$ und $(mix)$ äquivalent sind. Jedoch ist für die schwächere serielle Logik $D$ das Axiom $(sub)$ nicht auf vollen Nachbarschaftsprodukten gültig. Das Papier liefert ein Gegenbeispiel (durch Anpassung eines Kripke-Rahmen-Beispiels an die Nachbarschaftssemantik), das zeigt, dass $(sub) \notin D \times^+_n D$, während $(mix)$ weiterhin gültig bleibt.

• Entscheidbarkeit:
  Durch den Nachweis der endlichen Modell-Eigenschaft für die resultierenden Logiken $T_3^m$ und $D_3^m$ kommen die Autoren zu dem Schluss, dass diese Logiken entscheidbar sind.

Bedeutung
Das Papier erweitert bekannte Produktergebnisse für $S4$ und $D4$ auf schwächere Systeme ($T$ und $D$) innerhalb des Nachbarschaftssemantik-Rahmens. Es klärt die strukturellen Unterschiede zwischen vollen Produkten in topologischen Settings versus allgemeinen Nachbarschaftssettings, indem es spezifisch zeigt, dass die Reflexivität der zugrunde liegenden Rahmen eine notwendige Bedingung für die Gültigkeit des $(sub)$-Axioms in vollen Produkten ist. Die Arbeit liefert eine vollständige Charakterisierung der tri-modalen Logiken, die aus diesen Produkten entstehen, und schließt eine Lücke in der Literatur bezüglich der Interaktion von Modalitäten in nicht-normalen, produktbasierten Nachbarschaftsstrukturen. Die Autoren merken an, dass die Erweiterung dieser Ergebnisse auf nicht-serielle Logiken wie $K$ oder $K4$ eine offene Forschungsrichtung bleibt, da die verwendeten Techniken (die auf Serialität beruhen) hierfür nicht direkt anwendbar sind.