Metatheorie: Zusammenfassung und Herausforderungen

Zusammenfassung

Diese Lektion schließt die der Metatheorie gewidmete Einheit ab und mit ihr den Inhalt des Kurses. Sie rekonstruiert die deduktive Kette, die von der Allgemeingültigkeit der Axiome zur Korrektheit des Kalküls führt; von den zwei Lemmata über den Peirce-Pfeil zum Lemma von Kalmár und zur Vollständigkeit für endliche Prämissenmengen; vom Zwei-Zeugen-Lemma zum Kompaktheitssatz und über ihn zur starken Vollständigkeit; und von der Klauselform zur Korrektheit und zur Widerlegungsvollständigkeit der Resolutionsmethode, wobei bei jedem Glied angegeben wird, welche Ergebnisse es verwendet und in welcher Lektion es bewiesen wird. Sie zeigt, wie die drei vorangehenden Teile des Kurses, Sprache, Deduktion und Semantik, in der Übereinstimmung von $\vdash$ und $\models$ zusammenlaufen und was jeder von ihnen dazu beiträgt; sie unterscheidet, was der Kurs bewiesen hat, von dem, was er vorausgesetzt hat, und von dem, was er offenlässt. Sie wiederholt in ihrem Abschlusstest die Fertigkeiten des Eingangstests und endet mit sechs Herausforderungen, schwieriger als die Aufgaben der Lektionen, die verlangen, die Werkzeuge mehrerer von ihnen zu verbinden.

Lernziele

Die logische Ordnung der Ergebnisse der Einheit rekonstruieren, die früheren Ergebnisse, auf die sich jedes stützt, und die Lektion, in der es bewiesen wird, angeben und die Reihenfolge von Kompaktheit und starker Vollständigkeit begründen.
Erklären, wie Sprache, Deduktion und Semantik in der Übereinstimmung von $\vdash$ und $\models$ zusammenlaufen und welches Ergebnis jeder Einheit des Kurses dafür unentbehrlich ist.
Unterscheiden, was der Kurs bewiesen hat, von dem, was er vorausgesetzt hat (die Axiomenschemata, die Grundregeln und die Induktion), und von dem, was er offenlässt (die Kosten der Entscheidung der Erfüllbarkeit und die Logik mit Quantoren).
Aufgaben lösen, die Markierungen, das Lemma von Kalmár, die uniforme Substitution, die Kompaktheit und die Resolution verbinden, und dabei jeweils die leichte Seite der Übereinstimmung benutzen.

Was die Einheit erreicht hat

Die Einheit hatte sich vorgenommen, die beiden Relationen zu vergleichen, die die vorangehenden Einheiten auf derselben Sprache aufgebaut hatten, die Ableitbarkeit $\Gamma \vdash \varphi$ und die semantische Folgerung $\Gamma \models \varphi$ , und zu beweisen, dass sie übereinstimmen. Das Ziel ist ohne Einschränkungen in den Aussagen erreicht: Beide Relationen sind für jede Prämissenmenge, endlich oder unendlich, dieselbe, und die Resolution bietet einen dritten Weg, ebenso korrekt und vollständig, um die Folgerung zu entscheiden. Die Einschränkungen liegen in den Methoden, und jede wurde an ihrer Stelle genannt: Die Vollständigkeit der ersten Lektion ist konstruktiv, aber nicht praktisch, weil sie Deduktionen so lang wie die Tafel erzeugt; die Kompaktheit sichert, dass eine Belegung existiert, lehrt aber nicht, sie zu finden; und die Resolution entscheidet, aber ihre Kosten im ungünstigsten Fall sind eine offene Frage. Mit diesen Einschränkungen lässt sich der zurückgelegte Weg als eine einzige deduktive Kette in vier Abschnitten lesen.

Korrektheit

Die Lektion über Korrektheit und Vollständigkeit begann damit, das Vokabular festzulegen: Der Kalkül ist korrekt, wenn $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , und vollständig, wenn die Umkehrung gilt, in drei Graden (schwach, für endliche Prämissenmengen und stark). Sie nahm ein zirkuläres Argument auseinander, das die Vollständigkeit „aus der Korrektheit“ gewinnen will, indem es von $\nvdash \chi$ zu $\not\models \chi$ übergeht, ein Schritt, der die Kontraposition der schwachen Vollständigkeit ist, und sie zeigte, dass die beiden Eigenschaften unabhängig sind. Danach bewies sie, dass jede Instanz von A1, A2 und A3 allgemeingültig ist, indem sie eine Belegung annahm, die sie widerlegte, und über die falsche Zeile der Implikation zu unmöglichen Werten gelangte; und durch starke Induktion über die Zeilenzahl die Korrektheit, mit einem Fall für die Axiome, einem weiteren für die Prämissen, dem semantischen Modus ponens und, für die Regel der Ersetzung der doppelten Negation, der Äquivalenz $\theta \eqsem \neg\neg\theta$ mit dem semantischen Ersetzungssatz. Die Eigenschaft, die von Zeile zu Zeile weitergegeben wird, ist nicht die Allgemeingültigkeit, sondern das Erfülltsein durch eine feste Belegung, die die Prämissen erfüllt, und deshalb gilt die Korrektheit mit Prämissen, auch mit unendlich vielen. Aus ihr folgten die Widerspruchsfreiheit jeder erfüllbaren Menge, insbesondere die des Kalküls, und die Methode, die der Einheit über die Deduktion fehlte: Ein Gegenmodell beweist, dass eine Deduktion nicht existiert.

Kalmár und die endliche Vollständigkeit

Dieselbe Lektion bewies die Umkehrung in zwei Schritten. Der erste ist das Lemma von Kalmár: Liegen die Variablen von $\varphi$ unter $u_{1}, \ldots, u_{n}$ , so gilt $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ für jede Belegung $v$ , wobei $\psi^{v}$ gleich $\psi$ ist, wenn $v(\psi) = 1$ , und sonst $\neg\psi$ ; der Kalkül deduziert aus jeder Zeile, was die Zeile über die Formel sagt. Seine Induktion über die Komplexität hat einen einzigen zusammengesetzten Fall, $(\alpha \downarrow \beta)$ , weil der Peirce-Pfeil der einzige Grundjunktor ist, und darin drei Unterfälle, die zwei Lemmata des Kalküls verlangen, das zweite in zwei Formen: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , deduziert mit der Einführung der Konjunktion, der doppelten Negation und zwei Anwendungen der Regel EDN, und $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ und $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , deduziert mit der Einführung der Disjunktion. Der zweite Schritt beseitigt die Prämissen: Ist $\varphi$ eine Tautologie, so wird sie aus den Prämissen jeder der $2^{n}$ Zeilen deduziert, und die Fallunterscheidung beseitigt das Literal der letzten Variablen, dann das der vorletzten, bis man zu $\vdash \varphi$ gelangt, der schwachen Vollständigkeit. Mit dem semantischen Deduktionstheorem und der Umkehrung des syntaktischen wurde die Vollständigkeit auf endliche Prämissenmengen ausgedehnt; daraus folgt, dass bei endlichen Prämissen Deduktion und Folgerung übereinstimmen, die beweisbare Äquivalenz mit der semantischen übereinstimmt und die Ableitbarkeit entscheidbar ist, weil die Tafel für sie einsteht.

Kompaktheit und starke Vollständigkeit

Die Lektion über den Kompaktheitssatz nahm sich des unendlichen Falls an, den das Lemma von Kalmár nicht erreicht, weil sich unendlich viele Prämissen nicht in eine Implikation abladen lassen. Sie bewies, ohne irgendeine Deduktion zu erwähnen, dass eine Menge genau dann erfüllbar ist, wenn jede ihrer endlichen Teilmengen es ist. Eine Folge von Werten für $v_{1}, \ldots, v_{n}$ ist gut, wenn jede endliche Teilmenge der Menge von einer Belegung erfüllt wird, die sie fortsetzt; das Zwei-Zeugen-Lemma sichert, dass sich eine gute Folge zu einer guten fortsetzen lässt, denn wäre keine der beiden Fortsetzungen gut, so widerspräche die Vereinigung der beiden endlichen Zeugen der Annahme, dass die Folge gut ist; und die Belegung, die sich ergibt, wenn man stets den Wert $1$ vorzieht, sofern es möglich ist, erfüllt jede Formel nach dem Koinzidenzlemma, weil jede Formel endlich viele Variablen hat. Die Konstruktion braucht das Auswahlaxiom nicht, weil die Variablen nummeriert sind und jeder Schritt eine Regel hat. Aus der Kompaktheit folgten ihre äquivalenten Formen, die Unerfüllbarkeitsform und die Folgerungsform; aus dieser, aus der Vollständigkeit für endliche Prämissenmengen und aus der Monotonie die starke Vollständigkeit; und aus dieser und der Korrektheit die volle Übereinstimmung: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ für jedes $\Gamma$ , und eine Menge ist genau dann widerspruchsfrei, wenn sie erfüllbar ist. Die Lektion wies darauf hin, dass diese Reihenfolge keine Frage der Vorliebe ist: Die Kompaktheit aus einer noch nicht verfügbaren starken Vollständigkeit zu gewinnen, wäre zirkulär. Sie endete mit der Färbung abzählbarer Graphen, die ein unendliches Problem in eine Formelmenge übersetzt, deren endliche Teile erfüllbar sind, und mit den Grenzen dessen, was eine Formelmenge ausdrücken kann.

Resolution

Die Lektion über die Resolutionsmethode ersetzte Formelmengen durch Klauselmengen, jede Klausel eine endliche Menge von Literalen, mit zwei Darstellungen: der Klauselform, die dieselben Modelle hat, und der definitorischen Form, die für jede zusammengesetzte Teilschreibweise eine neue Variable einführt, nur die Erfüllbarkeit bewahrt und wie die Formel wächst, nicht wie eine Zweierpotenz. Eine einzige Regel wirkt auf die Klauseln: Aus $C$ und $D$ mit $\ell \in C$ und $\ell^{*} \in D$ schließt man auf $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , und eine Widerlegung ist eine Herleitung, die bei $\Box$ ankommt. Die Korrektheit wurde wie die des Kalküls bewiesen, durch Induktion über die Herleitung und mit der Resolvente als Folgerung ihrer Prämissen; die Widerlegungsvollständigkeit durch Induktion über die Anzahl der Variablen, mit der Elimination einer Variablen, die die Erfüllbarkeit bewahrt und deren Beweis ein Modell konstruiert; und für unendliche Mengen wiederum mit der Kompaktheit. Daraus folgte, dass $\Gamma \models \varphi$ genau dann, wenn eine Klauselform von $\Gamma \cup \{\neg\varphi\}$ eine Widerlegung hat, und dass die Saturierung, die endlich ist, weil es bei $n$ Variablen nicht mehr als $4^{n}$ Klauseln gibt, die Erfüllbarkeit ohne Tafeln entscheidet. Die Lektion stellte das Erfüllbarkeitsproblem vor, dessen Kosten im ungünstigsten Fall niemand kennt, und zwei Fälle, die sich schnell entscheiden lassen, die Horn-Klauseln und die Klauseln mit zwei Literalen.

Die folgende Abbildung fasst die vier Abschnitte zu einer einzigen Kette zusammen. Jeder Knoten der Spalte ist ein Ergebnis, nach der logischen Ordnung nummeriert und durch einen Bogen mit den früheren Gliedern verbunden, die sein Beweis verwendet; um sie herum schweben die Stützen, das heißt die Prinzipien und Werkzeuge, auf die die Kette immer wieder zurückgreift, jede durch eine durchgezogene Linie mit den Gliedern verbunden, die sich auf sie stützen, und durch eine gepunktete mit dem Glied, in dem sie aufgestellt wird, außer denen, die aus den vorangehenden Einheiten stammen und als Ringe gezeichnet sind. Ein Klick auf eine Stütze hebt alle Glieder hervor, die sie verwenden, und jedes Glied verweist auf die Lektion, in der es bewiesen wird. Man beachte, dass die Korrektheit und die Kompaktheit, die eine im ersten und die andere im dritten Abschnitt aufgestellt, in den folgenden Abschnitten wieder auftauchen und dass die am häufigsten besuchte Stütze der Einheit die der Belegungen und Koinzidenz ist, gefolgt von der Induktion in ihren drei Formen: über die Zeilen einer Deduktion, über die Komplexität einer Formel und über die Anzahl der Variablen einer Klauselmenge.

Stützen der Kette

AInduktion und Rekursion. Starke Induktion über die natürlichen Zahlen, Induktion über die Komplexität der Formeln, mit dem einzigen zusammengesetzten Fall $(\alpha \downarrow \beta)$ , und rekursive Definition. Sie wurden in der ersten Einheit bewiesen. In dieser Einheit ohne Beweis angenommen.
BKalkül des Kurses. A1, A2 und A3, der Modus ponens und die Regel EDN; Reflexivität, Monotonie, Modus ponens zwischen Deduktionen, Endlichkeit und $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . Sie wurden in der zweiten Einheit aufgestellt. In dieser Einheit ohne Beweis angenommen.
CAbgeleitete Techniken. Doppelte Negation, aus der Lektion über die vier Techniken; Einführung der Konjunktion und der Disjunktion und Fallunterscheidung (wenn $\Gamma \cup \{\psi\} \vdash \chi$ und $\Gamma \cup \{\neg\psi\} \vdash \chi$ , dann $\Gamma \vdash \chi$ ), aus der Lektion über die Techniken der klassischen Logik. Sie wurden in der zweiten Einheit bewiesen. In dieser Einheit ohne Beweis angenommen.
DBelegungen und Koinzidenz. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; stimmen zwei Belegungen auf $V(\varphi)$ überein, so geben sie $\varphi$ denselben Wert; die Allgemeingültigkeit wird mit $2^{n}$ Zeilen entschieden. Sie wurden in der dritten Einheit bewiesen. In dieser Einheit ohne Beweis angenommen.
ESemantische Folgerung. Falsche Zeile der Implikation, Monotonie, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ genau dann, wenn $\Gamma \cup \{\neg\varphi\}$ unerfüllbar ist, und der semantische Ersetzungssatz. Sie wurden in der dritten Einheit bewiesen. In dieser Einheit ohne Beweis angenommen.
FKonjunktive Formen. Wertlemma; jede Formel ist zu einer konjunktiven Normalform äquivalent, die $2^{n}$ Klauseln brauchen kann; eine Disjunktion von Literalen ist genau dann allgemeingültig, wenn sie ein komplementäres Paar enthält. Sie wurden in der dritten Einheit bewiesen. In dieser Einheit ohne Beweis angenommen.
GKorrektheit. Wenn $\Gamma \vdash \varphi$ , dann $\Gamma \models \varphi$ , für jede Menge $\Gamma$ ; ein Gegenmodell beweist, dass eine Deduktion nicht existiert. Begründet in: 2. Korrektheit.
HKompaktheit. Eine Formelmenge ist genau dann erfüllbar, wenn jede ihrer endlichen Teilmengen erfüllbar ist; daher ist, was unerfüllbar ist, es schon in einem endlichen Teil. Begründet in: 11. Kompaktheitssatz.

Abschnitt 1 Korrektheit
- Prüfen, dass jede Instanz der Schemata allgemeingültig ist, ohne ihre Tafel aufzustellen.
- Die Korrektheit durch starke Induktion über die Zeilenzahl beweisen, mit dem Fall der Regel der Ersetzung der doppelten Negation.
- Mit einem Gegenmodell beweisen, dass eine Formel nicht deduziert wird, und die Widerspruchsfreiheit aus der Korrektheit gewinnen.
1. Allgemeingültigkeit der Axiome. Jede Instanz von A1, A2 und A3 ist allgemeingültig: Eine Belegung, die sie widerlegte, verlangte über die falsche Zeile der Implikation unmögliche Werte.
  Stützt sich auf: E (Semantische Folgerung). Bewiesen in: Korrektheit und Vollständigkeit.
2. Korrektheit. Wenn $\Gamma \vdash \varphi$ , dann $\Gamma \models \varphi$ , für jedes $\Gamma$ : durch starke Induktion über die Zeilenzahl, mit einem Fall für die Axiome, einem weiteren für die Prämissen, dem semantischen Modus ponens und, für die Regel EDN, $\theta \eqsem \neg\neg\theta$ mit der semantischen Ersetzung.
  Verwendet: 1. Allgemeingültigkeit der Axiome. Stützt sich auf: A (Induktion und Rekursion), B (Kalkül des Kurses), E (Semantische Folgerung). Bewiesen in: Korrektheit und Vollständigkeit.
3. Widerspruchsfreiheit und Gegenmodelle. Jede erfüllbare Menge ist widerspruchsfrei; der Kalkül ist widerspruchsfrei und $\nvdash v_{1}$ ; erfüllt eine Belegung $\Gamma$ und widerlegt $\varphi$ , so gilt $\Gamma \nvdash \varphi$ , und die Tafel bescheinigt, dass, was nicht allgemeingültig ist, kein Theorem ist.
  Stützt sich auf: G (Korrektheit), D (Belegungen und Koinzidenz). Bewiesen in: Korrektheit und Vollständigkeit.
Abschnitt 2 Kalmár und die endliche Vollständigkeit
- Im Kalkül die zwei Lemmata über den Peirce-Pfeil deduzieren, mit der Regel der Ersetzung der doppelten Negation, wo es nötig ist.
- Das Lemma von Kalmár durch Induktion über die Komplexität beweisen, mit einem einzigen zusammengesetzten Fall.
- Mit der Fallunterscheidung die Prämissen der Zeilen beseitigen und endliche Prämissen mit den beiden Deduktionstheoremen abladen.
- Mit der Tafel die Ableitbarkeit, die beweisbare Äquivalenz und die Widerspruchsfreiheit aus endlichen Prämissen entscheiden.
1. Einführung des Peirce-Pfeils. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ und $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : Die Konjunktion der Negationen ist $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; die doppelte Negation entfernt die äußere, und die Regel EDN die beiden inneren.
  Stützt sich auf: B (Kalkül des Kurses), C (Abgeleitete Techniken). Bewiesen in: Korrektheit und Vollständigkeit.
2. Negation des Peirce-Pfeils. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ und $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , weil $\neg(\alpha \downarrow \beta)$ gleich $(\alpha \vee \beta)$ ist und die Einführung der Disjunktion genügt.
  Stützt sich auf: B (Kalkül des Kurses), C (Abgeleitete Techniken). Bewiesen in: Korrektheit und Vollständigkeit.
3. Lemma von Kalmár. Wenn $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , dann $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ für jede Belegung $v$ ; der Induktionsschritt hat einen einzigen Fall, $(\alpha \downarrow \beta)$ , mit drei Unterfällen je nach den Werten von $\alpha$ und von $\beta$ .
  Verwendet: 4. Einführung des Peirce-Pfeils, 5. Negation des Peirce-Pfeils. Stützt sich auf: A (Induktion und Rekursion), D (Belegungen und Koinzidenz), B (Kalkül des Kurses). Bewiesen in: Korrektheit und Vollständigkeit.
4. Schwache Vollständigkeit. Wenn $\models \varphi$ , dann $\vdash \varphi$ : Das Lemma von Kalmár deduziert $\varphi$ aus jeder Zeile, und die Fallunterscheidung beseitigt die Literale von der letzten Variablen bis zur ersten, mit $2^{n}$ Anwendungen des Lemmas und $2^{n} - 1$ der Fallunterscheidung.
  Verwendet: 6. Lemma von Kalmár. Stützt sich auf: C (Abgeleitete Techniken). Bewiesen in: Korrektheit und Vollständigkeit.
5. Vollständigkeit für endliche Prämissenmengen. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : Das semantische Deduktionstheorem führt zu einer Tautologie, die schwache Vollständigkeit deduziert sie, und die Umkehrung des Deduktionstheorems gibt die Prämissen zurück.
  Verwendet: 7. Schwache Vollständigkeit. Stützt sich auf: E (Semantische Folgerung), B (Kalkül des Kurses). Bewiesen in: Korrektheit und Vollständigkeit.
6. Endliche Übereinstimmung und Entscheidung. Für endliches $\Gamma$ gilt $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ und $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; daher ist die Ableitbarkeit aus endlichen Prämissen entscheidbar, mit der Tafel.
  Verwendet: 8. Vollständigkeit für endliche Prämissenmengen. Stützt sich auf: G (Korrektheit), D (Belegungen und Koinzidenz). Bewiesen in: Korrektheit und Vollständigkeit.
Abschnitt 3 Kompaktheit und starke Vollständigkeit
- Die Kompaktheit beweisen, indem man die Werte der Variablen einen nach dem anderen festlegt, mit der Invariante der guten Folgen und dem Zwei-Zeugen-Argument.
- Zwischen der Erfüllbarkeitsform, der Unerfüllbarkeitsform und der Folgerungsform wechseln.
- Die starke Vollständigkeit aus der Kompaktheit gewinnen, ohne Zirkularität, und aus ihr die Übereinstimmung von Widerspruchsfreiheit und Erfüllbarkeit.
- Probleme über unendliche Objekte in Formelmengen kodieren und sie mit der Kompaktheit lösen.
1. Zwei-Zeugen-Lemma. Ist die Folge $s$ festgelegter Werte gut (jede endliche Teilmenge der Menge wird von einer Belegung erfüllt, die sie fortsetzt), so ist es auch $(s, 1)$ oder $(s, 0)$ : Wäre es keine, so widerspräche die Vereinigung der beiden endlichen Zeugen der Annahme, dass $s$ gut ist.
  Stützt sich auf: D (Belegungen und Koinzidenz). Bewiesen in: Der Kompaktheitssatz.
2. Kompaktheitssatz. $\Gamma$ ist genau dann erfüllbar, wenn jede endliche Teilmenge es ist: Man setzt $v_{n + 1}$ auf $1$ , wenn $(s_{n}, 1)$ gut ist, und sonst auf $0$ , und die entstehende Belegung erfüllt jede Formel nach dem Koinzidenzlemma. Das Auswahlaxiom wird nicht gebraucht, weil die Variablen nummeriert sind.
  Verwendet: 10. Zwei-Zeugen-Lemma. Stützt sich auf: A (Induktion und Rekursion), D (Belegungen und Koinzidenz). Bewiesen in: Der Kompaktheitssatz.
3. Äquivalente Formen. $\Gamma$ ist genau dann unerfüllbar, wenn ein endlicher Teil es ist; $\Gamma \models \varphi$ genau dann, wenn $\Gamma_{0} \models \varphi$ für ein endliches $\Gamma_{0} \subseteq \Gamma$ ; und diese letzte Form impliziert ihrerseits den Satz.
  Verwendet: 11. Kompaktheitssatz. Stützt sich auf: E (Semantische Folgerung). Bewiesen in: Der Kompaktheitssatz.
4. Starke Vollständigkeit. Wenn $\Gamma \models \varphi$ , dann $\Gamma \vdash \varphi$ , für jedes $\Gamma$ : Die Folgerungsform liefert ein endliches $\Gamma_{0}$ , die Vollständigkeit für endliche Prämissenmengen liefert $\Gamma_{0} \vdash \varphi$ , und die Monotonie $\Gamma \vdash \varphi$ .
  Verwendet: 8. Vollständigkeit für endliche Prämissenmengen, 12. Äquivalente Formen. Stützt sich auf: B (Kalkül des Kurses). Bewiesen in: Der Kompaktheitssatz.
5. Deduktion ist Folgerung. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ für jedes $\Gamma$ ; die Theoreme sind genau die Tautologien, und eine Menge ist genau dann widerspruchsfrei, wenn sie erfüllbar ist.
  Verwendet: 13. Starke Vollständigkeit. Stützt sich auf: G (Korrektheit). Bewiesen in: Der Kompaktheitssatz.
6. Färbung abzählbarer Graphen. Mit einer Variablen $x_{i,c}$ für jede Ecke und Farbe und mit Formeln, die sagen, dass jede Ecke genau eine Farbe hat und benachbarte Ecken sich unterscheiden, besitzt ein abzählbarer Graph eine Färbung mit $k$ Farben, wenn jeder endliche Teilgraph eine besitzt.
  Stützt sich auf: H (Kompaktheit), F (Konjunktive Formen). Bewiesen in: Der Kompaktheitssatz.
Abschnitt 4 Resolution
- Eine Formelmenge als Klauselmenge darstellen, über die konjunktive oder über die definitorische Form.
- Widerlegungen aufbauen, ohne zwei komplementäre Paare in einem Schritt zu beseitigen.
- Die Korrektheit und die Widerlegungsvollständigkeit der Resolution beweisen, für endliche Mengen und, mit der Kompaktheit, für beliebige.
- Folgerungen durch Saturierung entscheiden und die Fälle erkennen, die sich schnell entscheiden lassen.
1. Klauselform. Eine Klausel ist eine endliche Menge von Literalen, erfüllt, wenn ein Literal den Wert $1$ annimmt, und $\Box$ ist unerfüllbar; eine Klauselform von $\Gamma$ hat dieselben Modelle, und $\Gamma \models \varphi$ genau dann, wenn eine Klauselform von $\Gamma \cup \{\neg\varphi\}$ unerfüllbar ist.
  Stützt sich auf: F (Konjunktive Formen), E (Semantische Folgerung). Bewiesen in: Die Resolutionsmethode.
2. Definitorische Klauselform. Mit einer neuen Variablen je Teilschreibweise und ihren Definitionsklauseln ist $T(\varphi)$ erfüllbarkeitsäquivalent zu $\varphi$ und hat höchstens $4k + 1$ Klauseln mit höchstens drei Literalen; die definitorischen Formen entscheiden die Folgerung aus endlichen Prämissen.
  Verwendet: 16. Klauselform. Stützt sich auf: A (Induktion und Rekursion), D (Belegungen und Koinzidenz). Bewiesen in: Die Resolutionsmethode.
3. Korrektheit der Resolution. $\{C, D\} \models R_{\ell}(C, D)$ , durch Fallunterscheidung nach dem Wert von $\ell$ ; durch starke Induktion über die Herleitung gilt $S \models C$ für jede Klausel $C$ , die aus $S$ hergeleitet ist, und hat $S$ eine Widerlegung, so ist es unerfüllbar.
  Verwendet: 16. Klauselform. Stützt sich auf: A (Induktion und Rekursion). Bewiesen in: Die Resolutionsmethode.
4. Elimination einer Variablen. $E_{p}(S)$ , das die Klauseln ohne $p$ und ohne $\neg p$ behält und die Resolventen nach $p$ hinzufügt, enthält $p$ nicht und ist erfüllbarkeitsäquivalent zu $S$ ; aus einem Modell davon gewinnt man eines von $S$ , indem man den Wert von $p$ wählt.
  Verwendet: 18. Korrektheit der Resolution. Stützt sich auf: D (Belegungen und Koinzidenz). Bewiesen in: Die Resolutionsmethode.
5. Endliche Widerlegungsvollständigkeit. Jede endliche unerfüllbare Klauselmenge hat eine Widerlegung, durch Induktion über die Anzahl der Variablen: Man eliminiert die letzte und fügt die Prämissen jeder Resolvente ein.
  Verwendet: 19. Elimination einer Variablen. Stützt sich auf: A (Induktion und Rekursion). Bewiesen in: Die Resolutionsmethode.
6. Widerlegungsvollständigkeit. Eine Klauselmenge, endlich oder unendlich, ist genau dann unerfüllbar, wenn sie eine Widerlegung hat; daher $\Gamma \models \varphi$ genau dann, wenn eine Klauselform von $\Gamma \cup \{\neg\varphi\}$ eine Widerlegung hat.
  Verwendet: 16. Klauselform, 18. Korrektheit der Resolution, 20. Endliche Widerlegungsvollständigkeit. Stützt sich auf: H (Kompaktheit). Bewiesen in: Die Resolutionsmethode.
7. Die Saturierung entscheidet. Bei $n$ Variablen hat die Menge der hergeleiteten Klauseln höchstens $4^{n}$ Elemente; die Saturierung bricht ab und entscheidet die Erfüllbarkeit ohne Tafeln, wenn auch nicht immer schneller als diese.
  Verwendet: 18. Korrektheit der Resolution, 20. Endliche Widerlegungsvollständigkeit. Bewiesen in: Die Resolutionsmethode.

Das Ende des Kurses. Die Kette endet dort, wo sich die beiden Seiten des Kurses als eine einzige Relation erkennen und man über eine Methode verfügt, sie zu entscheiden. Was offen bleibt, ist keine Frage über die Aussagenlogik mehr, sondern über ihre Kosten und über ihre Erweiterung um Quantoren.