Stärken und Schwächen

Zusammenfassung

In Abschnitt 3B3 haben wir Semi-Entscheidungsverfahren für Widersprüchlichkeit und logische Folgerung konstruiert: Algorithmen, die im positiven Fall immer, aber im negativen Fall nicht notwendig terminieren; wenn sie terminieren, erhält man die korrekte Antwort. Der amerikanische Logiker Alonzo Church und unabhängig der englische Mathematiker Alan Turing haben 1936 gezeigt, daß man die Semi-Entscheidungsverfahren nicht wie in der Aussagenlogik zu Entscheidungsverfahren verbessern kann. Die Eigenschaften sind unentscheidbar — auch schon in der offenen Prädikatenlogik. Den Beweis skizzieren wir in den ersten fünf Abschnitten dieses Kapitels. Dazu präsentieren wir in 3D1 ein unentscheidbares Problem über das Terminieren von Programmen, formalisieren in 3D2 das Umgehen mit Programmen (Rechnen) in Wörtern und schließen daraus in 3D3, daß die Theorie der Wörter unentscheidbar und daher nicht axiomatisierbar ist. In 3D4 axiomatisieren wir das Rechnen in der Theorie der Wörter und folgern in 3D5, daß die Prädikatenlogik selbst unentscheidbar ist. In den weiteren Abschnitten bauen wir darauf auf und ernten die Früchte der ganzen Arbeit bis hierher: In 3D6 konkretisieren wir die Nichtaxiomatisierbarkeit der Wörtertheorie, indem wir zu jedem angeblichen Axiomensystem eine wahre Formel konstruieren, die nicht daraus folgt. Die Nichtaxiomatisierbarkeitsergebnisse aus 3D3 und 3D6 hat Gödel 1931 für die Zahlentheorie bewiesen, indem er Berechnungen in Zahlen codierte. Codierungen in Wörter erwiesen sich später als einfacher. Wir übersetzen umgekehrt in 3D8 und 3D9 die Ergebnisse in die Zahlentheorie und gewinnen so die berühmten Gödelschen Nichtableitbarkeitssätze. Davor skizzieren wir in 3D7 einen ähnlichen Beweis von Tarski, daß man den Begriff ‘wahr in einem System’ in dem System selbst nicht formalisieren kann. In 3D10 erweitern wir die Logik ein Stück weit in die Mengenlehre hinein (Logik 2. Stufe); die Schwierigkeiten werden dadurch nur größer. Zum Schluß (3D11) nehme ich auf, was ich im ganzen Buch immer wieder übers Formalisieren im Großen und im Kleinen gesagt habe.