Modallogik

aus Freepedia, der freien Wissensdatenbank

Unter Modallogiken versteht man solche Logiken, die zusätzlich zu den aus der Aussagenlogik und Prädikatenlogik bekannten Konstrukten Operatoren enthalten, mit denen man über Modalitäten wie "möglich" und "notwendig" (alethische Logik), "immer (in der Zukunft)" und "manchmal/irgendwann (in der Zukunft)" (temporale Logik) etc. sprechen kann.

So lassen sich nicht nur Sätze wie "morgen wird es regnen" formulieren, sondern auch Sätze wie "möglicherweise wird es morgen regnen, möglicherweise auch nicht".

Die Sprache der unimodalen Modallogik

Die Sprache der unimodalen Modallogik enthält alle aussagenlogischen Formeln sowie zusätzlich alle Formeln der Gestalt <math>\Box\phi</math> ("box phi", phi ist notwendig) und <math>\Diamond\phi</math> ("diamond phi", phi ist möglich) für alle modallogischen Formeln <math>\phi</math>.

Dabei kann Box durch Diamond definiert werden und umgekehrt:

• <math>\Box\phi\leftrightarrow\lnot\Diamond\lnot\phi</math> und
• <math>\Diamond\phi\leftrightarrow\lnot\Box\lnot\phi</math>

Zwei unmittelbare Folgerungen daraus sind die an die De Morganschen Regeln erinnernden Sätze:

• "Es ist nicht notwendig, dass X" ist äquivalent zu "Es ist möglich, dass nicht X", und
• "Es ist nicht möglich, dass X" ist äquivalent zu "Es ist notwendig, dass nicht X".

Die Kripke-Semantik der unimodalen Modallogik

In der nach Saul Kripke benannten Interpretation der Modallogik betrachtet man alle "logisch möglichen Welten". Ein Kripke-Modell besteht aus einer Menge solcher Welten, einer Zugänglichkeitsrelation zwischen ihnen und einer Interpretation der Aussagenvariablen in jeder einzelnen der Welten.

Die Wahrheit einer Formel in einer möglichen Welt ist dann wie folgt definiert: aussagenlogische Tautologien gelten in allen Welten, eine Formel gilt in einer Welt genau dann, wenn ihre Negation nicht gilt, und eine Formel der Gestalt <math>\Box\psi</math> gilt in einer Welt w genau dann, wenn <math>\psi</math> in jeder von w aus zugänglichen Welt w' gilt.

Will man die Modallogik gemäß dieser Semantik axiomatisieren, so lässt sich dies durch die Einführung des Axiomenschemas K und der Schlussregel der Nezessisierung realisieren:

• Axiomenschema K: <math>\Box(\phi \rightarrow \psi) \rightarrow (\Box\phi \rightarrow \Box\psi)</math>.
• Nezessisierungsregel: Wenn gilt: <math>\vdash\psi</math> (d.h. wenn <math>\psi</math> ableitbar ist), so gilt auch <math>\vdash \Box\psi</math> (<math>\Box\psi</math> ist ableitbar).

Darüber hinaus benötigt man als Schlussregeln den Modus ponens und die universelle Substitution.

Je nach Anwendung und intendierter Semantik kann man weitere Axiomenschemata hinzufügen, etwa:

1. <math>\Box\phi \rightarrow \phi</math> (T)
2. <math>\Box\phi \rightarrow \Box\Box\phi</math> (4)
3. <math>\Diamond\phi \rightarrow \Box\Diamond\phi</math> (5)
4. <math>\phi \rightarrow \Box\Diamond\phi</math> (B)
5. <math>\Box\phi \rightarrow \Diamond\phi</math> (D)

Diese Schemata entsprechen in der obigen Reihenfolge der Reflexivität, Transitivität, Euklidizität (Linkskomparativität), Symmetrie und Serialität (Linkstotalität) der Zugänglichkeitsrelation.

Eine der am häufigsten verwendeten Modallogiken, S5, basiert auf den Axiomenschemata K, T und 5. Auch andere Kombinationen der erwähnten Axiomenschemata sind sinnvoll und gebräuchlich.

Zur Geschichte der Modallogik

Die frühesten formalen Ansätze zu einer Modallogik finden sich bereits bei Aristoteles in der ersten Analytik. Dort werden zu jedem kategorischen Syllogismus auch die modallogischen Varianten untersucht. Im Mittelalter untersucht u.a. Duns Scotus modallogische Begriffe. Gottfried Wilhelm Leibniz prägt den Ausdruck "mögliche Welt", der für die Entwicklung der modallogischen Modelltheorie wieder bedeutsam werden soll.

Die ersten modallogischen Kalküle in moderner Präsentationsform finden sich in Clarence Irving Lewis Werken "A Survey of Symbolic Logic (1918) und in der zusammen mit C. H. Langford verfassten "Symbolic Logic" (1932). In letzterem präsentieren die Autoren fünf Systeme (S1 bis S5), bei denen sie sich nicht entscheiden wollen, welches davon die Prinzipien modallogischen Folgerns am besten ausdrückt. Im Jahr 1933 zeigt Kurt Gödel eine enge Verbindung zwischen S4 (spezifiziert durch die obigen Axiome T, K und 4) und der intuitionistischen Logik auf. Rudolf Carnaps Buch "Meaning and Necessity" (1947) stellt den Versuch dar, den Begriff der Intension mit modallogischen Mitteln zu rekonstruieren. 1959 entwickelt Saul Kripke eine Semantik für verschiedene modallogische Systeme.