Wir wollen uns in diesem Unterkapitel genauer ansehen, was es bedeutet, wenn ein formales System widerspruchsfrei und vollständig ist. Dazu fassen wir noch einmal zusammen, was wir unter einem formalen axiomatisierten System verstehen:
Ein sehr einfaches formales System wäre beispielsweise das Schachspiel. Die Syntaxregeln und Umwandlungsregeln spiegeln dabei die Spielregeln wieder. Wohlgeformte Ausdrücke entsprechen Figurenaufstellungen auf dem Schachbrett. Als einziges Axiom dient die Startaufstellung. In diesem formalen System ist von logischen Aussagen allerdings noch keine Rede.
Wenn wir Hilberts Vision untersuchen wollen, müssen wir komplexere formale Systeme als das Schachspiel betrachten. So ist es notwendig, dass die Regeln der Logik in dem System enthalten sind. Erst dann ist es überhaupt möglich, zu einer Aussage \( A \) die verneinte Aussage \( \neg A \) zu formulieren.
Da man in der Mathematik sehr viele Dinge auf die natürlichen Zahlen zurückführen kann, interessieren wir uns besonders für ein entsprechendes formales System, das die Arithmetik der natürlichen Zahlen inklusive Addition und Multiplikation umfasst. Von diesem System ausgehend kann man sich dann zu Brüchen, reellen Zahlen und anderen komplexeren Systemen vorarbeiten. Ein Zitat von Leopold Kronecker aus dem Jahr 1886 spiegelt dies wieder:
"Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk."
(die ganzen Zahlen umfassen dabei die natürlichen Zahlen, die Null, und die natürlichen Zahlen mit einem negativen Vorzeichen versehen).
Betrachten wir nun allgemein die wohlgeformten Aussagen in einem formalen System. Diese Aussagen sind nichts anderes als Zeichenketten (Strings) mit Zeichen aus irgendeinem endlichen Alphabet, die bestimmten Syntaxregeln genügen. Ist es möglich, eine (unendlich lange) Liste zu erstellen, in der jede dieser wohlgeformten Zeichenketten garantiert in irgendeiner Zeile vorkommt?
Um diese Frage zu klären, erstellen wir in einem ersten Schritt eine Liste aller möglichen Zeichenketten, indem wir zunächst alle Zeichenketten der Länge 1 in irgendeiner Reihenfolge (z.B "alphabetisch") aufschreiben, anschließend alle Zeichenketten der Länge 2 hinzufügen usw.. Wenn unser Alphabet beispielsweise nur die beiden Zeichen A und B umfassen würde, sähe diese Liste so aus:
Wir sehen, dass die Liste sehr schnell wächst, nämlich exponentiell mit der Länge der Zeichenketten. Die Liste enthält tatsächlich alle Texte, die aus endlich vielen Zeichen des zugelassenen Alphabets bestehen. Nehmen wir die Zeichen einer Computertastatur, so steht an irgendeiner Stelle in der Liste das komplette Telefonbuch Leverkusens, an irgendeiner anderen Stelle befindet sich der erste Harry-Potter-Roman, und auch die Aussage \( 1 + 1 = 2 \) findet sich in der Liste. Bleibt also die Frage, ob wir die uns interessierenden Zeilen aus der Liste irgendwie – zumindest im Prinzip – herausfiltern können.
Wir hatten oben vorausgesetzt, dass es ein mechanisches Verfahren gibt, mit dem man in endlich vielen Schritten entscheiden kann, ob eine gegebene Zeichenkette wohlgeformt ist. Daher können wir in unserer Zeichenkettenliste die nicht-wohlgeformten Zeichenketten identifizieren und weglöschen. Übrig bleibt die gesuchte Liste aller wohlgeformten Zeichenketten bzw. Aussagen des formalen Systems. Unser Ergebnis lautet also
Man sagt auch, sie sind abzählbar. Sie lassen sich auflisten, wobei die Liste unendlich lang sein darf.
Das obige Verfahren ist natürlich für praktische Zwecke absolut unbrauchbar, denn die meisten zunächst erzeugten Zeichenketten sind nicht wohlgeformt und müssen gelöscht werden. Doch zunächst einmal geht es uns nur ums Prinzip: ein Verfahren braucht hier noch nicht effektiv zu sein; Hauptsache, es ist prinzipiell durchführbar. Umso gewichtiger wird dann später die Aussage sein, wenn es für eine Fragestellung nicht einmal im Prinzip ein solches Verfahren gibt!
Wir können noch einen Schritt weitergehen und versuchen, eine Liste aller möglichen Ableitungen wohlgeformter Zeichenketten (ausgehend von den Axiomen) zu erstellen. Eine solche Ableitung können wir als Aneinanderreihung von wohlgeformten Zeichenketten aufschreiben, wobei wir die Zeichenketten beispielsweise durch ein Komma trennen. Links fangen wir mit einem oder mehreren Axiomen an, dann wenden wir eine der Umwandlungsregeln an, um den nächsten String hinter dem Komma zu erzeugen usw.. Die Hintereinanderreihung der Zeichenketten ergibt somit gleichsam den formalen Beweis der am weitesten rechts stehenden Zeichenkette.
Nehmen wir als einfaches Beispiel für ein formales System wieder das Schachspiel. Die Ableitung einer Figurenaufstellung aus dem Axiom (also aus der Startaufstellung) ist die Abfolge der einzelnen Stellungen, die sich nach jedem Zug von Weiß bzw. Schwarz aus der Startaufstellung ergeben und die zur betrachteten Figurenaufstellung führen. Mit anderen Worten: die Ableitung entspricht der Notation der Schachpartie.
Ist es nun möglich, diese Ableitungen (also Beweisketten) in einer Liste komplett zu erfassen und durchzunummerieren?
Da auch mehrere aneinandergereihte, durch Komma getrennte Zeichenketten zusammen wieder eine Zeichenkette bilden, sollte es möglich sein, eine solche Liste aufzuschreiben. Wir können das Komma ja einfach als ein weiteres Zeichen unseres Alphabets auffassen. Beginnen wir also mit einer Liste aller Zeichenketten, die sich aus den Buchstaben des vorgegebenen Alphabets zuzüglich des Komma-Zeichens bilden lassen. Eine solche Liste lässt sich wie oben angegeben erzeugen, indem wir alle Zeichenketten der Größe nach alphabetisch auflisten.
Nun entfernen wir alle Zeichenketten, bei denen das Komma am Anfang oder am Ende steht, oder bei denen zwei Kommata aufeinander folgen. Weiterhin entfernen wir alle Zeichenketten, die kein Komma enthalten. Das Ergebnis ist eine Liste von Zeichenketten, bei denen Kommata einzelne Unter-Zeichenketten voneinander trennen. In unserem obigen Beispiel sähe diese Liste so aus:
Der nächste Schritt besteht darin, alle Zeichenketten zu entfernen, bei denen die Unter-Zeichenketten nicht wohlgeformt sind (das lässt sich ja immer eindeutig entscheiden). Die Liste enthält jetzt nur noch Zeichenketten, bei denen wohlgeformte Unter-Zeichenketten durch Kommata voneinander getrennt sind.
Nun folgt der entscheidende letzte Schritt: Wir gehen jede Zeichenkette von rechts nach links durch und überprüfen, ob die jeweils rechts vom Komma stehende Unter-Zeichenkette durch eine Umwandlungsregel aus den links stehenden Unter-Zeichenketten erzeugt werden kann. Dass eine solche Überprüfung möglich ist, hatten wir oben vorausgesetzt. Ganz links endet diese Überprüfungskette dann bei den Axiomen. Nur solche Zeichenketten werden in der Liste beibehalten, die diesen Überprüfungen stand halten. Das Ergebnis ist eine Liste aller Ableitungen (Beweise), die in dem formalen System möglich sind.
Fassen wir noch einmal zusammen:
Anders ausgedrückt: Es gibt eine vollständige Liste aller Beweise in einem formalen System. Dabei darf die Liste unendlich lang sein.
Zurück zu Hilberts Vision: Es gibt zwei Eigenschaften, die uns bei einem formalen System der natürlichen Zahlen besonders interessieren: die Widerspruchsfreiheit und die Vollständigkeit. Hier sind die Definitionen dieser beiden Begriffe:
Diese beiden Eigenschaften sollte nach Hilberts Vision ein formales System der natürlichen Zahlen aufweisen, d.h. jede Aussage über natürliche Zahlen sollte sich entweder beweisen oder widerlegen lassen, und Widersprüche sollten nicht vorhanden sein.
Nehmen wir einmal an, wir hätten tatsächlich ein formales System gefunden, das widerspruchsfrei und vollständig ist. Betrachten wir eine Zeichenkette \( A \) und ihre Negation \( \neg A \). Da das System vollständig ist, muss es entweder für \( A \) oder für \( \neg A \) eine Ableitung geben. Oben hatten wir gesehen, dass wir eine Liste aller Ableitungen wohlgeformter Zeichenketten erstellen können. Also muss irgendwo in dieser Liste entweder die Ableitung für \( A \) oder die Ableitung für \( \neg A \) zu finden sein. Wir brauchen die Liste nur noch abzusuchen, und diese Suche muss nach endlich vielen Schritten enden (wobei wir allerdings nicht wissen, nach wievielen Schritten, denn die Liste ist unendlich lang). Damit können wir rein mechanisch entscheiden, ob \( A \) oder \( \neg A \) aus den Axiomen ableitbar ist, und die Ableitung erhalten wir gleich noch dazu. Wir haben damit ein sogenanntes Entscheidungsverfahren gefunden. Hier noch einmal die genaue Definition:
Anders ausgedrückt: ein Entscheidungsverfahren sagt uns, ob eine Aussage beweisbar ist oder nicht, und liefert ggf. sogar den Beweis gleich mit. Wie wir gerade gezeigt haben, gilt:
Die Voraussetzung, dass das System widerspruchsfrei und vollständig ist, ist bei der obigen Überlegung ganz entscheidend. Ist das System unvollständig, so wissen wir nicht, ob es überhaupt eine Ableitung eines der Ausdrücke \( A \) oder \( \neg A \) gibt. Wir können die Liste daher ewig durchsuchen, ohne auf eine solche Ableitung zu stoßen. Allein aus der Tatsache, dass wir eine Liste aller Ableitungen aufstellen können, folgt also noch nicht, dass es ein Entscheidungsverfahren gibt.
Fassen wir noch einmal zusammen: Wenn sicher ist, dass entweder \( A \) oder \( \neg A \) ableitbar sind, so kann man auch (zumindest im Prinzip) entscheiden, welche dieser beiden Alternativen zutrifft. Wie effektiv ein solches Entscheidungsverfahren dabei ist, soll uns hier noch nicht interessieren – das obige Verfahren ist sehr, sehr langsam. Es ist für die Praxis total unbrauchbar und wäre in der Mathematik daher nicht geeignet, einen Beweis zu finden. Aber es würde sicherstellen, dass es einen Beweis für \( A \) oder für \( \neg A \) geben muss. Es wäre nur noch eine sportliche Herausforderung, ihn zu finden. Genau das war Hilberts Vision.
Literatur:
© Jörg Resag, www.joerg-resag.de
last modified on 19 February 2023