Professor of Mathematics
Research Group LogicI obtained my PhD (Dr.phil.nat.) in 1990 from the
Department of Mathematics
of the
J.W.Goethe-Universitaet Frankfurt (Germany).
In 1995 I got my Habilitation (`venia legendi') from the Department
of Mathematics of the University of Frankfurt.
During the academic year 1996-97 I was a visiting assistant professor
in the Department of
Mathematics of the University
of Michigan, Ann
Arbor. In July 1997, I joined BRICS
and the Department of Computer
Science of Aarhus
University (Aarhus, Denmark) where I became tenured associate professor
in 2000. Since April 2004
I am full professor of mathematics at Technische Universität
Darmstadt.
Research Interests: Logic (in particular proof theory, computability theory and constructive reasoning) with applications to mathematics and computer science, computational content of proofs, proof interpretations and their use in mathematics, functionals of higher type, computability and complexity in analysis, approximation theory, nonlinear analysis, fixed point theory, ergodic theory.
Here is my Curriculum Vitae: CV.pdf.Current teaching (Summer term 2014):
Editorial Work:
Other professional activities:
Association for Symbolic Logic (Vice President)
Wissenschaftliche Gesellschaft an der J.W.Goethe-Universität zu Frankfurt am Main (Corresponding Member)
PhD Students:
Publications:
Book: Ulrich Kohlenbach: "Applied Proof Theory: Proof Interpretations and their Use in Mathematics". Springer Monographs in Mathematics, xx+536pp., 2008. Articles:Majorizable functionals and recursion theoretical models for W. Friedrichs calculi of functionals (german). Master thesis. Frankfurt 1986, pp. 91.
Theory of majorizable and continuous functionals and their use for the extraction of bounds from non-constructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness (german). PhD Dissertation, Frankfurt 1990, pp.xxii+278.
Pointwise hereditary majorization and some application.. Final version in: Arch. Math. Logic 31, pp. 227-241 (1992).
Remarks on Herbrand normal forms and Herbrand realizations. Final version in: Arch. Math. Logic 31, pp. 305-317 (1992).
Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. J. Symbolic Logic 57, pp. 1239-1273 (1992).
Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallee Poussin's proof for Chebycheff approximation. Final version in: Annals of Pure and Applied Logic 64, pp. 27-94 (1993).
New effective moduli of uniqueness and uniform a-priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Final version in: Numer.Funct.Anal.and Optimiz. 14, pp. 581-606 (1993).
A note on the $\Pi^0_2$-induction rule. Final version in: Arch. Math. Logic 34, pp. 279-283 (1995).
Real growth in standard parts of analysis. Habilitationsschrift, pp. xv+166, Frankfurt 1995.
Analysing proofs in analysis. Final version in: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pp. 225-260, Oxford University Press (1996).
Mathematically strong subystems of analysis with low rate of growth of provably recursive functionals. Final version in: Arch. Math. Logic 36, pp. 31-71 (1996).
Elimination of Skolem functions for monotone formulas in analysis. Final version in: Arch. Math. Logic 37 pp. 363-390 (1998).
Arithmetizing proofs in analysis. Final version in: Larrazabal, J.M., Lascar, D., Mints, G. (eds.), Logic Colloquium '96, Springer Lecture Notes in Logic 12, pp. 115-158 (1998).
Proof theory and computational analysis. Electronic Notes in Theoretical Computer Science, Vol. 13, Elsevier (1998).
Relative constructivity. Final version in: J. Symbolic Logic 63, pp. 1218-1238 (1998).
On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness. Final version in: Ann. Pure Applied Logic 95, pp. 257-285 (1998).
The use of a logical principle of uniform boundedness in analysis. Final version in: Cantini, A., Casari, E., Minari, P. (eds.), Logic and Foundations of Mathematics. Synthese Library 280, pp. 93-106. Kluwer Academic Publishers (1999).
A note on Goodman's theorem. Final version in: Studia Logica 63, pp. 1-5 (1999).
On the no-counterexample interpretation. Final version in: J. Symbolic Logic 64, pp. 1491-1511 (1999).
Things that can and things that can't be done in PRA. Final version in: Ann. Pure Applied Logic 102, pp. 223-245 (2000).
A note on Spector's quantifier-free rule of extensionality. Final version in: Arch. Math. Logic 40, pp. 89-92 (2001).
On the computational content of the Krasnoselski and Ishikawa fixed point theorems. Final version in: Proceedings of the Fourth Workshop on Computability and Complexity in Analysis, J. Blanck, V. Brattka, P. Hertling, K. Weihrauch (eds.), Springer LNCS 2064, pp. 119-145 (2001).
Intuitionistic choice and restricted classical logic. Final version in: Math. Logic Quaterly 47, pp. 455-460 (2001).
A quantitative version of a theorem due to Borwein-Reich-Shafrir. Final version in: Numer. Funct. Anal. and Optimiz. 22, pp. 641-656 (2001).
On uniform weak König's lemma. Final version in: Ann. Pure Applied Logic 114, pp. 103-116 (2002).
Foundational and mathematical uses of higher types. Final version in: Sieg, W. et al. (eds.), Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman. Lecture Notes in Logic vol. 15, pp. 92-116, A.K. Peters (2002).
On weak Markov's principle. Final version in: Math. Logic Quaterly 48, suppl 1, pp. 59-65 (2002).
Applied foundations: proof mining in analysis. Final version in: Newsletter of the Danish Mathematical Society (`Matilde'), vol. 13, pp. 7-9 (2002).
Proof mining in L_1-approximation (with Paulo Oliva). Final version in: Ann. Pure Applied Logic 121, pp. 1-38 (2003).
Uniform asymptotic regularity for Mann iterates. Final version in: J. Math. Anal. Appl. 279, pp. 531-544 (2003).
Mann iterates of directionally nonexpansive mappings in hyperbolic spaces (with Laurentiu Leustean). Final version in: Abstract and Applied Analysis, vol. 2003, no.8, pp. 449-477 (2003).
Proof mining: a systematic way of analysing proofs in mathematics (with Paulo Oliva). Final version in: Proc. Steklov Inst. Math., vol. 242, pp. 136-164 (2003).
Bounds on iterations of asymptotically quasi-nonexpansive mappings(with Branimir Lambov). Final version in: Falset, J.G., Fuster, E.L., Sims, B. (eds.), Proc. International Conference on Fixed Point Theory and Applications, Valencia 2003, pp. 143-172, Yokohama Publishers (2004)
An arithmetical hierarchy of the law of excluded middle and related principles (with Y. Akama, S. Berardi, S. Hayashi). In: Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pp. 192-201, IEEE Press (2004).
Some logical metatheorems with applications in functional analysis. Final version in: Trans. Amer. Math. Soc. vol. 357, no. 1, pp. 89-128 (2005).
A complexity analysis of functional interpretations(with Mircea-Dan Hernest). Final version in: Theoretical Computer Science vol. 338, pp. 200-246 (2005).
Higher order reverse mathematics. Final version in: Stephen G. Simpson (ed.) Reverse Mathematics 2001. Lecture Notes in Logic vol. 21, pp. 281-295. ASL, A K Peters (2005).
Extracting Herbrand disjunctions by functional interpretation(with Philipp Gerhardy). Final version in: Arch. Math. Logic. vol. 44, pp. 633-644 (2005).
Some computational aspects of metric fixed point theory. Final version in: Nonlinear Analysis vol. 61, no. 5, pp. 823-837 (2005).
Strongly uniform bounds from semi-constructive proofs(with Philipp Gerhardy). Final version in: Ann. Pure Applied Logic vol. 141, pp. 89-107 (2006).
A logical uniform boundedness principle for abstract metric and hyperbolic spaces. Final version in: Electronic Notes in Theoretical Computer Science vol. 165 (Proc. WoLLIC 2006), pp. 81-93 (2006).
The approximate fixed point property in product spaces(with Laurentiu Leustean). Final version in: Nonlinear Analysis vol. 66, pp. 806-818 (2007).
Shoenfield is Goedel after Krivine (with Thomas Streicher). Final version in: Math. Logic Quaterly vol. 53, pp. 176-179 (2007).
Proof interpretations and the computational content of proofs in mathematics. Final version in: Bulletin EATCS no.93, pp. 143-173 (2007).
Effective bounds from proofs in abstract functional analysis. Final version in: Cooper, B., Loewe, B., Sorbi, A. (eds.), New Computational Paradigms: Changing Conceptions of What is Computable. Springer Publisher, pp. 223-258 (2008).
Interview on the Philosophy of Mathematics. Final version in: Philosophy of Mathematics: 5 Questions. Henricks, V.F., Leitgeb, H. (eds.), Automatic Press/VIP, pp. 183-190, 2008.
General logical metatheorems for functional analysis(with Philipp Gerhardy). Final version in: Trans. Amer. Math. Soc. 360, pp. 2615-2660 (2008).
Gödel's functional interpretation and its use in current mathematics. Final version in: Kurt Gödel and the Foundations of Mathematics. Horizons of Truth. Baaz, M. et al. (eds.), Cambridge University Press, New York 2011. Reprinted in: dialectica Vol. 62, no. 2, pp. 223-267 (2008).
Herbrand's theorem and extractive proof theory. Final version in: SMF - Gazette des Mathematiciens 118, pp. 29-41, 2008.
A quantitative Mean Ergodic Theorem for uniformly convex Banach spaces (with Laurentiu Leustean). Final version in: Ergodic Theory and Dynamical Systems Vol. 29, pp. 1907-1915 (2009).
Ramsey's theorem for pairs and provably recursive functions (with Alexander Kreuzer). Final version in: Notre Dame Journal of Formal Logic vol. 50, pp. 427-444 (2009).
Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces (with Laurentiu Leustean). Final version in: Journal of the European Mathematical Society Vol. 12, pp. 71-92 (2010).
On Tao's "finitary" infinite pigeonhole principle (with Jaime Gaspar). Final version in: J. Symbolic Logic 75, pp. 355-371 (2010).
On the logical analysis of proofs based on nonseparable Hilbert space theory. Final version in: Feferman, S., Sieg, W. (eds.), `Proofs, Categories and Computations. Essays in Honor of Grigori Mints'. College Publications, pp. 131-143 (2010).
On the computational content of the Bolzano-Weierstrass principle (with Pavol Safarik). Final version in: Math. Logic Quaterly vol. 56, pp. 508-532 (2010).
On quantitative versions of theorems due to F.E. Browder and R. Wittmann. Final version in: Advances in Mathematics 226, pp. 2764-2795 (2011).
Effective rates of convergence for Lipschitzian pseudocontractive mappings in general Banach spaces (with Daniel Körnlein). Final version in: Nonlinear Analysis vol. 74, pp. 5253-5267 (2011).
A note on the monotone functional interpretation. Final version in: Math. Logic Quart. vol. 57, pp. 611-614 (2011).
On the asymptotic behavior of odd operators. Final version in: J. Math. Anal. Appl. vol. 382, pp. 615-620 (2011).
Gödel functional interpretation and weak compactness. Final version in: Ann. Pure Applied Logic vol. 163, pp. 1560-1579 (2012).
A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem. Final version in: Communications in Contemporary Mathematics 14, 20pp. (2012).
Term extraction and Ramsey's theorem for pairs (with Alexander P. Kreuzer). Final version in: J. Symbolic Logic 77, pp. 853-895 (2012).
Effective metastability of Halpern iterates in CAT(0) spaces. (with Laurentiu Leustean). Final version in: Advances in Mathematics vol. 231, pp. 2526-2556 (2012). Addendum. (Final version in: Advances in Mathematics vol. 250, pp. 650-651, 2014)
On the computational content of convergence proofs via Banach limits (with Laurentiu Leustean). Final version in: Philosophical Transactions of the Royal Society A vol. 370, pp. 3449-3463 (2012).
Effective metastability for modified Halpern iterations in CAT(0) spaces (with Katharina Schade). Final version in: Fixed Point Theory and Applications 2012:191, 19pp.
Bounds on Kuhfittig's iteration schema in uniformly convex hyperbolic spaces (with Muhammad Aqeel Ahmad Khan). Final version in: J. Math. Anal. Appl. vol. 403, pp. 633-642 (2013).
Rate of metastability for Bruck's iteration of pseudocontractive mappings in Hilbert space (with Daniel Körnlein). Final version in: Numer. Funct. Anal. and Optimiz. vol. 35, pp. 20-31 (2014).
Fluctuations, effective learnability and metastability in analysis (with Pavol Safarik). Final version in: Ann. Pure and Applied Logic vol. 165, pp. 266-304 (2014).
Classical provability of uniform versions and intuitionistic provability (with Makoto Fujiwara). Final version to appear in: Math. Logic Quarterly.
Quantitative image recovery theorems (with Muhammad Aqeel Ahmad Khan). Final version in: Nonlinear Analysis vol. 106, pp. 138-150 (2014).
Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators (with Angeliki Koutsoukou-Argyraki). Submitted.
Published abstracts in journals:
Constructions in classical analysis by unwinding proofs using majorizability (abstract). J. Symbolic Logic 57, p. 307 (1992).
Herbrand normal forms in subsystems of (second-order) arithmetic (abstract). J. Symbolic Logic 58, pp. 1148-1149 (1993).
Exploiting partial constructivity relatively to non-constructive lemmas in given proofs (abstract). Bull. Symbolic Logic 1, pp. 243-244 (1995).
Real growth in standard parts of analysis (abstract). Bull. Symbolic Logic 3, p. 104 (1997).
General logical principles of uniform boundedness and their mathematical strength (abstract). Bull. Symbolic Logic 3, p. 387 (1997).
Mathematically strong extensions of ACA$_0$ (abstract). Bull. Symbolic Logic 5, pp. 141-142 (1999).
On extensions of weak König's lemma (abstract). Bull. Symbolic Logic 6, p. 117 (2000).
Applied foundations: recent progress in proof mining. Abstract of Papers Presented to the Amer. Math. Soc. vol. 22, no. 3, issue 125, p. 436 (2001).
(with Paulo Oliva) Effective bounds on strong unicity in L1-approximation (abstract). Bull. Symbolic Logic 8, p. 143 (2002).
Proof theoretic applications to functional analysis (abstract). Bull. Symbolic Logic 10, pp. 122-123 (2004).
Recent uses of proof theory in nonlinear analysis and geodesic geometry. (abstract). Bull. Symbolic Logic 13, p.377 (2007).
Applied proof theory: Proof interpretations and their use in mathematics (abstract). Bull. Symbolic Logic 16, pp. 92-93 (2010).
Uniform bounds from proofs in nonlinear ergodic and fixed point theory. Abstract of Papers Presented to the Amer. Math. Soc. vol. 32, no. 1, issue 163, p.15 (2011).
Recent developments in proof mining: Bounds from proofs in nonlinear ergodic theory (abstract). Bull. Symbolic Logic 19, pp. 404 (2013).
Projects:
Principal investigator of DFG Project KO 1737/5-1: "Extraction of effective bounds from proofs based on sequential compactness via logical analysis (Feb 2009-Feb 2013).
This project has been extended (KO 1737/5-2) until January 2016.
Principal investigator of IRTG 1529 `Mathematical Fluid Dynamics' (Tokyo-Darmstadt), since 2013.
Member of Deutsch-Russisches Kooperationsprojekt "Berechnungen ueber nichtdiskreten Strukturen: Modelle, Semantik, Komplexität" (DFG 436 RUS 113/850/0-1), 2006-2008.
Member of Deutsch-Südafrikanisches Kooperationsprojekt "From continuity to computability, (DFG/NRF 445 SUA-113/20/0-1), 2007-2009.
Member of APSEM II (IST-2001-38957 Programme of EU.
Principal investigator of project of the Danish Natural Science Research Council (Sagsnr.: 21-02-0474) "Proof Mining: A Logical Approach to Computational Mathematics (2003-2005; stopped in April 2004 due to my move to Germany).
Member of Board of BRICS International PhD School, Dept. of Computer Science, Aarhus University 2000-2004.
Link to the International Research Training Group 1529: Mathematics Fluid Dynamics.
HOT SPOTS:
WoLLIC 2014, Valpariaso, Chile, Sep. 1-4.
IRTG 1529 Kickoff Meeting, Waseda University, Tokyo, Japan, June 17-18, 2014.
IRTG 1529 Research Seminar "Proof Mining and Nonlinear Analysis", TU Darmstadt, Feb. 26-28, 2014.
Universality and Homogeneity. Hausdorff Trimester Program September 2 - December 20, 2013, Bonn.
Humboldt-Kolleg "Proof", Bern, Sep. 9-13, 2013.
Honory doctorate for Prof. Dr. Harvey M. Friedman and affiliated workshop, U Gent, Sep. 4-5, 2013.
WoLLIC 2013, TU Darmstadt, August 20-23
Proof Theory in Lisbon, July 19, 2013.
Types 2013, Toulouse, April 23-26, 2013.
3rd Workshop on Proof Theory and Rewriting. Kanazawa (Japan), March 4-8, 2013.
COLD SPOTS:
Third MALOA Training Workshop, University of Oxford, Mathematical Institute, Aug.26 - Sep.1, 2012.
15th Latin American Symposium on Mathematical Logic Bogotá, Colombia, June 4-8, 2012.
Workshop on Proof Theory and Computability Theory, Tokyo, Feb. 20-23, 2012.
Ramsey Theory in Logic, Combinatorics and Complexity. Bertinoro (Italy), May 22-27, 2011.
AMS-ASL Special Session on Logic and Analysis. New Orleans, January 6-9, 2011.
Collegium Logicum: Proofs and Structures, Paris, November 8-10, 2010.
Colloquium Logicum 2010 of the DVMLG. WWU Münster, September 22-24, Germany, 2010.
Colloquium PhD's in Logic II. Tilburg University, February 18-19, 2010, The Netherlands.
Reverse Mathematics: Foundations and Applications, University of Chicago, November 6-8, 2009.
Workshop on Ergodic Theory, Queen Mary, University of London London UK, October 30, 2009.
Maltsev Meeting, Novosibirsk, 24-28 August 2009.
Logic and Mathematics Conference, University of York, 3-7 August 2009.
ASL Logic Colloquium 2009, Sofia, Bulgaria, July 31- August 5, 2009.
Leeds Symposium on Proof Theory and Constructivism, Leeds, UK, July 3-16, 2009.
Computability, Reverse Mathematics and Combinatorics, December 7-12, Banff (Canada), 2008.
Colloquium Logicum 2008, TU Darmstadt, September 10-12. 2008
British Logic Colloquium 2008, September 4-6, 2008, University of Nottingham.
Centenary Paul Wolfskehl (with Andrew Wiles), TU Darmstadt, June 30, 2008.
Mathematical Logic: Proof Theory, Constructive Mathematics. Obwerwolfach, April 6-12, 2008
L'Heritage Scientifique de Jacques Herbrand. Herbrand Centenary, February 15, 2008, ENS, Paris.
Workshop "Deduction in Semantics", Stuttgart, 10.-12.10.2007.
ASL Logic Colloquium 2007, Worclaw. July 14-19, 2007.
2006-2007 ASL Winter Meeting. January 7-8, New Orleans, USA.
Computer Science Logic 2006 (CSL 2006), 25-29 September, 2006, Szeged, Hungary.
Minisymposium on "The use of proof theory in mathematics" within the DMV 2006 Meeting, Bonn 17.-23.09.06.
MAP 2006, Castro Urdiales (Spain), 9.1.2006-13.1.2006.
CSL'05, Oxford, UK, 22-25 August 2005.
Tagung: Logik und Wissen, Darmstadt 24.-26. Juni 2005
Computability in Europe 2005: New Computational Paradigms ILLC (Amsterdam), June 8-12, 2005
Logic Meeting at UCLA to inaugurate the UCLA Logic Center, February 3-6, 2005.
Computability in Analysis. Kyushu University, Fukuoka, Nov. 22-26, 2004.
Jahrestagung der Deutschen Mathematiker- Vereinigung, Heidelberg, Sept. 12-17, 2004
Sixth
International Workshop on Computability and Complexity in Analysis,
Wittenberg, Germany, August 16-20, 2004
2003
ASL Annual Meeting
University of Illinois at Chicago, Chicago, Illinois
June 1-4, 2003
18th IEEE Conference
on Computational Complexity, BRICS, University of Aarhus, Denmark,
July 7-10, 2003
International
Conference of Fixed Point Theory and Applications, Valencia (Spain),
July 13-19, 2003
12th. International
Congress of Logic Methodology and Philosophy of Science, Oviedo
(Spain), August 7-13, 2003
Symposium
on `Unusual
Effectiveness of Logic in Computer Science', Oviedo 2003 (as part of
LMPS)
Fall school of
the Logic seminar of the Mathematical Institute of the
Academy of Sciences of the Czech Republic, Pec p. Snezkou,
Sept. 14-20,
2003.
Workshop
on Proof Theory and Algorithms, Edinburgh, March
23-29, 2003
2002 Computability on the Continuuum Seminar, Kyoto, December 14-16, 2002
CSL'02: Annual Conference
of the European Association for Computer Science Logic, Edinburgh,
September 22-25, 2002
FLoC'02: The 2002 Federated Logic Conference,
Copenhagen, Denmark, July 20 -- August 1, 2002
As part of FLoC'02:
Seventeenth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS
2002), July 22-25, 2002 Copenhagen.
Bounded
Systems and Computational Complexity, Lisbon, June 28-29, 2002.
Meeting of
the American Mathematical Society, Columbus (Ohio), September 21-23,
2001
EEF Summer School
on Logical Methods, Aarhus, Denmark, June 25-July 6, 2001
International Conference
MATHEMATICAL LOGIC, ALGEBRA AND SET THEORY (dedicated to the
100 anniversary of P.S. Novikov), Moscow, August 27-31, 2001
Fourth Workshop on Computability and Complexity in Analysis, September
17-19, 2000, Swansea, Wales
Series of lectures
on Constructive Mathematics by D.S. Bridges, Roskilde and Aarhus,
Aug 30- Sep 1
Summer School on
"Philosophy of Mathematics", University of Roskilde, June 19-32, 2000,
Roskilde
Memorial
Colloquium for Professor Kurt Schuette and Workshop `Proof and Computation'
(November 5-6, 1999)
First St. Petersburg Days
of Logic and Computability (May 26-29, 1999)
Reflections: A Symposium Honoring Solomon Feferman on his 70th Birthday
(December 11-13, 1998, Stanford University)
BRICS THEME '98: Proofs and Complexity
BRICS
Workshop: Proof Theory and Complexity (August 3-7, 1998)