Mathematische Logik

Gegenstand und Bedeutung

Die mathematische Logik, auch symbolische Logik genannt, ist ein Teilgebiet der Mathematik und eine Anwendung der modernen formalen Logik. Sie dient besonders als Methode der Metamathematik, also zur mathematischen Untersuchung der Grundlagen, Begriffe und Verfahren der Mathematik selbst. Ihre Forschung wurde durch Fragen nach den Grundlagen der Mathematik angeregt und hat wesentlich zu deren Untersuchung beigetragen.

Ein zentrales Ziel ist es, die Ausdrucksstärke formaler Logiken und formaler Beweissysteme zu bestimmen. Formale Systeme verwenden genau festgelegte Zeichen, Regeln und Schlussverfahren. Ihre Komplexität und Leistungsfähigkeit lassen sich unter anderem daran messen, welche Aussagen in ihnen definiert oder bewiesen werden können.

Dabei werden zwei Seiten unterschieden: Die Syntax untersucht formale Zeichenketten und ihre regelgerechte Bildung. Die Semantik beschäftigt sich mit der Bedeutung, die solchen Zeichenketten durch Interpretationen oder Modelle gegeben wird.

Formale logische Systeme

Die mathematische Logik untersucht mathematische Begriffe, die durch formale logische Systeme ausgedrückt werden. Das am weitesten verbreitete System ist die Prädikatenlogik erster Stufe. Sie erweitert die Aussagenlogik um Prädikate, Variablen und Quantoren und ist sowohl für die Grundlagen der Mathematik als auch wegen ihrer Eigenschaften der Vollständigkeit und Korrektheit besonders wichtig.

Daneben werden die Aussagenlogik, stärkere klassische Logiken wie die Prädikatenlogik zweiter Stufe und nichtklassische Systeme wie die intuitionistische Logik untersucht. Die klassische symbolische Logik ist mit der Logik von Aristoteles vergleichbar, formuliert ihre Aussagen und Schlussregeln jedoch mit Symbolen statt in natürlicher Sprache.

Die vier Hauptgebiete

Das Handbook of Mathematical Logic von 1977 unterscheidet vier Hauptgebiete:

• Die Mengenlehre untersucht Mengen, also abstrakte Zusammenfassungen von Objekten. Einfache Begriffe wie die Teilmenge gehören zur naiven Mengenlehre. Die moderne Forschung arbeitet vor allem axiomatisch und fragt mit logischen Methoden, welche Aussagen in formalen Theorien wie der Zermelo-Fraenkel-Mengenlehre mit Auswahlaxiom (ZFC) oder New Foundations beweisbar sind.

• Die Beweistheorie untersucht formale Beweise und logische Deduktionssysteme, also genau geregelte Verfahren zum Ableiten von Aussagen. Beweise werden dabei selbst als mathematische Objekte dargestellt und mit mathematischen Methoden analysiert. Frege formalisierte den Begriff des Beweises.

• Die Modelltheorie untersucht Modelle formaler Theorien. Ein Modell ist eine mathematische Struktur, in der die Aussagen einer Theorie gelten. Die Gesamtheit aller Modelle einer bestimmten Theorie heißt „elementare Klasse“. Die klassische Modelltheorie erforscht die Eigenschaften solcher Modelle und prüft, ob bestimmte Klassen von Strukturen elementar sind. Mithilfe der Quantorenelimination können Aussagen so umgeformt werden, dass Quantoren entfallen; dadurch lässt sich zeigen, dass die Modelle bestimmter Theorien nicht zu kompliziert sein können.

• Die Rekursionstheorie, auch Berechenbarkeitstheorie genannt, untersucht berechenbare Funktionen. Turinggrade ordnen nicht berechenbare Funktionen nach dem Grad ihrer Nicht-Berechenbarkeit. Zum Gebiet gehören außerdem die verallgemeinerte Berechenbarkeit und die Definierbarkeit.

Die Grenzen zwischen diesen Bereichen sind nicht scharf. Gödels Unvollständigkeitssatz ist beispielsweise sowohl für die Rekursions- als auch für die Beweistheorie bedeutend und führte zum Satz von Löb, der in der Modallogik wichtig ist. Auch die Kategorientheorie verwendet ähnliche formale und axiomatische Methoden, wird aber üblicherweise nicht zur mathematischen Logik gezählt.

Entwicklung und Informatik

Frühe Versuche, logische Operationen symbolisch oder algebraisch zu behandeln, stammen unter anderem von Gottfried Wilhelm Leibniz und Johann Heinrich Lambert, blieben jedoch weitgehend isoliert und unbekannt. In der Mitte des 19. Jahrhunderts entwickelten George Boole und Augustus de Morgan einen systematischen Zugang. Dadurch wurde die traditionelle aristotelische Logik reformiert und zu einem geeigneten Werkzeug für die Untersuchung mathematischer Grundlagen erweitert. Der Artikel betont allerdings, dass damit nicht sämtliche grundlegenden Kontroversen der Jahre 1900 bis 1925 geklärt wurden.

Historisch wichtige Veröffentlichungen sind Gottlob Freges Begriffsschrift, die von Charles Sanders Peirce herausgegebenen Studies in Logic, die Principia Mathematica von Bertrand Russell und Alfred North Whitehead sowie Kurt Gödels Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.

Zwischen mathematischer Logik und Informatik bestehen enge Verbindungen. Pioniere der Informatik wie Alan Turing arbeiteten zugleich als Mathematiker und Logiker. Teile der mathematischen Logik gehören heute zur theoretischen Informatik. Die deskriptive Komplexitätstheorie verbindet logische Beschreibungen mit der Komplexitätstheorie. Die endliche Modelltheorie steht in enger Beziehung zur Automatentheorie: Nach dem Satz von Büchi ist eine Sprache genau dann in MSO, der monadischen Logik zweiter Stufe, definierbar, wenn sie regulär ist.

Grundlegende Ergebnisse

• Der Satz von Löwenheim-Skolem von 1919 besagt: Besitzt eine Theorie in einer abzählbaren Sprache der ersten Ordnung ein unendliches Modell, dann besitzt sie Modelle jeder unendlichen Kardinalität.

• Gödels Vollständigkeitssatz von 1929 zeigt für die klassische Prädikatenlogik erster Stufe die Äquivalenz von semantischem und syntaktischem Folgern. Eine logisch in allen Modellen folgende Aussage kann demnach auch formal hergeleitet werden, und umgekehrt.

• Gödels Unvollständigkeitssatz von 1931 zeigt, dass kein genügend starkes formales System seine eigene Konsistenz beweisen kann.

• Alan Turing und Alonzo Church entdeckten 1936 unabhängig voneinander die algorithmische Unlösbarkeit des Entscheidungsproblems. Es gibt kein Computerprogramm, das für jede beliebige mathematische Aussage korrekt entscheidet, ob sie wahr ist.

• Die Kontinuumshypothese ist von ZFC unabhängig: Innerhalb von ZFC sind weder sie noch ihre Widerlegung beweisbar. Gödel zeigte 1940, dass ZFC zusammen mit der Kontinuumshypothese konsistent ist, falls ZFC konsistent ist. Paul Cohen bewies 1963 entsprechend die Konsistenz von ZFC zusammen mit der Negation der Kontinuumshypothese, sofern ZFC konsistent ist.

• Juri Matijassewitsch zeigte 1970 die algorithmische Unlösbarkeit von Hilberts zehntem Problem. Es gibt kein Computerprogramm, das für jedes Polynom in mehreren Variablen mit ganzzahligen Koeffizienten korrekt entscheidet, ob es ganzzahlige Nullstellen besitzt.