In this paper we naturally define when a theory has bounded quantifier elimination, or is bounded model complete. We give several equivalent conditions for a theory to have each of these properties. These results provide simple proofs for some known results in the model theory of the bounded arithmetic theories like CPV and PV1. We use the mentioned results to obtain some independence results in the context of intuitionistic bounded arithmetic. We show that, if the intuitionistic theory of polynomial induction (...) on strict $\Pi_2^{b}$ formulas proves decidability of $\Sigma_1^b$ formulas, then P=NP. We also prove that, if the mentioned intuitionistic theory proves ${\rm LMIN}(\Sigma_{1}^{b})$ , then P=NP. (shrink)

We use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra PV ω defines exactly the PTIME-functions. As a byproduct we obtain a syntax-free generalisation of PTIME-computability to higher types. By restricting to sheaves for a suitable topology we obtain a model for intuitionistic predicate logic with ∑ 1 b -induction over PV ω and use this to re-establish that the provably total functions in this system are polynomial time computable. Finally, we (...) apply the category-theoretic approach to a new higher-order extension of Bellantoni-Cook's system BC of safe recursion. (shrink)

This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory Smath image, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1.

A notion of feasible function of finite type based on the typed lambda calculus is introduced which generalizes the familiar type 1 polynomial-time functions. An intuitionistic theory IPVω is presented for reasoning about these functions. Interpretations for IPVω are developed both in the style of Kreisel's modified realizability and Gödel's Dialectica interpretation. Applications include alternative proofs for Buss's results concerning the classical first-order system S12 and its intuitionistic counterpart IS12 as well as proofs of some of Buss's conjectures concerning IS12, (...) and a proof that IS12 cannot prove that extended Frege systems are not polynomially bounded. (shrink)

This paper defines natural hierarchies of function and relation classes □i,kc and Δi,kc, constructed from parallel complexity classes in a manner analogous to the polynomial-time hierarchy. It is easily shown that □i−1,kp □c,kc □i,kp and similarly for the Δ classes. The class □i,3c coincides with the single-valued functions in Buss et al.'s class , and analogously for other growth rates. Furthermore, the class □i,kc comprises exactly the functions Σi,kb-definable in Ski−1, and if Tki−1 is Σi,kb-conservative over Ski−1, then □i,kp is (...) completely parallelizable. All functions in □i,kc are Σi,kb-definable in Rki; this suffices to show that if the known Σi,kb conservativity between R3i and S3i−1 extends to R2i and S2i−1, then NC = NC1 relative to an oracle in PH. We prove a KPT-style witnessing theorem for Ski using constantly many rounds of □i,kc interactive computation, and thus show that if Ski ≡ Rki+1 then the bounded arithmetic hierarchy collapses, provably in Ski. (shrink)