Delineating classes of computational complexity via second order theories with weak set existence principles.

Abstract: "In this paper we characterize the well-known computational complexity classes of the Polynomial Time Hierarchy as classes of provable functions of some second order theories with weak comprehension. Our formalism is somewhat different from Leivant's, who was the first to introduce such a theory for delineating polynomial time computable functions. Besides being, in our view, foundationally advantageous,our formalism also has significant technical advantages: it enables us to characterize all the classes of the Polynomial Time Hierarchy within our theories and also to relate these theories very naturally to Buss' theories of bounded arithmetic S[superscript i/].The latter feature enables us to bypass both a complicated cut-elimination procedure or a difficult model-theoretic argument usually used tocharacterize provable functions of a theory, and a tedious proof of representability of functions from various complexity classes in the theories we consider, reducing both problems to such theorems about bounded arithmetic."