Kripkes Completeness Theorem (K&L)

Saul Kripke – A completeness theorem in modal logic (1959)

Der Kontext:

Leibniz bezeichnete diese unsere Welt als die beste aller möglichen Welten. Er hatte noch eine Reihe weiterer Dinge über mögliche Welten zu sagen, diese wurden aber großteils über Bord geworfen (z.B. jede mögliche Welt ist maximal, d.h. sie enthält alles, was sie enthalten kann ohne widersprüchlich zu werden; mögliche Welten sind gegenseitig ausschließend, d.h. ein Element aus einer Welt existiert nur in dieser, nicht auch noch in anderen Welten). (Mates) Die Idee jedoch, dass verschiedene Welten möglich gewesen wären, (aus denen Gott die beste gewählt und realisiert hat) hat sich für die Logik als sehr praktisches Instrument erwiesen.

In der Logik hatte sich Jahrhunderte lang relativ wenig bewegt. Die aristotelische Logik wurde natürlich weiter entwickelt, jedoch nicht ersetzt. Logik wurde als die Kunst des Denkens betrachtet (so lautet auch der Titel von Arnaulds und Nicoles Port Royal-Logik aus dem 17. Jahrhundert). Erst mit Boole, Frege und Russell kam es im Lauf des 19. und frühen 20. Jahrhunderts zur Entwicklung einer mathematischen Logik.

Die Aussagen- und Prädikatenlogik stellt ein System für formale Ableitungen dar. Übersetzen wir Sätze korrekt in diese logische „Sprache“, können wir somit erkennen, welche Schlüsse gültig gezogen werden können. Wittgensteins Wahrheitstafeln ergänzen diese durch eine auf einen Blick erfassbare Semantik.

Der Nachteil des Systems lag darin, dass eine Reihe von Sätzen nicht formuliert werden konnten, und zwar alle jene, die nicht eine Beschreibung der Welt darstellten, sondern Spekulationen im Gegensatz zu Sicherheiten ausdrückten. Beispiele:

Es ist möglich, dass es morgen regnet.
Der Bus müsste gleich kommen.
Diese Tulpe könnte orange werden.
Tulpen sind notwendigerweise Pflanzen.
Wenn er ein Junggeselle ist, muss er männlich und unverheiratet sein.

C.I. Lewis gilt als Begründer der Modallogik. Er wollte ursprünglich eine Möglichkeit finden, zwischen notwendiger und kontingenter Wahrheit zu unterscheiden. Auf ihn gehen die Systeme S4 und S5 zurück. (Fitch) Diese Systeme sind syntaktisch, d.h. sie geben Spielregeln für korrektes Schließen vor. Für S4 gelten (zusätzlich zu allen Regeln der Aussagenlogik):

- wenn p ein aussagenlogisches Theorem ist, ist □p ein modallogisches Theorem
- □p -> p
- □(p->q) ->(□ p-> □q)
- □p -> □□p

Und für S5 zusätzlich zu allen Regeln für S4 noch:

- ◊p ->□◊p

Carnap unternahm als erster die modell-theoretische Untersuchung logischer Konsequenzbeziehungen in der Modallogik. Er geht von Zustandsbeschreibungen S aus, die aus einer Menge atomarer Sätze bestehen und ihrerseits in einer Menge M zusammengefasst sein können. Er definiert einen Satz p als genau dann wahr, wenn er Element von S ist, und als notwendig wahr, wenn er in jeder Zustandsbeschreibung S’, die Element von M ist, wahr ist. Dieser Satz enthält eine Reihe von Problemen, die Kripke mit seiner möglichen Welt-Methode repariert. (Zalta)

Logische Systeme werden wie folgt beurteilt (Fitch):

- Ein System, in dem keine Aussage p abgeleitet werden kann, wenn gleichzeitig eine Aussage ~p abgeleitet werden kann, ist konsistent.
- Ein System, in dem alle Theoreme, die logisch aus den Axiomen des Systems abgeleitet werden können, wahr sind, ist widerspruchsfrei.
- Ein System, in dem alle logischen Wahrheiten des Systems aus den Axiomen und Regeln des Systems abgeleitet werden können, ist vollständig.

Alfred Tarski hat den Begriff der logischen Wahrheit für die Prädikatenlogik als „Befriedigung“ oder „Erfüllung“ definiert: Eine Formel A ist hinsichtlich einer Interpretation <D,f> genau dann wahr, wenn diese Formel durch die Interpretation erfüllt wird, und sie ist logisch wahr (d.h. gültig) genau dann, wenn sie von allen Interpretationen (dieser Sprache) erfüllt wird. (Fitch)

Das ist für die Aussagen- und Prädikatenlogik gut und schön, in der Modallogik, wo es um Notwendigkeit und Möglichkeit geht, ist einiges an Anpassungen nötig. Diese hat Kripke vorgenommen, indem er mögliche Welten eingeführt hat, in denen Dinge nicht mehr einfach wahr oder falsch sind, sondern wahr oder falsch in Bezug auf eine bestimmte mögliche Welt.

In „A Completeness Theorem in Modal Logic“ entwickelt er also eine Semantik für die Modallogik (und zwar für S5). Folgen wir ihm Schritt für Schritt:

Kripke geht aus von S5, ergänzt durch den Existenz- und den Allquantor und das Gleichheitszeichen, und nennt dieses System S5*=. Er verwendet die üblichen Konnektive und legt noch 3 Axiome und Ableitungsregeln fest (siehe Beiblatt).

Wir nehmen jetzt eine Domäne D an, die eine abzählbare Anzahl Elemente enthält. Eine Formel A lässt sich durch die Elemente aus D erfüllen, d.h. ich kann für jede freie Variable der Formel A ein Element aus D einsetzen und diesen einen Wahrheitswert T (wahr) oder F (falsch) zuweisen. So eine „ausgefüllte“ Formel bezeichnet er als G und eine Sammlung von Gs als K. Ein Modell besteht somit aus <G, K>.

Die Formel A ist genau dann gültig in D, wenn A in jedem Modell von A in D gilt.
Die Formel A kann in D genau dann erfüllt werden, wenn A in mindestens einem Model von A in D gilt.
Die Formel A ist genau dann universell gültig, wenn A in jeder Domäne gilt, die nicht leer ist.
Als Grundlage dafür nennt er, dass ein Satz notwendig ist, wenn er in allen möglichen Welten wahr ist.

In der Modallogik möchten wir nicht nur wissen, ob ein Satz in der tatsächlichen Welt gilt, sondern ob er in allen möglichen Welten gilt. Deshalb gehen wir nicht nur von G aus, sondern von einer Reihe von erfüllten Formeln, K. Die Elemente aus D können mehrfach in eine Formel, also z.B. in G ebenso wie in H und I eingesetzt werden, dieselben Namen bezeichnen hierbei als starre Bezeichner (rigid designators) immer dieselben Objekte.

Für seinen Vollständigkeitsbeweis geht Kripke von Beths semantischen Tableaux oder Baumstrukturen aus. Für diese gibt es eine Reihe von Regeln (siehe Beiblatt). Ein Ast des Baumes / Spalte des Tableaus ist „geschlossen“, wenn das Ergebnis ein Widerspruch zur Prämisse (d.h. also ‚falsch’) ist.

Jetzt kommt Kripke zu seinen Theoremen:

Theorem 1: B folgt semantisch aus A₁ , A₂ ,…A_n genau dann, wenn die Konstruktion in der linken Spalte mit A₁ , A₂ ,…A_n beginnt und B in der rechten Spalte geschlossen ist. (d.h. wenn A₁ , A₂ ,…A_n wahr ist, und falsch ist, dass B falsch ist).

Als Beweis bietet er 2 Lemmata an: Lemma 1: Wenn eine Konstruktion mit A₁ , A₂ ,…A_n auf der linken Seite beginnt und B auf der rechten Seite geschlossen ist, dann folgt B semantisch aus A₁ , A₂ ,…A_n .

Der Beweis dazu: Für eine reductio ad absurdum nimmt Kripke an, dass B nicht semantisch aus A₁ , A₂ ,…A_n folgt.

Er schreibt jetzt also:

wahr falsch_________ A₁ , A₂ ,…A_n ->B

A₁ , A₂ ,…A_n B

Und geht die Liste der Tableau-Regeln (siehe Beiblatt) durch, woraus sich ergibt, dass die Konstruktion geschlossen ist und jede alternative Menge (bzw. jede mögliche Welt) in K ein Tableau enthält, das entweder eine Formel in beiden Spalten hat (sich also selbst widerspricht) oder a=a in der rechten Spalte (also sagt, dass a nicht gleich a ist). Es ist somit falsch, dass B nicht aus A₁ , A₂ ,…A_n folgt; also folgt B aus A₁ , A₂ ,…A_n .

Lemma 2: Wenn die Konstruktion mit A₁ , A₂ ,…A_n auf der linken Seite beginnt und B auf der rechten nicht geschlossen ist, dann folgt B nicht semantisch aus A₁ , A₂ ,…A_n .

Hier geht der Beweis umgekehrt, verglichen mit dem Beweis für Lemma 1: Die Konstruktion ist nicht geschlossen, also gibt es mindestens eine Menge von Tableaux, die nicht geschlossen ist. Das ist die Menge, die uns interessiert. Wir machen durch Zuweisungen von freien Variablen aus D ein Modell <G, K> von A₁ , A₂ ,…A_n ->B in D. Jede Formel in der linken Spalte wird als wahr angesehen, jede in der rechten Spalte als falsch. Da die Konstruktion nicht geschlossen ist, können Formeln nur entweder links oder rechts stehen. Nach Il führt „a=b“ links zum Ersetzen von a durch b; steht „a=b“ rechts, sind die Variablen unterschiedlich. Wenn ~C links steht, ist C falsch. Wenn □C links steht, steht C in der linken Spalte jedes Tableaus dieser Menge, wodurch C dann für jedes Element von K wahr ist und □C wahr ist. Wenn □C rechts steht, steht C in mindestens einem Tableau dieser Menge rechts und ist daher in mindestens einem Element von K falsch. Daher ist □C falsch.

Da A₁ , A₂ ,…A_n im Haupttableau links stehen, sind sie in G wahr, da B rechts steht, ist B in G falsch. Daher ist A₁ , A₂ ,…A_n ->B falsch und im Modell <G,K> nicht gültig – und B folgt somit nicht semantisch aus A₁ , A₂ ,…A_n .

Theorem 2: Wenn eine Formel in einer nicht leeren Domäne erfüllt werden kann, ist sie in einem Modell <G, K> in einer Domäne D gültig, wenn D und K beide entweder eine endliche Zahl oder abzählbare Elemente besitzen. Wenn eine Formel in jeder endlichen oder abzählbaren Domäne gültig ist, ist sie universell gültig.

Beweis: Der zweite Satz folgt aus dem ersten. Wenn eine Formel B in einer Domäne erfüllbar ist, ist ~B nicht universell gültig. Nach Theorem 1 ist ~B falsch und nach Lemma 2 ist ~B ungültig und B somit gültig. Sowohl D und K sind jedoch endlich und abzählbar (siehe Regeln nach denen Tableaux erstellt werden).

Theorem 3: Wenn eine Formel, die kein Gleichheitszeichen enthält, in einer nicht leeren Domäne erfüllt werden kann, ist sie in einem Modell <G, K> in einer Domäne D gültig, wenn K endlich oder abzählbar ist und D abzählbar ist. Wenn sie in jeder abzählbaren Domäne gültig ist, ist sie universell gültig.

Beweis: Dieses Theorem folgt aus Theorem 2 und dem folgenden Lemma:

Lemma 3: Wenn eine Formel A, die kein Gleichheitszeichen enthält, in einem Modell <G, K> in einer nicht leeren Domäne D gültig ist und D eine Teilmenge von D’ ist, dann ist A in einem Modell <G’, K’> in D’ gültig, wenn K und K’ gleichmächtig sind.

Beweis: Wir nehmen jetzt eine neue „Welt“ nach Formel A, nämlich H (ein Element aus K) und parallel dazu H’. H’ macht dieselben Zuweisungen aus S’ wie H aus S, wobei S’ alle n-Tupel von S enthält sowie jene n-Tupel, die sich ergeben, wenn man Elemente aus D in D’ durch andere ersetzt. Wir bekommen somit K’ indem wir jedes H aus K durch H’ ersetzen. Daraus ergibt sich, dass A in <G’, K’> gültig ist.

Theorem 4: Wenn in Theorem 2 und 3 die betreffende Formel kein „□“ enthält, kann K als die Einermenge von G betrachtet werden.

Beweis: Analyse der Konstruktion von K in den Theoremen 2 und 3. Die Theoreme 2 und 3 sind die modalen Analoga des Löwenheim-Skolem-Theorems.

Das Löwenheim-Skolem-Theorem besagt, dass eine Menge von Aussagen der Prädikatenlogik erster Stufe, die in einem Modell mit einer überabzählbar unendlich großen Domäne erfüllt ist, immer auch in einem Modell mit einer abzählbar unendlich großen Domäne erfüllt ist. (Wikipedia) Ohne Modalität gilt das Löwenheim-Skolem-Theorem, außerdem können wir dieses für jene Konstruktionen anwenden, in denen am Anfang in einer oder beiden Spalten unendlich viele Formeln stehen. Kripke definiert dann „charakteristische Formeln“.

Lemma 4: Wenn A die charakteristische Formel der ersten Stufe einer Konstruktion ist und B die charakteristische Formel jeglicher Stufe der Konstruktion, dann gilt in S5*=, dass B aus A folgt.

Der Beweis für Lemma 4 zeigt, dass die charakteristische Formel einer bestimmten Stufe die charakteristische Formel der nächsten Stufe impliziert. Da Implikation transitiv ist, lässt sich Lemma 4 aufstellen.

Theorem 5: Wenn A universell gültig ist, dann gilt A in S5*=.

Beweis: Da A universell gültig ist, ist ein Tableau mit A in der rechten Spalte geschlossen. Wir nehmen B als die charakteristische Formel jener Stufe an, bei der der Schließungsgrund auftritt (es zu einem Widerspruch kommt). Nach Lemma 4 können wir ~B und somit die Gültigkeit von A beweisen. Dasselbe lässt sich für alternative Mengen C und D beweisen.

Theorem 5 ist Kripkes Vollständigkeitstheorem. Aus den Theoremen 2, 3 und 5 ergeben sich folgende Zusätze:

Zusatz 1: Wenn eine Formel A aus S5*= in jeder endlichen (nicht leeren) oder abzählbaren Domäne gilt, gilt A in S5*=.

Zusatz 2: Wenn eine Formel A aus S5* in jeder abzählbaren Domäne gilt, dann gilt A in S5*.

Um zu zeigen, dass das System konsistent ist, beweist Kripke jetzt den Umkehrschluss:

Theorem 6: Wenn A in S5*= gilt, ist A universell gültig.

Beweis: Mittels eines geeigneten Tableaus können wir nachweisen, dass jedes Axiom von S5*= universell gültig ist. Wenn A und A ->B universell gültig sind, ist es B auch (siehe Regel 1). Und wenn □A nicht ungültig ist, ist es ebenfalls universell gültig (siehe Regel 2).

Theorem 7: A gilt in S5*= genau dann, wenn A universell gültig ist. Für die Aussagenlogik wird universelle Gültigkeit mittels Wahrheitstafeln ermittelt. Kripke schlägt solche Wahrheitstafeln auch für S5 vor. Aus diesen lässt sich dann ablesen, dass für Formeln aus S5 unser Begriff von Tautologie mit unserem Begriff der universellen Gültigkeit übereinstimmt.

Theorem 8: A gilt in S5 genau dann, wenn A eine Tautologie von S5 ist.

Beweis: Nachweis der Äquivalenz von Tautologieheit und universeller Gültigkeit, eingeschränkt auf S5 durch Theorem 7.

Theorem 9: A sei eine Formel aus S5, die in S5 nicht beweisbar ist. P₁ , P₂ ,…P_n seien ihre freien Aussagevariablen. Wenn (P₁) …. (P_n)A zu S5 mit Aussagequantoren hinzugefügt wird, ist das entstehende System inkonsistent.

Beweis: Da A in S5 nicht beweisbar ist, enthält nach Theorem 8 irgendeine Wahrheitstafel eine Zeile, in der A falsch ist. B sei die charakteristische Formel dieser Tafel. Nach Theorem 8 gilt, dass aus B in S5 ~A folgt. Nach S5 mit Aussagequantoren gilt (P₁ …. P_n) (B ->~A) und daher ├ (∃P₁)...(∃P_n)B ->(∃P₁)...(∃P_n)~A. Da P₁ …. P_n die freien Variablen sind, die in dieser charakteristischen Formel eingesetzt werden, widerspricht (∃P₁)...(∃P_n)~A jedoch (P₁)...(P_n)A.

Theorem 9 ist ein Vollständigkeitsergebnis für S5.

---

Saul Kripke – Definitionen, Axiome, Regeln, etc.

Symbole:
^ ............und
~ ........... nicht
□........... notwendig
(x) ......... Allquantor
= ........... ist ident mit

Definitionen:
AvB...........~(~A^~B)
A-> B ........~(A^~B)
◊A............ ~□ ~A
(∃x)A(x)..... ~(x)~A(x)

Axiome und Regeln:
A1: □A->A
A2: ~ □A->□~ □A
A3: □ (A->B)-> (□A->□B)

R1: wenn ├A und ├A->B, ├B
R2: wenn ├A, ├□A

Regeln für semantische Baumstrukturen nach Beth (wenn [fett], dann [nicht fett]) :

Regel :: wahr :: falsch

Nl :: ~A :: A
Nr :: A :: ~A

Λl :: A^B

A

B

Λr1 A^B Baum teilt sich!
A
Λr2 A^B
B

Πl (x)A(x)
A (a)
Πr (x)A(x)
A(a)

Il a=b
A(a,b) ersetzen
durch A(b,b)
Ir ---

Yl □A
A Yr □A
Neuer Hilfstableau: wahr falsch
A