POLYNOMIAL AND FUNCTIONAL INTERPRETATIONS: CONSTRUCTIVE FOUNDATIONS FOR NON-STANDARD ARITHMETIC

standard Methods. Gödel’s Dialectica interpretation (see [3]) has inspired many workers in the field of proof mining of theorems in classical analysis. Kohlenbach, Fer-reira and Oliva in particular have made use of the functional interpretation to obtain constructive or feasible versions of important theorems in set the-ory or functional analysis. Gödel’s motivation was intuitionistic in extending the finitist point of view by a functional interpretation over all finite types. It is also the case for the Curry-Howard isomorphism between formulas and types (or sets). The polynomial translation (see [2]) of the functional interpretation is a more radical enterprise and attempts to define an isomor-phism between formulas and polynomials for a non-standard arithmetic, the Fermat-Kronecker theory of forms (or homogeneous polynomials) with the constructive principle of infinite descent substituting for Peano’s induction postulate for standard arithmetic. Neither bounded arithmetic (see [1]) for subsystems of Peano’s arithmetic, nor predicative arithmetic (see [4]) fo