In dieser Sitzung haben wir uns mit dem Beweisverfahren der semantischen Bäume im Kontext der Modallogiken beschäftigt.
Beweise mit semantischen Bäumen
Angenommen wir wollen zeigen, dass \(A\) allgemeingültig ist. Die generelle Idee hinter diesem Beweisverfahren ist zu widerlegen, dass es eine Interpretation der gegebenen Formel \(A\) gibt, in der diese negiert wahr ist. Falls dies glückt, muss die Formel \(A\) selbst in jeder Interpretation wahr sein. Damit ist sie allgemeingültig.
Der erste Schritt ist also, anzunehmen, dass \(\neg A\) gilt in einer gegebenen Welt gilt. Wir schreiben dafür:
\[ \neg A, 1 \]
Die Welten schreiben wir einfach als Zahlen: für jede Welt genau eine Zahl 1, 2, 3 …
Beachte: wäre \(A\) allgemeingültig, dürfte es keine Welt geben in der \(\neg A\) gilt, denn \(A\) würde in jedem Modell an jeder Welt gelten.
Nun analysieren wir, was es heißt, dass \(\neg A\) in der Welt 1 gilt. Folgende Regeln stehen uns dafür zur Verfügung:
sowie
sowie
und die folgenden beiden Regeln für negierte modale Formeln:
Wie analysieren wir nicht-negierte Formeln? Für Junktoren benutzen wir die Regeln, die wir schon aus der Aussagenlogik kennen:
sowie
Die interessante Fälle sind die beiden für Modaloperatoren. Man nehme etwa an, wir hätten \(\Box A, i\) gegeben. Das heißt, dass \(A\) in allen von \(i\) aus erreichbaren Welten \(j\) gilt. Wir schreiben \(iRj\) um auszudrücken, dass \(j\) von \(i\) aus erreichbar ist.
Damit ist die Regel für \(\Box\) die folgende:
Falls wir \(\Diamond A, i\) vorliegen haben, heißt dies, dass \(A\) in einer erreichbaren Welt gelten muss. Die Regel sieht wie folgt aus:
Die Regel hat folgende wichtige Einschränkung: die erreichbare Welt in der \(A\) gilt, darf im selben Ast des Baumes noch nicht erwähnt worden sein. Wir wissen ja über die erreichbare Welt \(j\) nur eines: nämlich, dass \(A\) in ihr gilt. Wäre \(j\) schon im selben Ast vorliegend, dann wüssten wir über \(j\) bereits mehr.
Beispiel1. Im folgenden Beispiel wird gezeigt, dass \(\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)\) allgemeingültig ist.
Wie wir das schon aus der Aussagenlogik kennen, werden Äste, die Widersprüchlichkeiten aufweisen mit \(\otimes\) markiert. Das heißt, diese Äste schließen: sie stellen keine legitimen Analysen unserer Ausgangsformel dar. Sobald der letzte Ast schließt, sind uns die Kandidaten ausgegangen, eine Interpretation unserer Ausgangsformel zu finden: unser Widerlegungsverfahren ist erfolgreich und die Ausgangsformel ist allgemeingültig. Dies ist die Situation im Beispiel: der linke Ast schließt, da sowohl \(p\) also auch \(\neg p\) in Welt 2 gelten: dies ist widersprüchlich. Der rechte Ast schließt, da sowohl \(q\) als auch \(\neg q\) in Welt 2 gelten.
Im Falle, dass ein vollständiger Ast nicht schließt, ist die Widerlegung nicht erfolgreich und unsere Ausgangsformel ist nicht allgemeingültig. Zur Erinnerung: ein vollständiger Ast ist von der Art, dass keine Regel mehr angewandt werden kann, die einen neuen Eintrag auf dem Ast produziert.
Hier ist ein zweites Beispiel.
Beispiel 2.
Nun ein Beispiel, in dem ein Ast nicht schließt:
Beispiel 3.
Beachte, dass der rechte Ast vollständig ist: keine Regel kann mehr auf ihn angewandt werden, die einen neuen Eintrag produziert.
Wir gehen wir vor, wenn wir nachweisen wollen, dass \(A\) eine logische Konsequenz aus der Prämissenmenge \(\Gamma\) ist? Genauso wie zuvor, nur dass wir noch zusätzlich zu jedem Zeitpunkt \(B, i\) in einen Ast des Baumes einfügen dürfen, für \(B \in \Gamma\) und beliebiges \(i\). Um zu widerlegen, dass \(A\) aus \(\Gamma\) folgt, wollen wir ja ein Modell finden, in dem \(\neg A\) an einer Welt gilt und in dem jede der Prämissen in jeder Welt gilt.
Stärkere Modallogiken
Die Logik K, die wir bisher kennengelernt haben, ist etwas schwach. Abhängig davon wie wir \(\Box\) interpretieren (Notwendigkeit, Wissen, Obligationen, etc.), drücken etwa folgende Formeln Prinzipien aus, die intuitive wären, die jedoch in K nicht allgemeingültig sind:
Prinzip
Name
Alethisch
Epistemisch
Doxastisch
Deontisch
\(\Box A \rightarrow A\)
T (auch M)
\(\checkmark\): notwendig→aktual
\(\times\)
\(\times\)
\(\times\)
\(\Box A \rightarrow \Diamond A\) bzw. \(\Box A \rightarrow \neg \Box \neg A\)
Wir benutzen folgende Interpretationen (die selbstverständlich noch weiter verfeinert werden können):
alethisch
epistemisch
doxastisch
deontisch
\(\Box A\)
Es ist notwendig, dass \(A\).
Ich/Akteur \(X\) weiß, dass \(A\).
Ich/Akteur \(X\) ist der Überzeugung, dass \(A\).
Es ist obligatorisch, dass \(A\).
\(\Diamond A\)
Es ist möglich, dass \(A\).
Ich/Akteur \(X\) weiß nicht, dass \(\neg A\). Oder: \(A\) ist mit meinem/\(X\)s Wissen konsistent.
Ich/Akteur \(X\) bin/ist nicht der Überzeugung, dass \(\neg A\). Oder: \(A\) ist mit meinen/\(X\)s Überzeugungen konsistent.
\(A\) ist erlaubt.
Etwa im Bereich der epistemischen/doxastischen Logik, hängt es davon ab, wie idealisiert der zugrundeliegende Begriff des Wissens/der Überzeugungen ist, welche Prinzipien man akzeptieren will. Für einen sehr idealisierten Begriff des Wissens macht es etwa Sinn, positive und negative Introspektion anzunehmen. Für deskriptiv adäquatere Versionen, ist man evtl. gewillt, nicht an diesen Prinzipien festzuhalten. Ähnlich im Bereich der deontischen Logiken: unsere Normsysteme (etwa ethische Normen) sind nur als Idealisierung derart, dass sie nicht zu normativen Konflikten Anlass geben.
Wie können wir Modallogiken definieren, die solche Prinzipien verwirklichen? Die Grundlegende Idee ist, mit Rahmenklassen zu arbeiten, in denen die Erreichbarkeitsrelation bestimmte Eigenschaften erfüllt. Hier ist eine Übersicht für obige Prinzipien:
Prinzip
Axiom
Anforderung an die Erreichbarkeitsrelation
Definition
T (auch: M)
\(\Box A \rightarrow A\)
reflexiv
\(\forall x: xRx\)
D
\(\Box A \rightarrow \Diamond A\)
seriell
\(\forall x \exists y xRy\)
4
\(\Box A \rightarrow \Box \Box A\)
transitiv
\(\forall x \forall y \forall y: xRy \wedge yRz \Rightarrow xRz\)
5
\(\Diamond A \rightarrow \Box \Diamond A\)
euklidisch
\(\forall x \forall y \forall z: xRy \wedge xRz \Rightarrow y R z\)
B
\(A \rightarrow \Box \Diamond A\)
symmetrisch
\(\forall x \forall y: xRy \Rightarrow yRx\)
Warum funktieren diese Charakterisierungen? Betrachte etwa T. Angenommen unsere Erreichbarkeitsrelation \(R\) ist seriell. Damit, falls \(\Box A\) in einer Welt \(w\), so gilt in allen erreichbaren Welten \(A\). Da \(R\) seriell ist, gilt \(A\) auch in \(w\). Versuchen Sie nachzuvollziehen, warum dies auch in anderen Fällen gilt.
Rahmenklassen, die obigen Anforderungen genügen charakterisieren Modallogiken, die stärker sind als K. In obigen Fällen sind diese genau genannt, wie die zugrundeliegenden Prinzipien. Etwa, ist die Logik T (auch M) ist charakterisiert durch reflexive Rahmen. Eine Formel ist eine T-Tautologie, falls sie in allen Modellen mit reflexiven Erreichbarkeitsrelation gilt. Eine Formel \(A\) ist eine T-Konsequenz einer Prämissenmenge \(\Gamma\) falls in jeder Modell \(M\) mit reflexiven Rahmen und jeder Welt \(w\) in \(M\) gilt: falls \(M,w \models B\) für alle \(B \in \Gamma\) dann auch \(M,w \models A\). Analog wird für die Logiken KD (K plus T), K4 (K plus 4), K5 (K plus 5), B (K plus B), S4 (T plus 4), und S5 (T plus 5) vorgegangen.
Die Regeln für das Baumkalkül können auch in einfacher Weise ergänzt werden.
Etwa ergänzen wir die K-Regeln durch
um ein Beweissystem für T zu definieren.
Beispiel 4.
Folgende Regeln fügen wir für KD hinzu
:
Hierbei gilt die Einschränkung, dass für alle \(k\), \(irk\) noch nicht auf demselben Ast auftaucht und zusätzlich, dass \(j\) noch nicht auf demselben Ast auftaucht.
Beispiel 5.
In KD kann man in Beweisen unendlich lange Äste erzeugen.
Beispiel 6.
Dieser Ast schließt nie. Er gibt uns Aufschluss darüber, wie ein Modell aussieht in dem \(\Box p \rightarrow p\) nicht gilt (in einer Welt):
wobei \(v(p,w_1) = 0\), \(v(p,w_2) = 1\) und ansonsten ist \(v\) beliebig. Offensichtlich ist diese Modell nicht minimal. Es gibt ein Modell mit nur 2 Welten in dem \(\Box p \rightarrow p\) nicht gilt.
Übung. Bestimmen Sie ein minimales Modell \(M\), so dass in einer Welt \(w\) in \(M\) gilt \(M,w \models \neg(\Box p \rightarrow p)\).
Für die Logik K4 fügen wir folgende Regel hinzu:
Die Logiken S4 und S5 haben folgende interessante Eigenschaften:
Übungen
Übung 1. (\(\star\)) Zeigen Sie, dass \(\Box p \rightarrow \Box \Box p\) in S4 allgemeingültig ist. Beachten Sie, dass im Beweissystem für S4 die Regeln R-T und R-4 zu den Regeln von K hinzugefügt werden.
Übung 2. (\(\star\)) Für die Logik K5 fügen wir folgende Regel zu den Regeln von K hinzu:
Beweisen Sie \(\Diamond p \rightarrow \Box \Diamond p\) in diesem System.
Übung 3. (\(\star\)) Zeigen Sie im Beweissystem von K, dass \(\Box (p \vee q) \rightarrow (\Box p \vee \Box q)\) nicht allgemeingültig ist.
Übung 4. (\(\star\)) Beweisen Sie, dass \(\Diamond (p \vee q) \rightarrow (\Diamond p \vee \Diamond q)\) in K allgemeingültig ist.
Übung 5. (\(\star\)) Überprüfen Sie mit einem semantischen Baum, ob \(\Diamond \Box \Diamond p \rightarrow \Box \Diamond \Diamond p\) n S5 gilt. Beachten Sie, dass das zugrundeliegende Beweissystem das Beweissystem von K um die Regeln R-T und R-5 stärkt.
:
