Description of Ulrich Kohlebach's lectures at the
Fall school (Sept.'03)

Proof mining

`Proof mining' is the process of logically analyzing proofs with the aim of obtaining new information that was not visible beforehand (see [4] for a very short essay on proof mining). The new information can be a program, an effective bound but also new qualitative information on the independence of a solution from certain parameters among others. The logical techniques used are specially adapted so-called proof interpretations which interpret given proofs in a high level language, typically based on functionals of higher types. Proof mining has its origin in ideas of G. Kreisel (`unwinding of proofs') going back to the 50's, but has been pursued more systematically only in recent years.

In this course we will discuss, by means of examples from various parts of mathematics, some of the main techniques used in proof mining such as Herbrand analysis, no-counterexample interpretation, realizability and functional interpretations. We prove general metatheorems which show how these techniques apply to large classes of proofs based on classical logic and non-computational principles such as the attainment of the infimum of continuous functions f:[0,1] -> R and forms of sequential compactness.

We discuss recent case studies in approximation theory and fixed point theory where this logic-based approach has provided quite a number of new results.

The course will be based on (parts of) the lecture notes [1] augmented by some of the material from the survey paper [2] and -- if time permits -- some of the very recent developments reported in [3].

Literature:

[1] Proof Interpretations on the Computational Content of Proofs. Lecture Notes, May 2003, ii+165pp., available at: http://www.brics.dk/~kohlenb/newcourse.ps
[2] (With Paulo Oliva) Proof mining: a systematic way of analyzing proofs in mathematics. To appear in: Proc. Steklov Math. Institute. Available at: http://www.brics.dk/~kohlenb/novikov.ps
[3] Some logical metatheorems with applications in functional analysis. BRICS Research Report RS-03-21, 55pp. (2003), available at http://www.brics.dk/RS/03/21/.
[4] Applied foundations: proof mining in analysis. Newsletter of the Danish Mathematical Society, vol. 13, pp. 7-9 (2002). Available at: http://www.brics.dk/~kohlenb/matilde.ps