Gibt es ein Beweissystem für die Prädikatenlogik? Nun, angesichts des Titels dieses Kapitels liegt es nahe, dass es ein solches gibt, aber klar ist dies keineswegs. Die Prädikatenlogik ist einfach komplizierter als die Aussagenlogik und dies spiegelt sich auch in der Antwort auf die Frage wider, ob es ein Beweissystem gibt.
Bei der Aussagenlogik war von Anfang an klar, dass es ein Beweissystem gibt, nämlich die Wahrheitstafeln, vortrefflich streiten ließ sich lediglich um die Frage, ob denn nun die Resolution oder doch eher Hilbertbeweise mit Freges Axiomsystem geeigneter seien. Bei der Prädikatenlogik versagt die Wahrheitstafelmethode kläglich: die Entsprechung dieser Methode in der Prädikatenlogik ist, für eine Formel alle möglichen Welten durchzugehen und zu testen, ob die Formel für alle diese Welten wahr wird. Leider gibt es selbst für völlig banale Formeln wie x=x unendliche viele mögliche Welten, die getestet werden wollen. Zum Vergleich: bei der Aussagenlogik ist die Anzahl der Welten, die bei einer Formel mit n Variablen getestet werden müssen, »nur« 2^n.
Ob eine prädikatenlogische Formel eine Tautologie ist oder nicht, ist ein semantische Fragestellung, die wir aber nicht allein durch die Untersuchung von semantischen Begriffen wie Welten und Modellen beantworten können. Es gibt einfach zu viele Welten.
Der Trick besteht darin, die Fronten zu wechseln und zum syntaktischen Lager überzulaufen. Das Beweissystem von Hilbert ist das Flagschiff der syntaktischen Fraktion: Sie erinnern sich vielleicht noch daran, dass in diesem System formalistisch einfach nur Formeln zeilenweise untereinander geschrieben wurden und nur eine einzige Regel, der Modus ponens, beachtet werden muss. Während eines solchen Hilbertbeweises ging sehr schnell jegliche Anschauung verloren, was die Formeln bedeuten; man war einfach nur glücklich und ermattet, wenn endlich am Ende die gewünschte Formel stand.
In diesem Kapitel werden Sie sehen, dass wir den Hilbertkalkül für Aussagenlogik zu einem für die Prädikatenlogik ausbauen können, einfach indem wir einige neue Axiome hinzufügen. Wie immer sind die Axiome Trivialitäten wie $x\equ x$. Es war eine der wirklich großen Sternstunden der Mathematik, als Kurt Gödel 1929 bewiesen hat, dass man nur mittels des Modus ponens aus einem solchen Satz von Axiomen alle prädikatenlogischen Tautologien herleiten kann.