Intuitionistic formal theories with realizability in subrecursive classes (Q1377631)

The paper studies relationships between formal theories and complexity classes, especially the class of functions computable in polynomial time. It presents a formal intuitionistic system for strings over finite alphabets whose induction schema is restricted, requiring that the induction formula have all its quantifiers bounded with regard to word length. A proof is sketched that this theory is rich enough so that for any function computable in polynomial time a Turing machine program for computing the function can be defined and shown, in the theory, to have that property. This result is acknowledged to be similar to one on Bounded Arithmetic obtained by Buss. The paper's main theorem goes in the converse direction: Given any proof in the system of a formula \(\forall x\exists yA(x,y)\), one can find an algorithm for a function \(f\), computable in polynomial time, such that \(\forall xA(x,f(x))\). Analogous results, in both directions, are claimed for other complexity classes, including the Kalmar elementary functions and the Grzegorczyk class LINSPACE. Suitable modifications of the given intuitionistic system are seen to suffice for these results.