Characterising polynomial time computable functions using theories with weak set existence principles

Several authors have independently introduced second order theories whose provably total functionals are polynomial time computable functions on strings (e.g. [4], [6] and [7]), including the first author ([3], meant to be the second part of [2]). In this paper we give a detailed proof of the bi-interpretability result between such a second order theory and Buss' first order bounded arithmetic, based on an elegant definition of multiplication due to the second author.