Finitisieren und mechanisieren

Zusammenfassung

Jetzt übertragen wir einige wichtige Ergebnisse des 2. Teils — Semi-Entscheidungsverfahren und Endlichkeitssätze, nicht dagegen Vollständigkeit — auf die Quantorenlogik und gewinnen so wichtige, aber auch überraschende Ergbenisse. Als erstes stellen wir die Theorembeweiser, von denen Clarissa in der Einleitung zu Teil 2 gesprochen hat, für die Prädikatenlogik auf. Dazu setzen wir alles zusammen, was wir bisher gelernt haben: Mit Hilfe der Ergebnisse aus 3A überführen wir Formeln in pränexe Normalform (3B1) und beseitigen dann die Quantoren durch Skolemisieren (3B2). Die entstehenden quantorenfreien Formeln können wir in die Theorembeweiser aus 2D5 oder 2D6 eingeben (3B3). Als Anwendung benutzen wir Theorembeweiser, um Beispielterme für Existenzformeln zu finden (3B4). Damit formulieren wir das alte Ergebnis von Herbrand um, das wir in Abschnitt 2D6 in einer Fassung fürs Theorembeweisen gebracht haben, und verallgemeinern es fürs logische Programmieren. In 3B5 spezialisieren wir das Verfahren für Hornformeln und erläutern so die Vorgehensweise, die PROLOG zugrundeliegt. In 3B6 zeigen wir, daß auch in der Prädikatenlogik jede erfüllbare Formelmenge ein Herbrandmodell hat und folgern daraus in 3B7, daß es zu jeder Struktur eine äquivalente (die selben Formeln erfüllende) höchstens abzählbare gibt (Satz von Löwenheim und Skolem). In 3B8 schließlich gewinnen wir aus dem Vollständigkeits-den Kompaktheits- und den Endlichkeitssatz wieder. Als erste Konsequenz daraus bedrohen uns Monster in Architektenstrukturen, die uns in Kap. 3C in den natürlichen Zahlen heilsame Lehren erteilen werden.