Professor of MathematicsResearch Group Logic
I obtained my PhD (Dr.phil.nat.) in 1990 from the
Department of Mathematics
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 2013):
Other professional activities:
Association for Symbolic Logic (Vice President)
Wissenschaftliche Gesellschaft an der J.W.Goethe-Universität zu Frankfurt am Main (Corresponding Member)
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.
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.
Fluctuations, effective learnability and metastability in analysis (with Pavol Safarik). Submitted.
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 to appear in: Numer. Funct. Anal. and Optimiz.
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).
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.
Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics. Mathematical Research Institute Oberwolfach, November 16-22, 2014.
Universality and Homogeneity. Hausdorff Trimester Program September 2 - December 20, 2013, Bonn.
Proof Theory in Lisbon, July 19, 2013.
Workshop CSPM Computer Science, Philosophy, Mathematics, Institut de Mathematiques de Toulouse, April 26, 2013.
Types 2013, Toulouse, April 23-26, 2013.
3rd Workshop on Proof Theory and Rewriting. Kanazawa (Japan), March 4-8, 2013.
International Workshop on Fixed Point Theory and Applications, October 11-13, 2012, Istanbul, Turkey.
Third MALOA Training Workshop, University of Oxford, Mathematical Institute, Aug.26 - Sep.1, 2012.
10th International Conference of Fixed Point Theory and its Applications, July 9-15, 2012, Cluj-Napoca, Romania.
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.
Oberwolfach Workshop on Computability Theory.Mathematical Research Institute Oberwolfach, February 5-11, 2012.
Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics. Mathematical Research Institute Oberwolfach, November 6-12, 2011.
Ramsey Theory in Logic, Combinatorics and Complexity. Bertinoro (Italy), May 22-27, 2011.
New Trends in Logic. Conference honoring the Winners of the Kurt Gödel Research Prize Fellowships 2008 and 2011. Austrian Academy of Sciences, Vienna, April 28-29, 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.
CL&C'10, Third International Workshop on Classical Logic and Computation. Brno, Czech Republic, August 21-22, 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.
Symposium for Mogens Nielsen's 60th birthday: an Aarhus celebration, Aarhus University, Denmark, October 3-4, 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.
Summer School and Conference Mathematics, Algorithms and Proofs (MAP), August 11-29, 2008, Abdus Salam International Centre for Theoretical Physics, Trieste.
WoLLIC'2008 15th Workshop on Logic, Language, Information and Computation July 1st to 4th, 2008, Edinburgh, Scotland.
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.
Joint Workshop DOMAINS VIII and Computability over Continuous Data Types, Novosibirsk , September 11-15, 2007, Russia.
ASL Logic Colloquium 2007, Worclaw. July 14-19, 2007.
Trimester on methods of proof theory in mathematics. Max Planck Institute for Mathematics, Bonn, March-June 2007.
Joint Mathematics Meeting, AMS-ASL Special Session on Logical Methods in Computational Mathematics, January 5-7, 2007, New Orleans, USA.
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.
WoLLIC'2006, 13th Workshop on Logic, Language, Information and Computation July 18-21, 2006, Stanford, California, USA.
Horizons of Truth: Logics, Foundations of Mathematics, and the Quest for Understanding the Nature of Knowledge. Gödel Centenary 2006. An International Symposium Celebrating the 100th Birthday of Kurt Gödel, Vienna, 27.-29. April 2006.
MAP 2006, Castro Urdiales (Spain), 9.1.2006-13.1.2006.
CSL'05, Oxford, UK, 22-25 August 2005.
7th International Conference on Fixed Point Theory and Applications. Guanajuato (Mexico), July 17-23, 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.
COLLOQUIUM LOGICUM 2004, Biannual Meeting of the German Society for Mathematical Logic (DVMLG), September 17 - 19, 2004, Heidelberg (Germany).
Jahrestagung der Deutschen Mathematiker- Vereinigung, Heidelberg, Sept. 12-17, 2004
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)