Wozu Mathematische Logik?

WOLFGANG ZUBER

Mathematische Logiker stehen oft im Verdacht, besondere Pedanten zu sein. Wahr an dem Vorurteil ist, dass das A und O der Arbeit vieler Logiker in ihrem Hang zum Formalismus steckt. Geht man dem Phänomen jedoch etwas weiter nach, so wird man bald überrascht den tieferen Grund für diese Feinarbeit feststellen: Faulheit!

Während der typische Mathematiker versucht, ein Problem zu lösen, indem er eine Anschauung gewinnt, anhand derer er inhaltlich schließt (was bei der Komplexität der in der Praxis auftretenden Probleme scheußliche Kopfschmerzen bereiten kann), hofft der Logiker, wenn er das Problem erst einmal in eine Formel gefasst hat, sich getrost auf ein Dutzend Regeln (einen "Kalkül") verlassen zu können, die er nur stur anwenden muss, ohne weiter nachzudenken.

Gottlob Frege war vor hundertzwanzig Jahren der erste, der so einen Kalkül aufstellte, den er Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens nannte und den damals außer ihm fast keiner verstand. David Hilbert, der größte Mathematiker seiner Zeit, war so begeistert von der Idee, dass er zu Beginn unseres Jahrhunderts gleich die gesamte Mathematik in einem großen, widerspruchsfreien System formalisieren wollte. Alfred North Whitehead und Bertrand Russell haben 1910/12/13 in ihrem monumentalen Buch Principia Mathematica die ersten Schritte umgesetzt. (Der Beweis von 1+1=2 wird in Band 1, Seite 362 erstmals angekündigt, gelingt aber erst in Band 2.) Die theoretische Fundierung schien 1930 der junge Kurt Gödel in seiner Dissertation über die Vollständigkeit der Axiome des logischen Funktionenkalküls zu liefern:

(Vollständigkeitssatz.) Eine Formel folgt genau dann logisch aus gegebenen Axiomen, wenn sie rein nach den Regeln des Kalküls ableitbar ist.

(Man sagt deshalb, der Kalkül sei "vollständig".)

Der Formalismus hatte Nahrung bekommen von in der Mathematik der Jahrhundertwende auftretenden Paradoxien, die man einem zu sorglosen Umgang mit den neuen Objekten zuschrieb ("Grundlagenkrise"). Frege, der gerade ein Buch über die Mengenlehre von Georg Cantor geschrieben hatte, verzweifelte ob des ihm von Russell vorgelegten Paradoxons der
Menge aller Mengen, die sich selbst nicht als Element enthalten.

(Diese "Menge" enthält sich selbst als Element genau dann, wenn sie es nicht tut.)

Cantor selbst bereitete die Unlösbarkeit eines anderen mengentheoretischen Problems, des Größenvergleichs unendlicher Mengen, ernsthafte psychische Probleme. Ernst Zermelo umging Russells Paradoxon, indem er Cantors natürlichsprachliche Definition durch ein Schema von abzählbar vielen Axiomen ersetzte. Seine Axiomatisierung der Mengenlehre von 1908 setzte sich durch und wurde bis heute vielfach erweitert - durch Abraham Fränkel, Thoralf Skolem, Johann von Neumann, Paul Bernays und andere.

Russell hatte zu demselben Zweck Typen eingeführt und verlangt, dass jede Menge nur Elemente gewisser Typen enthalten dürfe. Die bereits in den Principia Mathematica enthaltene Typentheorie entwickelt sich heute unter Per Martin-Löf zu einem eigenständigen Versuch, eine Grundlage für die Mathematik zu bieten. Daneben gibt es auch eine pragmatische Ausprägung, die vor allem den Wert von Typsystemen in der Entwicklung und Untersuchung von Programmiersprachen einsetzt. Heute kann das Type-Checking als eine der effizientesten Methoden bei der Fehlersuche in Programmen bezeichnet werden.

Man musste einsehen, dass die von Gödels Satz gerechtfertigte reine Logik "erster Stufe" offenbar zu schwach war, um die gesamte Mathematik zu erfassen. Schon Leopold Löwenheim (1915) und Skolem (1920) hatten gesehen, dass jedes Axiomensystem für die reellen Zahlen auch auf Objekte zutraf, die man garnicht beschreiben wollte (sogenannte Nonstandardmodelle). Aus dieser Beobachtung entstand die Modelltheorie. Heute ist das Model-Checking eine Technik, die von rechnergestützten Beweissystemen eingesetzt wird.

Die Nonstandard-Methoden kamen, aufbauend auf Grundlagen von Alfred Tarski in der Nonstandard-Zahlentheorie aus dem Jahre 1934, durch die Arbeiten von Leon Henkin und Abraham Robinson in der Nonstandard-Algebra und vor allem in der Nonstandard-Analysis ab 1966 zur Blüte, da mit ihnen ein altbewährter Kalkül von Gottfried Wilhelm Leibniz wiederentdeckt wurde und endlich theoretisch fundiert werden konnte, der der auf Augustin Cauchy zurückgehenden Analysis an Einfachheit der Argumentation weit überlegen ist. Sie können sich davon auf unserem Poster über Nonstandard-Analysis -- Rechnen mit unendlich kleinen Zahlen überzeugen.

Waren die mit den Nonstandard-Modellen einhergehenden Antinomien noch als unerwünschte Randerscheinungen hinnehmbar, so waren die beiden zentralen Sätze aus Gödels Habilitationsschrift für Hilberts Programm anscheinend vernichtend:

(1. Unvollständigkeitssatz.) In jeder einigermaßen interessanten Theorie lassen sich Probleme formulieren, die in dieser Theorie nicht lösbar sind.

(2. Unvollständigkeitssatz.) Die Widerspruchsfreiheit jeder einigermaßen interessanten Theorie ist mit ihren eigenen Mitteln nicht beweisbar.

Dabei heißt eine Theorie schon einigermaßen interessant, wenn man in ihr mit natürlichen Zahlen rechnen kann.

Nach diesem Donnerschlag hätten alle Formalisten und Logizisten einpacken können - wie Hilbert es tat. Der Traum war ausgeträumt. Aber das Gegenteil passierte. Gerhard Gentzen zeigte die Widerspruchsfreiheit der Zahlentheorie unter Zuhilfenahme eines in der Zahlentheorie selbst nicht beweisbaren, da mächtigeren, Prinzips; und in seiner Folge entstand eine Schule der Beweistheorie, die angeführt vom ersten Lehrstuhlinhaber für Mathematische Logik an der LMU, Kurt Schütte, systematisch Theorien bezüglich ihrer Beweisstärke miteinander verglich. Über die Ziele, Methoden und Ergebnisse informieren einige Zitate von Schütte, die Sie auf einem extra Poster über Beweistheorie finden können.

Ein etwas anderer Zweig der Beweistheorie, der auf Gentzens Dissertation Untersuchungen über das logische Schließen von 1933 zurückgeht, beschäftigt sich mit der Aufgabe, Beweise schematisch, aber effizient, so umzuformulieren, dass man aus ihnen möglichst viel Information ablesen kann.

(Hauptsatz.) Jeder Beweis, der unter Zuhilfenahme bewiesener Hilfssätze geführt wurde, kann auch direkt geführt werden.
Wir verfolgen diese Richtung derzeit am Lehrstuhl für Mathematische Logik mit der Entwicklung des interaktiven Beweissystems MINLOG, einem Prototypen zur Entwicklung garantiert korrekter Software.

Die Beweise der Gödelschen Sätze beruhen zum großen Teil auf geschickten Codierungen aller Objekte der formalen Logik in Zahlen und berechenbaren Funktionen über Zahlen. Dieser Zweig, die Rekursionstheorie, erlangte in den Fünfzigerjahren einhergehend mit der Entwicklung erster programmierbarer Rechner große Bedeutung. Die bekannteste aller "Maschinen" (idealisierte Rechner) stammt von Alain Turing (dem berühmten Knacker des deutschen U-Boot-Funkcodes im 2. Weltkrieg). Unter den führenden Rekursionstheoretikern jener Zeit unbedingt zu nennen ist Rózsa Péter, eine der leider bis vor nicht allzu langer Zeit wenigen Frauen in der Logik. (Man möge deshalb die in dieser historischen Betrachtung fast durchgehend maskulinen Formulierungen verzeihen!)

Etwa gleichzeitig entwickelte sich eine Kultur des formalen Rechnens, die darauf abzielte, alle berechenbaren Funktionen auf zwei Grundfunktionen, die Abstraktion f(x)->f(·) und die Applikation (f,x)->f(x), sowie eine einfache Ersetzungsregel f(·)(x)=>f(x) zurückzuführen. Haskell B. Curry und Alonzo Church waren unterschiedlicher Auffassung, ob man nur Objekte zulassen sollte, die im Sinne der Typentheorie wohlgeformt waren. Tatsächlich hatte die ungetypte Version kein Modell in der Mengenlehre und ließ sich erst in den sechziger Jahren durch Dana Scotts Bereichstheorie erklären. Hendrik Barendregt hat inzwischen zuerst über die ungetypte, dann über die getypte Version zwei dicke Bücher geschrieben, die in Fachkreisen scherzhaft das Alte und das Neue Testament genannt werden.

Bereits zu Beginn des Jahrhunderts war eine alternative Schule entstanden, die den Weg der Anschauung auch in der Logik nicht verlassen wollte. Der Topologe Luitzen Egbertus Jan Brouwer forderte 1908 in seiner Schrift über die Unzuverlässigkeit der logischen Prinzipien, dass ein Beweis stets eine geistige Konstruktion sein solle, und lehnte inkonstruktive Hilfsmittel, insbesondere Beweise durch Widerspruch, ab. Er wehrte sich auch gegen jegliches formale Schließen. Bezeichnenderweise hat sein Schüler, der Logiker Arend Heyting, dann doch 1930 in einem Buch die formalen Regeln der intuitionistischen Logik und Mathematik aufgestellt. Die intuitionistische Logik hat als Konkurrenzprodukt zur klassischen Logik überlebt, weil sie sich von ihren ideologischen Vorgaben löste und mittels der Erkenntnis von Curry und William A. Howard, dass Beweise in der intuitionistischen Version von Gödels Kalkül des Natürlichen Schließens und Programme funktionaler Programmiersprachen sich formal gesehen exakt gleich verhalten, wunderbar in der Informatik anwenden läßt.

Wegen ihrer hohen algorithmischen Aussagekraft ist die konstruktive Mathematik, die sich Ihnen auf einem eigenen Poster näher vorstellt, von großer Bedeutung. Um den Ansprüchen gerecht zu werden, war harte Arbeit notwendig, bis der größte Teil der klassischen Analysis konstruktiv neu bewiesen war. Errett Bishop hat dies getan. Die konstruktive Mathematik kann in gewisser Weise als Antipode zur eleganten, doch höchst inkonstruktiven Nonstandard-Mathematik betrachtet werden. Auch hier zeigt sich die enorme Spannbreite logischer Methoden in der Mathematik.

Andere nichtklassische Logiken sind in den letzten Jahrzehnten anwendungsbezogen entstanden; so z.B. temporale Logiken zur Beschreibung von Abläufen, nichtmonotone Logiken als Grundlage der Programmiersprachenfamilie Prolog (= Programming in Logic) und für Datenbanksysteme, sowie 1987 Jean-Yves Girards Lineare Logik als Kalkül für speicherplatzrelevante Probleme und zur Modularisierung von Aufgaben in modernen Parallelrechnern.

So kann man am Beispiel der mathematischen Logik deutlich sehen, wie sich eine Grundlagenkrise innerhalb eines Jahrhunderts zu einer Vielzahl von Disziplinen entwickelt hat, für die inzwischen von Anwenderseite, d.h. vor allem aus der Informatik, akuter Bedarf an Spezialwissen, Spezialisten und genauso natürlich auch an Spezialistinnen besteht. Siehe dazu auch unser Poster über Beweistheorie in der Informatik! (Das mit dem Bedarf war anscheinend schon immer so.)

Die aktuellen Forschungen der derzeit 22 Mitglieder der Arbeitsgruppe Mathematische Logik an der Ludwig-Maximilians-Universität erstrecken sich über fast alle der hier angesprochenen Themenbereiche - natürlich in einer Tiefe der Fragestellungen, die sich auf wenigen Seiten nicht darstellen lässt. Einen Ausschnitt der Themen sehen Sie auf unserer Auswahl von Veröffentlichungen.

Seit 1. April 1997 existiert ein Graduiertenkolleg, d.h. ein Forschungsverbund und gleichzeitig eine Fördereinrichtung für Doktorandinnen und Doktoranden, mit derzeit 37 Mitgliedern von unserer und der Technischen Universität, sowie von mehreren grossen Unternehmen mit dem gemeinsamen Thema Logik in der Informatik.

Alle zwei Jahre organisieren wir eine internationale Sommerschule mit etwa 100 Fachkolleginnen und -kollegen aus allen Teilen der Welt, um unserem akademischen Nachwuchs die internationale Bühne, für die er bestens gerüstet ist, zu erschließen.


25.1.2000, Wolfgang Zuber