Ulrich Kohlenbach: Gödel's functional interpretation and its use in current mathematics
AbstractSyntactic 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.