© 1999
François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung
angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine
Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials
bedarf der Erlaubnis des Autors.
Für die Prädikatenlogik erster Stufe haben wir bisher noch keine Beweismethode kennengelernt, die zumindest im Prinzip funktioniert, so wie die Methode der Wahrheitstabellen für die Aussagenlogik. Die dazu erforderlichen Bausteine wurden allerdings bereits behandelt und brauchen jetzt nur noch zusammengesetzt zu werden.
Eine endliche Formelmenge ist genau dann unerfüllbar, wenn die Konjunktion aller Formeln dieser Menge unerfüllbar ist. Es reicht also aus, den Fall einer einzelnen Formel F zu betrachten.
Nach dem Normalformensatz für die PL1S (Satz 4.4.14) gibt es Algorithmen zur effektiven Berechnung einer Formel F' in Klauselnormalform, so dass F genau dann unerfüllbar ist, wenn ∀(F') kein Herbrand-Modell hat. Nach Satz 3.8.16 gilt dies genau dann, wenn die Menge S* der Grundinstanzen von ∀(F') kein Herbrand-Modell hat.
Wenn die betrachtete Sprache der Prädikatenlogik erster Stufe nur endlich viele Konstanten und keine mindestens einstelligen Funktionssymbole enthält, gibt es nur endlich viele Grundterme, und S* ist endlich. Im allgemeinen ist S* aber abzählbar unendlich.
Wir können nun jede der höchstens abzählbar vielen atomaren Formeln in S* als Namen einer Aussagenvariablen ansehen. Da weder Quantoren noch Variablen in S* vorkommen, entspricht jede Herbrand-Interpretation bei dieser Sichtweise einer Wahrheitsbelegung für diese Aussagenvariablen. Damit ist F genau dann unerfüllbar, wenn die unendliche Menge S*, als Menge von aussagenlogischen Formeln betrachtet, unerfüllbar ist.
Diese Frage ist nach Satz 4.2.2 semi-entscheidbar, sofern S* aufzählbar ist. Dies folgt aber unmittelbar daraus, dass die Menge aller Grundterme zu einer gegebenen Signatur aufzählbar ist.
Das Prinzip ist also, die zu testende Formel in Klauselnormalform umzuwandeln und davon systematisch alle Grundinstanzen aufzuzählen. Nach jeder neuen Grundinstanz kann man zum Beispiel mit der Methode der Wahrheitstabellen testen, ob die bisher erzeugte Menge von Grundinstanzen unerfüllbar ist. Sobald das der Fall ist, ist auch die Unerfüllbarkeit der ursprünglichen Formel nachgewiesen.
Man beachte, dass der Satz bereits für eine einzige Formel nur die Semi-Entscheidbarkeit sicherstellt, nicht die Entscheidbarkeit. Die Unerfüllbarkeit im endlichen Fall ist zwar für die Aussagenlogik entscheidbar, aber nicht für die Prädikatenlogik erster Stufe.
Dies kann durch Reduktion auf eine als unentscheidbar bekannte Frage gezeigt werden. Wenn es einen Entscheidungs-Algorithmus für die Unerfüllbarkeit von Formeln der Prädikatenlogik erster Stufe gäbe, könnte man daraus beispielsweise einen Entscheidungs-Algorithmus für das Halteproblem von Turingmaschinen konstruieren.
Es gibt jedoch einige syntaktische Einschränkungen, unter denen die Unerfüllbarkeit einer Formel doch entscheidbar ist: zum Beispiel, wenn alle Funktions- und Relationssymbole höchstens einstellig sind, oder auch, wenn die Formel universell ist und keine mindestens einstelligen Funktionssymbole enthält.
Mit derartigen syntaktischen Einschränkungen der Logik ist natürlich nicht mehr alles ausdrückbar, was mit der uneingeschränkten Prädikatenlogik erster Stufe ausdrückbar ist. Man verbessert also die algorithmische Behandelbarkeit auf Kosten der Ausdrucksstärke. Will man umgekehrt die Ausdrucksstärke verbessern, geht dies auf Kosten der algorithmischen Behandelbarkeit. Wenn die Logik nur so weit über die Prädikatenlogik erster Stufe hinausgeht, dass man die natürlichen Zahlen darin formalisieren kann, verliert man sogar die Semi-Entscheidbarkeit der Unerfüllbarkeit. Das folgt aus einem berühmten Ergebnis von Kurt Gödel, dem sogenannten Unvollständigkeitssatz.
Die Prädikatenlogik erster Stufe ist in mancherlei Hinsicht der beste Kompromiss zwischen Ausdrucksstärke und algorithmischer Behandelbarkeit.