 Among the proposals for extending finitist methods put forward in his 1938 lecture at Zilsel’s, Gödel appears to have favored the route via higher type functions. Details of what came to be known as the Dialectica interpretation were not published until 1958 (Gödel 1958) but the D-interpretation itself was arrived at by 1941. Gödel’s system \({T}\) axiomatizes a class of functions that he called the primitive recursive functionals of finite type. \({T}\) is a largely equational theory whose axioms are equations involving terms for higher type functionals with just a layer of propositional logic on top of that. In this way the quantifiers, problematic for finists and irksome to intuitionists, are avoided. To explain the benefits of the D-interpretation we need to have a closer look at the syntax of \({T}\).