Beweise selbst zum Gegenstand der Betrachtung zu machen, speziell über Manipulationen von Beweisen zu berichten, das ist die Grundidee von Hilberts Beweistheorie. Hilbert wollte so unter Beschränkung auf informelle finitistische Methoden die Konsistenz wichtiger formaler mathematischer Theorien T nachweisen. Im Lichte speziell von Gödels Unvollständigkeitssätzen mag dies nicht funktionieren. Eine Variante davon -- man gelangt zu Informationen über T und die Beziehung zwischen T und einer formalen Theorie S, indem man in S das Herleiten in T formalisiert -- ist allerdings zu einem erfolgreichen Programm der Metamathematik geworden.
Wir werden uns in diesem Seminar nur mit dessen Anfangsgründen befassen. Es wird um PA (die Peano-Arithmetik), Teiltheorien T bzw. S von PA und geringfügige Erweiterungen T bzw. S von PA gehen. Die Standardresultate sollen vorgestellt und diskutiert werden: es geht (in Schlagworten) um die Ordinalzahl von T bzw. S, um beweistheoretische Reduzierbarkeit, vielleicht um die beweisbar rekursiven Funktionen von T bzw. S und um relative Interpretierbarkeit. Dabei sollen einige Teile der einschlägigen Beweise etwas detaillierter als üblich ausgearbeitet werden.
Hierbei werden verschiedene philosophische Themen paradigmatisch behandelt: intertheoretische Relationen, die Tragweite syntaktischer Methoden, das Explizitmachen von Implizitem.
- Kursverantwortliche/r: Ben Jähnert
- Kursverantwortliche/r: Karl-Georg Niebergall
- Kursverantwortliche/r: Hannah Theis