# 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.