Während die Typenlogik die Prädikatenlogik erster Stufe dadurch
erweitert, daß Objekte höherer Ordnung in dem zugrundeliegenden
Universum (wie zum Beispiel Mengen von Objekten) mitbetrachtet werden, besteht
die Modallogik [HC68] in einer Erweiterung der Prädikatenlogik um
einen neuen Operator 
, dem gewisse logische Eigenschaften
zugeschrieben werden. Auch diese Erweiterung hat in der
Wissensrepräsentation mannigfache Anwendungen gefunden. Einer davon werden
wir im nächsten Kapitel bei der Behandlung der autoepistemischen Logik (siehe Abschnitt 3.8)
begegnen.
Formeln der Modallogik sind also wie die der Prädikatenlogik aufgebaut, nur
ist als zusätzlicher einstelliger Operator beim Aufbau beteiligt.
Die intendierte Bedeutung einer Formel der Gestalt 
variiert je
nach Anwendung. Man liest sie zB. als ``notwendigerweise 
''.
Zu gibt es einen dualen Operator 
, der sich in
definitorischer Weise als 
einführen
läßt, was dann als ``möglicherweise '' gelesen werden kann.
Die Semantik der Modallogik läßt sich mittels möglicher Welten charakterisieren [Kri59, Kri63]. Eine mögliche Welt ist eine Interpretation im Sinne der Prädikatenlogik, mittels derer den Formeln Wahrheitswerte zugewiesen werden. Eine Menge möglicher Welten hat im Vergleich zu einer Menge von Interpretationen jedoch eine zusätzliche Struktur, und zwar in Form von Beziehungen unter den Welten.
Man denke etwa an die uns umgebende Welt als eine solche mögliche Welt, die
sich jedoch im Verlauf einer Minute in vieler Hinsicht ändert (zB. sind die
Wolken ein Stück weitergezogen, das vorbeifahrende Auto ist inzwischen einen
Kilometer entfernt, der Vogel sitzt in einem anderen Baum usw.). Wir
könnten also im Verlauf von zehn Minuten zehn verschiedene mögliche Welten
voneinander unterscheiden. Dabei besteht die Beziehung unter diesen zehn
Welten darin, daß die zweite Welt 
aus der ersten 
, die
dritte 
aus der zweiten usw. hervorgegangen bzw.
erreichbar ist.
Die Beziehungen unter den möglichen Welten wird mathematisch als
eine Relation 
, der
Erreichbarkeitsrelation,
formal repräsentiert. Im Beispiel ergäbe sich also 
für 
. Wenn wir bedenken, daß in diesem Beispiel
ebenfalls aus 
(über 
) hervorgegangen ist, so
macht es hier Sinn, den transitiven Abschluß von zu
bilden, so daß 
für 
gilt.
Formal ergibt sich die Semantik einer Modallogik nun als ein Tupel 
, genannt eine
Kripkestruktur.
ist die Menge der Welten, 
ist die sogenannte
aktuelle Welt,
ist eine Funktion, die jeder Welt 
eine Interpretation
(im üblichen Sinne) zuordnet, und ist die
besprochene Relation. Dann erhält den Wert wahr, wenn
in allen aus 
erreichbaren Welten wahr ist, wie es die
Abbildung 2.37
Abbildung 2.37: gilt in allen von der Welt aus erreichbaren Welten
(für den Fall einer transitiven Erreichbarkeitsrelation) illustriert. 
erhält den Wert wahr, wenn in
mindestens einer erreichbaren Welt wahr ist, was die Abbildung 2.38
Abbildung 2.38: gilt in einer von der Welt aus erreichbaren Welt
(wieder für den Fall einer transitiven Erreichbarkeitsrelation) illustriert. Hierbei sprechen wir kurz von dem Wahrheitswert einer Formel in
einer Welt 
, obwohl wir eigentlich den Wahrheitswert in der Interpretation
meinen. Da letztere aber vermöge durch die Welt
eindeutig bestimmt ist, erweist sich diese Sprechweise als gerechtfertigt.
Eine Kripkestruktur heißt ein
Kripkemodell für
eine modallogische Formel , wenn sie in dieser Struktur den Wert wahr
erhält.
Wie wir vorher gesehen haben, macht es Sinn, für bestimmte
Eigenschaften, wie in dem genannten Beispiel die Transitivität, zu
verlangen. Je nach den hierbei geforderten Eigenschaften ergeben sich dann
verschiedene Modallogiken. Die Tabelle 2.2 zeigt einige der
gebräuchlichsten Eigenschaften. Die Tabelle 2.3 listet die
gebräuchlichsten Modallogiken zusammen mit den für ihre jeweilige
Erreichbarkeitsrelation geforderten Eigenschaften. Diese Eigenschaften lassen
sich auch syntaktisch mit Axiomen charakterisieren, die bei den entsprechenden
Logiken zusätzlich gefordert werden. Tabelle 2.4 zeigt vier
solcher Axiome, mit denen die in Tabelle 2.3 aufgeführten
Modallogiken auf die in der letzten Spalte angegebenen Weise charakterisiert
werden können. In jedem dieser Fälle tritt neben diesen zusätzlichen
Axiomen noch die zusätzliche Schlußregel
So besteht etwa S4 aus den Axiomen und Schlußregeln der klassischen Prädikatenlogik, dieser zusätzlichen Regel und den zusätzlichen Axiomen A1, A2 und A3.
| A1 | Notwendigkeit |  |
| A2 | Distributivität |  |
| A3 | Positive Introspektion |  |
| A4 | Negative Introspektion |  |
Die Modallogiken S4 und S5 spielen besonders bei der Formalisierung des
Schließens über das Wissen und das schwache S4 und S5 bei der
Formalisierung des Schließens über das Glauben eine wichtige Rolle
(siehe Abschnitt 4.2.3). In beiden und anderen Fällen ist es zudem
möglich, den modalen Operator als zweistelligen Operator
aufzufassen, wobei die erste Stelle ein Term ist, der etwa einen Akteur
bezeichnet, der etwas weiß oder glaubt. Anstelle von 
schreibt man dann auch oft 
. In diesem Fall muß auch die
Erreichbarkeitsrelation dieses zusätzliche Argument berücksichtigen, so
daß wir für jeden Akteur ein eigenes 
erhalten.
In der zuletzt beschriebenen Form spielt die Modallogik auch eine große
Rolle als Formalismus für Beweise über Programme in der Informatik,
genannt dynamische Logik. In
dieser Anwendung steht 
für ein Programm und beschreibt die
Relation, mit der Welten, dh. in diesem Fall Zustände einer abstrakten
Maschine, mittels dem Programm in Beziehung gesetzt werden.
Für Modallogiken sind eine Reihe von Deduktionsmechanismen entwickelt worden. Wir nennen insbesondere den auf der Konnektionsmethode basierenden Ansatz [Wal90] sowie die Technik der Transformation in die klassische Prädikatenlogik [Ohl91].
Christoph Quix, Thomas List, René Soiron
impliziert 
implizieren 
