In this paper we introduce applicative theories which characterize the polynomial hierarchy of time and its levels. These theories are based on a characterization of the functions in the polynomial hierarchy using monotonicity constraints, introduced by Ben-Amram, Loff, and Oitavem.

We give recursion-theoretic characterizations of the counting class \(\textsf {\#P} \), the class of those functions which count the number of accepting computations of non-deterministic Turing machines working in polynomial time. Moreover, we characterize in a recursion-theoretic manner all the levels \(\{\textsf {\#P} _k\}_{k\in {\mathbb {N}}}\) of the counting hierarchy of functions \(\textsf {FCH} \), which result from allowing queries to functions of the previous level, and \(\textsf {FCH} \) itself as a whole. This is done in the style of (...) Bellantoni and Cook’s safe recursion, and it places \(\textsf {\#P} \) in the context of implicit computational complexity. Namely, it relates \(\textsf {\#P} \) with the implicit characterizations of \(\textsf {FPTIME} \) (Bellantoni and Cook, Comput Complex 2:97–110, 1992) and \(\textsf {FPSPACE} \) (Oitavem, Math Log Q 54(3):317–323, 2008), by exploiting the features of the tree-recursion scheme of \(\textsf {FPSPACE} \). (shrink)

In Spescha and Strahm [15], a system of explicit mathematics in the style of Feferman [6] and [7] is introduced, and in Spescha and Strahm [16] the addition of the join principle to is studied. Changing to intuitionistic logic, it could be shown that the provably terminating operations of are the polytime functions on binary words. However, although strongly conjectured, it remained open whether the same holds true for the corresponding theory with classical logic. This note supplements a proof of (...) this conjecture. (shrink)

This paper studies systems of explicit mathematics as introduced by Feferman [9, 11]. In particular, we propose weak explicit type systems with a restricted form of elementary comprehension whose provably terminating operations coincide with the functions on binary words that are computable in polynomial time. The systems considered are natural extensions of the first-order applicative theories introduced in Strahm [19, 20].

This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the two subsystems of (...) second order arithmetic, Π10-CA and Π11-CA, respectively. (shrink)