Bar recursion versus polymorphism

Abstract

By constructing a counter, model we show that a certain appealing equation E has no solution in Girard's [1972] second order lambdacalculus (the so-called polymorphic, lambda calculus). The equation E = Eφ (with φ a type 3 variable) is a simple functional equation in thelkiguage of Gödel's [1958] system of higher order primitive recursive fanctiotals and has an easy solution in Spector's [1962] system of bar recursive functionals. This shows that the class of bar recursive functionals differs from the class of functionals definable in the polymorphic lambda calculus. The fact that the two calculi have different classes of definable functionals (at least of type 3), contrasts the metamathematical results from Spector [1962] and Girard [1972] which state that the two calculi have the same class of definable functions, namely the provably total recursive functions of analysis.