 Spector (1962) extended Gödel’s functional interpretation, engineering an interpretation of \(\bZ_2\) into T augmented via a scheme of transfinite recursion on higher type orderings. This type of recursion, called bar recursion, is conceptually related to Brouwer’s bar induction principle. (For a definition of bar induction and a presentation of Spector’s result see  appendix C.)