Ulrich Kohlenbach: Gödel's functional interpretation and its use in
Syntactic translations of certain theories T1 into other
theories T2, so-called proof interpretations, play and important role
in Gödel's work. Examples are his negative translation of classical
arithmetic into intuitionistic arithmetic, his translation of
intuitionistic logic into modal logic S4 and - most prominently - his
functional ("Dialectica") interpretation of intuitionistic
(and -- via negative translation -- also classical) arithmetic into a
quantifier-free calculus of primitive recursive functionals T.
Whereas Gödel's main motivation was to address foundational issues
(e.g. relative consistency results), proof interpretations have
subsequently been used to extract new information from given proofs in
various areas of mathematics. In particular, in recent years versions
of functional interpretation have been used as a powerful tool to obtain new
effective bounds as well as qualitatively new uniformity results from
proofs in numerical analysis, functional analysis and hyperbolic geometry.
We will give a survey of this development.