On the Computational Content of Proofs that Use Ideal Elements

Ulrich Kohlenbach

We report on progress in the program of applied proof theory that uses tools from proof theory to extract hidden computational information from proofs of ∀∃-theorems S that use highly noneffective principles I. Reverse mathematics as pioneered by Harvey Friedman provides important guidance to single out the relevant principles I and to find the proper representation of notions needed to formalize them.

It turns out that many proofs in ordinary mathematics (as it currently exists) not really utilize the full proof-theoretic strength of I but rather use I as some regulative idea (in the sense of Hilbert) which helps to make the proof conceptually feasible while being in principle avoidable. This makes Harvey Friedman's research on showing how to insert the real strength of I into the context of combinatorial/computational meaningful statements all the more relevant.

Applied proof theory strongly relies on the interplay between systems of classical mathematics and intuitionistic mathematics with the Markov rule (which follows from Friedman's striking A-translation) being the crucial feature.

Institutional Honorary Doctorate Degree for Prof Dr Harvey M. Friedman