Guests of the Alexander von Humboldt Foundation at TU Darmstadt

My field of research is fascinating. The best way to explain it to non-specialists in a comprehensible manner is:

My interests lie at the crossing of two research areas in mathematical logic, namely, computability theory and proof theory. These are very advanced and sophisticated areas of research, but their motivating questions, what we can(not) compute and what we can(not) prove, are among the most basic and fundamental in mathematics and science. Being at the intersection of these two research areas, I’m interested in what kind of information (such as an algorithm performing certain numerical computations) we can obtain from just analyzing the proof of a mathematical theorem. This is not at all a new question in mathematical logic, it has a long tradition, and yet remains one of the most intriguing to this day, even more so in view of the constant development of artificial intelligence.

What research questions are you currently working on?

I am investigating a number of meta-mathematical properties in the context of constructive set theory. For instance, a much desired property is the so called existence property. Most constructive theories are such that whenever they prove that something exists, they do actually provide a witness. This usually fails in a classical framework. Another question I’m interested in is how much choice one can add to constructive theories and still remain constructive.

I’ve chosen the TU Darmstadt because of…

the excellent research profile of the logic group of the Department of Mathematics at the Technische Universität Darmstadt. The group has unique research expertise in key areas of my project, ranging from proof theory to higher-type computability. My host, Prof. Ulrich Kohlenbach, a prominent figure in proof theory, is the main leader and advocate of the so called proof mining program, whose goal is to apply proof-theoretic tools to core areas of mathematics such as functional analysis in order to extract quantitative information.

My most important success in research to date is…

the reverse mathematics analysis of the size-change principle for program termination due to Lee, Jones and Ben-Amram. This work shows that the use of full Ramsey’s theorem for pairs in the orginal proof of the size-change criterion is far from optimal and pinpoints the exact strength of this criterion. Interestingly enough, this criterion is equivalent to arithmetical induction for predicates of very low complexity.