Extraction of effective uniform bounds from proofs based on sequential compactness via logical analysis
Final Report Abstract
In den letzten 20 Jahren hat sich, wesentlich durch die Arbeiten des Berichterstatters und seiner Mitarbeiter, eine angewandte Form von Beweistheorie (,,Proof Mining”) als ein neues Teilgebiet der Logik etabliert. Hierbei geht es um die Anwendung beweistheoretischer Transformationen (sogenannter Beweisinterpretationen, die auf neuen Formen und Erweiterungen von Gödels berühmter Funktionalinterpretation basieren) auf konkrete (meist nicht effektive) Beweise innerhalb der Mathematik mit dem Ziel der Gewinnung neuer Daten (wie z.B. effektiver Schranken). Dies hat insbesondere zu zahlreichen Anwendungen in der Nichtlinearen Analysis (metrische Fixpunkttheorie, Ergodentheorie, konvexe Optimierung, Cauchy-Probleme) geführt. In diesem Projekt stand die Analyse von Beweisen, die auf starker und schwacher Folgenkompaktheit basieren, im Vordergrund. Dazu wurden zunachst die in Proof Mining verwendeten Beweistransformationen auf diese Kompaktheitsprinzipien, aber auch auf noch inkonstruktivere Methoden wie Ultrapotenzen oder Banach-Limiten ausgeweitet. Zudem wurden erstmals in diesem Kontext kombinatorische Prinzipien, wie der Satz von Ramsey (für Paare), oder das sogenannte Cohesiveness Prinzip, die eng mit Kompaktheitsprinzipien zusammenhängen, behandelt. Für die Extraktion extrem uniformer Schranken ist es wesentlich, auszunutzen, dass die analysierten Beweise nur abstrakte Charakterisierungen der im spezifischen Kontext verwendeten Klassen metrischer und normierter Strukturen verwenden. Im Rahmen des Projektes gelang es die bislang in Proof Mining verwendeten Klassen stark zu erweitern: so konnte zusammen mit Daniel Günzel gezeigt werden, dass sämtliche normierten Strukturen, die in der sogenannten ,,positive bounded logic” axiomatisiert werden können, beweistheoretische Metatheoreme zur Extraktion uniformer effektiver Schranken ermöglichen. Zusammen mit Adriana Nicolae wurde dies kürzlich auch für die wichtige Klasse von Gromovs CAT(κ)-Raumen mit κ > 0 gezeigt. Neben zahlreichen theoretischen und innerlogischen Resultaten war ein Hauptthema des Projekts die Anwendungen der genannten Methoden auf konkrete Beweise in der Nichtlinearen Analysis. Hierbei gelang es, neue effektive Konvergenzraten für sogenannte asymptotische Regularitätsaussagen sowie Metastabilitätsraten (im Sinne von T. Tao) für iterativen Verfahren in der Fixpunkttheorie, der nichtlinearen Ergodentheorie und erstmals auch der konvexen Optimierung (Proximal Point Algorithm, Convex Feasibility Problems, Yamada’s ,,Hybrid steepest descent” Methode) zu extrahieren, die in Fachzeitschriften der entsprechenden Gebiete bzw. allgemeinen mathematischen Fachzeitschriften (wie z.B. Adv. Math.) veröffentlicht wurden. Die mehr theoretischen Resultate zu den logischen Grundlagen des ,,Proof Mining” wurden in führenden Fachzeitschriften im Bereich Logik, aber auch in allgemeinen mathematischen Zeitschriften veröffentlicht. Über die Resultate dieses Projekts wurde auf mehr als 30 internationalen Tagungen vorgetragen.
Publications
- On quantitative versions of theorems due to F.E. Browder and R. Wittmann. Adv. Math. 226, pp. 2764-2795 (2011)
Kohlenbach, U.
- The cohesive principle and the Bolzano-Weierstraß principle. Math. Logic Quart. 57, 292-298 (2011)
Kreuzer, A.P.
- A quantitative nonlinear strong ergodic theorem for Hilbert spaces. J. Math. Anal. Appl. 391, pp. 26-37 (2012)
Safarik, P.
(See online at https://doi.org/10.1016/j.jmaa.2012.02.038) - A uniform quantitative form of sequential weak compactness and Baillon’s nonlinear ergodic theorem. Comm. Contemp. Math. 14, 20pp. (2012)
Kohlenbach, U.
(See online at https://doi.org/10.1142/S021919971250006X) - Effective metastability of Halpern iterates in CAT(0) spaces. Adv. Math. 231, pp. 2526-2556 (2012). Addendum in: Adv. Math. 250, pp. 650-651, 2014)
Kohlenbach, U., Leu¸stean, L.
- Gödel functional interpretation and weak compactness. Ann. Pure Appl. Logic 163, pp. 1560-1579 (2012)
Kohlenbach, U.
(See online at https://doi.org/10.1016/j.apal.2011.12.009) - Term extraction and Ramsey’s theorem for pairs. J. Symbolic Logic 77, pp. 853-895 (2012)
Kreuzer, A.P., Kohlenbach, U.
(See online at https://doi.org/10.2178/jsl/1344862165) - Fluctuations, effective learnability and metastability in analysis. Ann. Pure Appl. Log. 165, pp. 266-304 (2014)
Kohlenbach, U., Safarik, P.
(See online at https://doi.org/10.1016/j.apal.2013.07.014) - Rates of metastability for Bruck’s iteration of pseudocontractive mappings in Hilbert space. Numer. Funct. Anal. Optimiz. 35, pp. 20-31 (2014)
Kornlein, D., Kohlenbach, U.
(See online at https://doi.org/10.1080/01630563.2013.809361) - Logical metatheorems for abstract spaces axiomatized in positive bounded logic. Adv. Math. 290, 503-551 (2016)
Günzel, D., Kohlenbach, U.
(See online at https://doi.org/10.1016/j.aim.2015.12.007) - On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces. Israel Journal of Mathematics 216, pp. 215-246 (2016)
Kohlenbach, U.
(See online at https://doi.org/10.1007/s11856-016-1408-4) - Quantitative Analysis of Iterative Algorithms in Fixed Point Theory and Convex Optimization. Technische Universität Darmstadt, Ph.D. Thesis, 2016
Körnlein, D.
