Article:
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.