Applied Proof Theory

Diese Vorlesung entwickelt die wichtigsten Methoden der angewandten Beweistheorie, nämlich sogenannte Beweisinterpretationen, und gibt Anwendungen in unterschiedlichen Gebieten der Mathematik wie Approximationstheorie, nichtlineare Analysis, Ergodentheorie. Bei diesen Anwendungen geht es um die Extraktion effektiver Schranken und neuer Uniformitätsaussagen aus prima facie ineffektiven Beweisen. Die hauptsächlich behandelten Methoden sind: Herbrand-Theorie, Kreisels no-counterexample Interpretation, modifizierte Realisierbarkeit (Kreisel), Gödels Funktionalinterpretation, Negativübersetzungen (Gödel), Funktionalinterpretation der vollen Analysis (Spector), monotone Interpretationen und ihre Erweitung auf Systeme mit Klassen von abstrakten (nicht separablen) Strukturen, wie allgemeinen metrischen, hyperbolischen und normierten Räumen.