Extraction of effective bounds from proofs based on sequential compactness via logical analysis

In den letzten 15 Jahren hat sich als neues Teilgebiet der Logik eine angewandte Form von Beweistheorie ("Proof Mining") etabliert, in der es um die Anwendung beweistheoretischer Transformationen auf konkrete (insbesondere ineffektive) Beweise innerhalb der Mathematik mit dem Ziel der Gewinnung neuer Daten (wie z.B. effektiver Schranken) geht. Dieses Projekt behandelt einen besonders schwierigen Aspekt dieser Forschung, nämlich die Analyse von Beweisen, die wesentlichen Gebrauch von (hochgradig ineffektiven) Folgenkompaktheitsargumenten machen. Während sich Beweise, die auf Heine-Borel Kompaktheit basieren (logisch gesprochen korrespondiert dies zu dem binären Lemma von König), mit den existierenden Techniken gut analysieren lassen, stellen Anwendungen von Kompaktheitsargumenten wie dem Satz von Arzela-Ascoli, Hellys Theorem für Funktionen mit beschränkter Variation oder der Gebrauch der schwachen Kompaktheit der Einheitskugel in gleichmäßig konvexen normierten Räumen große Schwierigkeiten für eine effektive und quantitative Analyse von Beweisen dar. Gleichwohl gibt es hier in der jüngsten Zeit erhebliche Fortschritte, deren Weiterentwicklung und Anwendung Gegenstand dieses Projekts ist.