Maria Hämeen-Anttila

The roots of Kurt Gödel's functional interpretation in the Dialectica paper of 1958 go back to a lecture course from 1941 and a single lecture given at Yale in April 1941. Although the functional interpretation is first mentioned in 1938 in the context of the extended Hilbert Programme, the 1941 lectures mostly discuss the functional interpretation in the context of intuitionistic logic. In this article, I will examine the early development of the functional interpretation and its relationship to the 1938 ‘Zilsel’ lecture, especially the critical remarks on Gentzen's consistency proof. It is shown that Gödel's functional interpretation was decidedly influenced by Gentzen, putting into question his earlier criticism of Gentzen's proof.

In 1936, Gerhard Gentzen published a proof of consistency for Peano Arithmetic using transfinite induction up to ε0, which was considered a finitistically acceptable procedure by both Gentzen and Paul Bernays. Gentzen’s method of arithmetising ordinals and thus avoiding the Platonistic metaphysics of set theory traces back to the 1920s, when Bernays and David Hilbert used the method for an attempted proof of the Continuum Hypothesis. The idea that recursion on higher types could be used to simulate the limit-building in transfinite recursion seems to originate from Bernays. The main difficulty, which was already discovered in Gabriel Sudan’s nearly forgotten paper of 1927, was that measuring transfinite ordinals requires stronger methods than representing them. This paper presents a historical account of the idea of nominalistic ordinals in the context of the Hilbert Programme as well as Gentzen and Bernays’ finitary interpretation of transfinite induction.