Dynamic Hypersequents for Public Announcement Logic

Technische Zusammenfassung: Dynamische Hypersequenzen für die Logik öffentlicher Ankündigungen

Problemstellung
Die Dynamische Epistemische Logik (DEL) und speziell die Logik öffentlicher Ankündigungen (PAL) modellieren die Evolution von Wissen durch Informationsupdates. Während die Semantik von PAL als Transformationen von Kripke-Modellen gut verstanden ist (wobei eine Ankündigung die Menge der möglichen Welten einschränkt), haben bestehende beweistheoretische Rahmenwerke Schwierigkeiten, diese Dynamik auf der syntaktischen Ebene zu erfassen. Frühere Versuche, einschließlich Tableau-Methoden und verschiedener Sequenzenkalküle (markiert und unmarkiert), scheitern oft daran, gleichzeitig eine genuine Unterformel-Eigenschaft, die Zulässigkeit aller strukturellen Regeln (einschließlich Kontraktion) und eine syntaktische Schnittelimination zu erreichen. Viele bestehende Systeme verlassen sich auf Reduktionsaxiome, die dynamische Formeln in statische übersetzen, wodurch die dynamische Natur der Logik innerhalb des Beweissystems selbst verschleiert wird.

Methodik
Die Autoren schlagen einen neuen beweistheoretischen Rahmen auf Basis von dynamischen Hypersequenzen vor. Dieser Ansatz erweitert den Hypersequenzenkalkül für S5 (eingeführt in [15, 16]) durch die Integration eines Mechanismus, der Übergänge zwischen epistemischen Modellen modelliert, die durch öffentliche Ankündigungen induziert werden.

1. Dynamische Sequenzen: Eine dynamische Sequenz wird definiert als eine Folge von Standardsequenzen, die durch verschiedene endliche Folgen von Ankündigungen markiert sind (z. B. $\alpha_1 \Gamma_1 | \dots | \alpha_n \Gamma_n$). Intuitiv repräsentiert eine dynamische Sequenz eine spezifische Welt $w$ in einem Anfangsmodell $M$ und ihre „Kopien" in sukzessiv aktualisierten Modellen $M_{\alpha}$.
2. Dynamische Hypersequenzen (DHS): Eine dynamische Hypersequenz ist eine Sammlung von dynamischen Sequenzen. Diese Struktur repräsentiert syntaktisch ein gesamtes epistemisches Modell und seine sukzessiven Updates gleichzeitig. Die Autoren interpretieren eine DHS als Disjunktion von geklammerten Formeln, wobei jede Komponente einer Welt im Modell oder ihren Updates entspricht.
3. Der Kalkül ($DHSPAL$): Die Autoren definieren einen Kalkül $DHSPAL$, der Folgendes umfasst:
   • Propositionale und modale Regeln: Angepasst von Standard-Hypersequenzenkalkülen für S5.
   • Ankündigungsregeln: Regeln $(L[\cdot])$ und $(R[\cdot])$, die Formeln öffentlicher Ankündigungen $[A]B$ zerlegen. Diese Regeln verwalten explizit den Übergang von einem aktuellen Zustand zu einem aktualisierten Zustand, indem sie neue dynamische Sequenzen einführen, die mit der erweiterten Ankündigungsfolge $\alpha \cdot A$ markiert sind.
   • Dynamische strukturelle Regeln: Spezifische Regeln wie $(Lat)$ und $(Rat)$ (Atomare Permanenz), $(New)$ (sicherstellend, dass Welten in aktualisierten Modellen in vorherigen existieren) und $(Recall)$ (sicherstellend, dass die angekündigte Formel im vorherigen Modell gilt).
   • Dynamische modale Regel: Eine spezialisierte Regel $(L\Box_3)$, die die Interaktion zwischen Wissen ($\Box$) und Folgen von Ankündigungen behandelt und zwischen Welten unterscheidet, die ein Update überleben, und denen, die es nicht tun.

Hauptbeiträge und Ergebnisse
Die Arbeit stellt fest, dass $DHSPAL$ ein robustes Beweissystem für PAL ist, das mehrere Eigenschaften erreicht, die früheren Systemen gleichzeitig fehlten:

• Zulässigkeit struktureller Regeln: Die Autoren beweisen die hp-Zulässigkeit (höhen-erhaltende Zulässigkeit) der Schwächung, Kontraktion und einer Mischungsregel. Entscheidend ist dies einschließlich der Kontraktion, die in dynamischen Logiken oft schwer zu erreichen ist, ohne die Analytizität zu verlieren.
• Invertierbarkeit logischer Regeln: Alle logischen Regeln im Kalkül werden als hp-invertierbar nachgewiesen. Diese Eigenschaft ist wesentlich für die Beweisssuche und die Etablierung der Schnittelimination.
• Syntaktische Schnittelimination: Die Arbeit liefert einen Beweis für die Zulässigkeit der Schnittregel. Der Beweis stützt sich auf eine doppelte Induktion: eine auf der DHS-Komplexität der Schnittformel (ein Komplexitätsmaß relativ zur Ankündigungsfolge) und eine andere auf der Summe der Höhen der Herleitungen der Prämissen.
• Korrektheit und Vollständigkeit: Der Kalkül wird bezüglich der Standard-Kripke-Semantik von PAL als korrekt und vollständig bewiesen. Der Vollständigkeitsbeweis umfasst die Herleitung aller Hilbert-stil-Axiome von PAL, einschließlich der Reduktionsaxiome, innerhalb des Rahmens der dynamischen Hypersequenzen.
• Unterformel-Eigenschaft: Als Konsequenz der Schnittelimination genießt der Kalkül die Unterformel-Eigenschaft, wodurch sichergestellt wird, dass jede Formel in einer Herleitung eine Unterformel des Endsequents oder einer darin vorkommenden Ankündigung ist.

Bedeutung und Behauptungen
Die Autoren behaupten, dass diese Arbeit einen bedeutenden Schritt darstellt, um die Lücke zwischen der semantischen Dynamik von PAL und ihrer syntaktischen Beweistheorie zu schließen. Durch die Verwendung dynamischer Hypersequenzen erfasst das System den dynamischen Charakter der Logik durch rein strukturelle Mittel und vermeidet die Notwendigkeit expliziter semantischer Elemente (wie Markierungen für Welten) oder einer Reduktion auf statische Logik.

Die Arbeit behauptet, dass $DHSPAL$ nach Kenntnis der Autoren der erste Kalkül für PAL ist, der gleichzeitig Folgendes erfüllt:

1. Zulässigkeit aller strukturellen Regeln (einschließlich Kontraktion).
2. Invertierbarkeit aller logischen Regeln.
3. Syntaktische Schnittelimination.
4. Eine genuine Unterformel-Eigenschaft.

Die Autoren schließen daraus, dass der Rahmen der dynamischen Hypersequenzen ausdrucksstark und robust genug ist, um als Grundlage für die Entwicklung von Sequenzenkalkülen für breitere Klassen dynamischer epistemischer Logiken zu dienen, die verschiedene Arten von Informationsupdates beinhalten. Sie schlagen vor, dass zukünftige Arbeiten die Entscheidbarkeit, Interpolation und Komplexitätsanalyse innerhalb dieses Rahmens untersuchen könnten.