Functional interpretations of feasibly constructive arithmetic (Q685962)

A polynomially bounded version of Gödel's primitive recursive functionals is defined here by suitable bounding of primitive recursion (which can have arguments of higher types but only numerical values). Necessary properties of these functionals are established in suitable free-variable calculi (which requires about 30 pages). This opens way to the use of realizability (Dialectica interpretation and a \(q\)-version of Kreisel's modified realizability) in a more or less familiar way to prove conservative extension results for classical systems over intuitionistic ones and for higher-order systems over equation calculi. Another consequence is a characterization of provably recursive functions: if \((\forall x)(\exists y)A(x,y)\) for sufficiently simple \(A\) is provable, then there is a polynomially computable function \(y= f(x)\) provably satisfying \(A(x,f(x))\). The latter result for \(\text{IS}^ 1_ 2\) establishes a conjecture of S. Buss.