The polynomial hierarchy and intuitionistic bounded arithmetic

Abstract

Intuitionistic theories IS2i of Bounded Arithmetic are introduced and it is shown that the definable functions of IS2i are precisely the □ip functions of the polynomial hierarchy. This is an extension of earlier work on the classical Bounded Arithmetic and was first conjectured by S. Cook. In contrast to the classical theories of Bounded Arithmetic where Σib-definable functions are of interest, our results for intuitionistic theories concern all the definable functions. The method of proof uses □ip-realizability which is inspired by the recursive realizability of S.C. Kleene [3] and D. Nelson [5]. It also involves polynomial hierarchy functionals of finite type which are introduced in this paper.