Intensional interpretations of functionals of finite type I
W. W. Tait · Journal of Symbolic Logic · 1967
T 0 will denote Gödel's theory T[3] of functionals of finite type (f.t.) with intuitionistic quantification over each f.t. added. T 1 will denote T 0 together with definition by bar recursion of type o, the axiom schema of bar induction, and the schema of choice. Precise descriptions of these systems are given below in §4. The main results of this paper are interpretations of T 0 in intuitionistic arithmetic U 0 and of T 1 in intuitionistic analysis is U 1 . U 1 is U 0 with quantification over functionals of type (0,0) and the axiom schemata AC 00 and of bar induction.