Daimiposten er internt meddelelsesorgan for studerende og medarbejdere ved Datalogisk Institut, Aarhus Universitet. Indlæggene er ikke udtryk for afdelingens officielle holdning.
Ulrich Kohlenbach has held a research position at Brics since 1997 and since 2000 he has been a part of the permanent faculty at Daimi. Last semester he taught the course ”Models and Logic” together with Mogens Nielsen and this semester he is teaching the course ”Logic and Proof Interpretations”.
I first became interested in logic - the area I am still working in - during my late years in high school where I happened to learn about Gödel's results and the so-called "foundational crisis" in mathematics around 1900 by pure accident. Our mathematics teacher had the idea that everybody should write some report on a particular period in the history of mathematics. He had designed 20 topics ranging from ancient mathematics to modern times. Unfortunately, I was ill the day the topics were chosen by the students. Of course, everybody had tried to get an easy assignment assuming that the older the period in history to be covered the easier the mathematics to be dealt with. So when I came back the next day it turned out that the only topic left was no. 20 on Cantor, Hilbert and Gödel. After I had overcome some initial shock, I started to work on this and for the first time I heard about things like proof theory, undecidability, incompleteness and the like. After my graduation from high school I was determined to become a logician and enrolled at the Goethe University in Frankfurt am Main for mathematics and philosophy. The first years were slightly frustrating as I didn't understand (at that time!) why I should compute all these integrals and determinants instead of learning more about logic but from the third year on I was free to attend the logic seminar run by Horst Luckhardt on proof theory and computability theory. I also went to Claus-Peter Schnorr's complexity theory seminar.
Whereas in the beginning, my interests in logic were centered around set theory and model theory, I soon got interested in recursion theory and proof theory as well. In 1986, I got my masters degree ("Diplom") in mathematics with a thesis on extensions of the Kreisel-Kleene continuous functionals to certain infinite types which had been developed in a PhD thesis by Wolfgang Friedrich in Frankfurt some years before in connection with proof theoretic questions. After this I was ready to write a PhD thesis in the area of proof theory. However, in order to do so I had to get either a fellowship or - financially more rewarding - an assistant position. In the German university system assistant positions are associated to chairs. Since the only logician in the department, my supervisor Luckhardt, was an associate (C3) professor but not a full (C4) professor, there was no such position in logic. Fortunately, Jürgen Bliedtner, who held the chair for "Real analysis and Potential theory" was willing to offer me one of his assistant positions on the condition that I had to do some teaching and supervision of students in his area. Of course, I happily agreed and had all the freedom to pursue my own research interests in logic.
In addition to the impact that Horst Luckhardt had as my supervisor, I was under strong influence of the writings of Georg Kreisel and Anne Troelstra. Kreisel had since the 50's proposed the "program" of using proof theoretic methods to extract new computational data from prima facie ineffective proofs e.g. in number theory, combinatorics and other areas. Kreisel called this activity "unwinding of proofs" and asked for a reorientation of traditional proof theory which had been focused on foundational issues related to the so-called Hilbert program. In order to effectivize non-constructive proofs, the study of the relation between such proofs and proofs based on constructive (intuitionistic) principles was of obvious relevance. It was from this applied perspective that I became interested in the study of intuitionistic theories, a topic that Anne Troelstra has contributed to profoundly for many decades. In my thesis I developed a combination of various proof theoretic techniques based on Gödel's functional (so-called "Dialectica")-interpretation and certain recursion theoretic constructions due to W.A. Howard. I showed that this approach allowed to "unwind" proofs in large fragments of classical type theory and, in particular, showed how to extract algorithms from unique existence proofs in analysis. Finally, I applied this to concrete proofs in the area of Chebycheff approximation theory.
In 1990 I received my PhD degree in mathematics. The next year I spent publishing the main results of my thesis in a series of papers. More importantly, I got married to my wife Gabriele the same year.
As my assistant position was about to terminate, I was in need of a new position in order to work on the next "thesis" the so-called "Habilitationsschrift", a peculiar German requirement for a career as a university teacher. This time the chair of "Analytic Number Theory", Wolfgang Schwarz helped me out and he was as supportive of my research as Bliedtner had been before. In 1995, my Habilitationsschrift "Real growth in standard parts of analysis" which deals with the extractability of polynomial bounds from interesting fragments of analysis was accepted by the department of mathematics and I was awarded the title "Privatdozent".
The next year, my wife and I moved to the US where I took up a visiting position at the Mathematics Department of the University of Michigan in Ann Arbor. Despite an exhausting teaching load (so-called "Michigan reform calculus") this was an exciting year having as eminent logicians as Andreas Blass, Peter Hinman, Yuri Gurevich and Kevin Compton as colleagues.
Already shortly before my departure to Michigan, Martin Hyland had suggested to me that Brics would be an ideal place to pursue my research interests and urged me to apply there. In the winter of 1996, Brics offered me a research position. After considering for a while the pros and cons of going back to Europe we finally decided to move to Århus which has turned out to be one of the best decisions I ever made. Already during my first year in Århus, Glynn Winskel offered me the possibility to organize (together with my colleagues Søren Riis and Carsten Butz) a special year in logic for 1998 with an international workshop as one of the main activities. This workshop "Proof Theory and Complexity" took place in summer 1998 with as many as 27 invited speakers and proceedings published subsequently in "Annals of Pure and Applied Logic".
In recent years, one of my research agendas has been to establish the use of proof theoretic techniques in the area of computability and complexity in analysis. During the last decade an increasing amount of research on computability on continuous data types and exact real number computation has emerged in computer science accompanied with a corresponding complexity theory. Of course, traditional numerical analysis has already accumulated a large body of relevant results and algorithmic approaches which, however, often cannot be used directly here as they involve non-computational (and therefore non-implementable) steps and concepts. Proof theoretic techniques could be successfully applied to transform ineffective proofs in numerical analysis (and other areas of computational mathematics) into computationally meaningful procedures. A couple of years ago, Dana Scott suggested to me to call this approach "proof mining", a suggestion which I meanwhile took up.
Much of my free time I am spending listening to Jazz or 20th century classical music (in particular: Igor Strawinsky). A recent interest of mine is the history of early Harlem stride piano.
When in summer 1999 our daughter Katharina was born at Skejby Sygehus we had to think about settling down somewhere. So I was very glad when in August 2000 I got the offer to join the permanent faculty of Daimi. We then looked for a convenient place to live for the years to come and finally bought a house in Løgten where we moved to early this year.
Ever since I first came to Brics, the place keeps amazing me by the number of exciting events going on, the support from colleagues like Glynn Winskel, Mogens Nielsen and Erik Meineche Schmidt, the quality of the PhD students, the efficiency of the secretarial staff and many other things. Whenever I am abroad, I am asked for more information about this miraculous place called Brics that people have already heard so many unbelievable stories about, most recently just a week ago at a meeting of the American Mathematical Society in Columbus, Ohio.
Sidste ændring: 6. november 2001
Daimiposten