Kursinformation

Zusammenfassung:
Der in Greifswald geborene Gerhard Gentzen (1909-1945) ist einer der wichtigsten Logiker des 20. Jahrhunderts. Als er 26 Jahre alt war, veröffentlichte er in der Mathematischen Zeitschrift die Artikel „Untersuchungen über das logische Schließen I“ und „Untersuchungen über das logische Schließen II“, womit er die moderne Beweistheorie gründete. Wir werden Gentzens Arbeiten und deren Einbettung in der Philosophie der Mathematik der Zwischenkriegszeit anhand einer gerade erschienenen, für Philosophiestudierenden geschriebenen Einführung in die Beweistheorie studieren. Die erste Hälfte dieser Einführung behandelt Themen der strukturellen Beweistheorie, darunter die Gödel-Gentzen-Übersetzung der klassischen in die intuitionistische Logik, die Theorie des natürlichen Schließens und deren Normalisierungssätze, Gentzens Sequenzenkalküle und sein ‚Hauptsatz‘ (das Schnitteliminationstheorem) für diese Kalküle.

Struktur und Voraussetzungen:
Das Hauptseminar enthält 14 Sitzungen, in denen wir die zentralen Definitionen und Sätze mit Beispielen und Beweisen erkunden und erklären werden. Zulassungsvoraussetzung ist eine vollständig abgeschlossene logische Propädeutik.

Prüfung:
Weil Studierende die Theorie nur lernen können, wenn sie viel mit der Materie spielen und üben, wird am Ende jeder Sitzung eine Aufgabe ausgereicht. Die Studierenden reichen am Anfang der nächsten Sitzung ihre eigene handgeschriebene, aber lesbare Lösung ein. Um dieses Hauptseminar zu bestehen, müssen Studierende mindestens 12 von den 14 Aufgaben ihrer eigenen Lösungen einreichen.

Literatur:
Paolo Mancosu, Sergio Galvan und Richard Zach (2021). An Introduction to Proof Theory. Oxford: Oxford University Press.