Logische Extraktion von effektiven uniformen Schranken aus Beweisen, die auf Folgenkompaktheit basieren.

• Antragsteller: Professor Dr. Ulrich Kohlenbach
• Fachliche Zuordnung: Mathematik
• Förderung: Förderung von 2009 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 108728300

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 des beantragten Projekts ist.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Vassilios Gregoriades, Ph.D.