Samuel R. Buss.
    "The Polynomial Hierarchy and Intuitionistic Bounded Arithmetic."  
    In  Structure in Complexity, Lecture Notes in Computer Science #223, Springer Verlag, 1986, pp. 77-103.

    Download article:  searchable PDF or plain PDF

Abstract  Intuitionistic theories IS2i of Bounded Arithmetic are introduced and it is shown that the definable functions of IS2i are precisely the FPip functions of the polynomial time 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 FPip-realizability which is inspired by the recursive realizability of S.C. Kleene and D. Nelson.  It also involves the polynomial hierarchy functionals of finite type which are introduced in this paper.

Back to Sam Buss's publications page.