Functional interpretations of feasibly constructive arithmetic

DOI10.1016/0168-0072(93)90044-EMaRDI QIDQ685962zbMATH OpenFDO

Publication date 13 October 1993

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(93)90044-E

conservative extension free-variable calculi polynomially bounded version of Gödel's primitive recursive functionals provably recursive functions realizability Dialectica interpretation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof theory in general (including proof-theoretic semantics) (03F03) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Review text

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.

Recommendations

Cites work

Cited in

(59)

This page was built for publication: Functional interpretations of feasibly constructive arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685962)