kohlenb

Ulrich Kohlenbach's homepage

Ulrich Kohlenbach

Professor of Mathematics, Prodekan

Research Group Logic
Department of Mathematics
Technische Universität Darmstadt
Schlossgartenstrasse 7
D-64289 Darmstadt, Germany
kohlenbach [at] mathematik [dot] tu-darmstadt [dot] de
Tel.: (+49) 06151-16-3415 (Office)
Tel.: (+49) 06151-16-4686 (Secretary)
Fax: (+49) 06151-16-3317

I 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 (Winter term 2009/10):

Vorlesung: Analysis I. Mo 11:40-13:20 (S311/08) und Di 16:15-17:55 (S311/08), Beginn 12.10.
Vorlesung: Angewandte Beweistheorie (Applied Proof Theory, V-Modulhälfte Logik), Mi 11.40-13.20 (S215/51). Beginn: 14.10.
Literatur: U. Kohlenbach: Applied Proof Theory, Proof Interpretations and Their Use in Mathematics. Springer Monographs in Mathematics, xx+536pp., 2008.
Übung zur Vorlesung: Angewandte Beweistheorie (Applied Proof Theory), Do 16:15-17:55 (S102/36). Beginn: 15.10.

Editorial Work:

Coordinating Editor: Annals of Pure and Applied Logic
Editorial Board Member: Notre Dame Journal of Formal Logic
Editorial Board Member: Mathematical Logic Quarterly

Other professional activities:

DVMLG Deutsche Vereinigung für Mathematische Logik und für Grundlagen der Exakten Wissenschaften

Wissenschaftliche Gesellschaft an der J.W.Goethe-Universität zu Frankfurt am Main

PhD Students:

Paulo Oliva (PhD 2003, Aarhus, Thesis)
Philipp Gerhardy(PhD 2006, Aarhus, Thesis)
Branimir Lambov (PhD 2006, Aarhus,Thesis)
Eyvind Briseid (PhD 2009, TU Darmstadt,Thesis)
Jaime Gaspar
Alexander Kreuzer
Pavol Safarik

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 to appear in: Horizons of Truth: Logics, Foundations of Mathematics, and the Quest for Understanding the Nature of Knowledge. Baaz, M. et al. (eds.), Cambridge University Press, New York (anticipated 2010). 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 to appear in: Notre Dame Journal of Formal Logic.
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 to appear in: Festschrift for Grigori Mints.
On the computational content of the Bolzano-Weierstrass principle (with Pavol Safarik). Final version to appear in: Math. Logic Quaterly.
On quantitative versions of a theorem due to F.E. Browder. 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).

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 2012).

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 Computability and Complexity in Analysis Network.

Link to the MAP Mathematics, Algorithms, Proofs Network.

HOT SPOTS:

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.

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.