 (b) Theories of higher type functionals comprise Gödel’s T and Spector’s extension of T via functionals defined by bar recursion. The basic idea goes back to Gödel’s 1938 lecture at Zilsel’s (Gödel 1995: 94). It was inspired by Hilbert’s 1926 Über das Unendliche, which considered a hierarchy of functionals over the natural numbers, not only of finite but also of transfinite type.