Functional interpretations of feasibly constructive arithmetic
type: Item
instance of: scholarly article
title: Functional interpretations of feasibly constructive arithmetic
zbMATH Open document ID: 0780.03026
DOI: 10.1016/0168-0072(93)90044-E
author: Alasdair Urquhart
author: Stephen Cook
published in: Annals of Pure and Applied Logic
publication date: 1993-10-13T00:00:00Z
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.
reviewed by: G. E. Mints
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 68Q15
zbMATH DE Number: 425685
zbMATH Keywords: realizability Dialectica interpretation
zbMATH Keywords: polynomially bounded version of Gödel's primitive recursive functionals
zbMATH Keywords: free-variable calculi
zbMATH Keywords: conservative extension
zbMATH Keywords: provably recursive functions
MaRDI profile type: Publication
cites work: Q5604461
cites work: Q3800030
cites work: Q3138830
cites work: Q4035302
cites work: Q3235339
cites work: Q3757904
cites work: A feasibly constructive lower bound for resolution proofs
cites work: Q4133141
cites work: Q4010352
cites work: Q4011103
cites work: Q4035304
cites work: The relative efficiency of propositional proof systems
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: The intractability of resolution
cites work: Provably total functions of intuitionistic bounded arithmetic
cites work: Q4722037
cites work: Q5812175
cites work: Propositional proof systems, the consistency of first order theories and the complexity of computations
cites work: Q3727946
cites work: Syntactic translations and provably recursive functions
cites work: Q4726219
cites work: Q5559220
cites work: Q4694254
cites work: Monadic Elementary Formal Systems
cites work: The typed lambda-calculus is not elementary recursive
cites work: Intensional interpretations of functionals of finite type I
cites work: Proof theory. 2nd ed
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
description: scientific article; zbMATH DE number 425685