Intensional interpretations of functionals of finite type I

Abstract

T₀ will denote Gödel's theory T[3] of functionals of finite type (f.t.) with intuitionistic quantification over each f.t. added. T₁ will denote T₀ 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₀ in intuitionistic arithmetic U₀ and of T₁ in intuitionistic analysis is U₁. U₁ is U₀ with quantification over functionals of type (0,0) and the axiom schemata AC₀₀ and of bar induction.