Functional interpretations of feasibly constructive arithmetic

DOI10.1016/0168-0072(93)90044-EzbMath0780.03026MaRDI QIDQ685962

Alasdair Urquhart, Stephen A. Cook

Publication date: 13 October 1993

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

zbMATH Keywords

conservative extensionfree-variable calculiprovably recursive functionspolynomially bounded version of Gödel's primitive recursive functionalsrealizability Dialectica interpretation

Mathematics Subject Classification ID

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

Related Items (42)

A feasible theory of truth over combinatory algebra ⋮ Semantics vs syntax vs computations: Machine models for type-2 polynomial-time bounded functionals ⋮ The basic feasible functionals in computable analysis ⋮ Game semantics approach to higher-order complexity ⋮ A tight relationship between generic oracles and type-2 complexity theory ⋮ Bounded functional interpretation and feasible analysis ⋮ Preservation theorems for bounded formulas ⋮ On parallel hierarchies and \(R_k^i\) ⋮ Graded multicategories of polynomial-time realizers ⋮ On feasible numbers ⋮ Computation models and function algebras ⋮ Expressing computational complexity in constructive type theory ⋮ Type 2 polynomial hierarchies ⋮ A second-order system for polytime reasoning based on Grädel's theorem. ⋮ Interpreting classical theories in constructive ones ⋮ Theories with self-application and computational complexity. ⋮ Polynomial time operations in explicit mathematics ⋮ TWO (OR THREE) NOTIONS OF FINITISM ⋮ 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000 ⋮ Type-two polynomial-time and restricted lookahead ⋮ An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras ⋮ Polynomial-time Martin-Löf type theory ⋮ Provably recursive functions of constructive and relatively constructive theories ⋮ Realizability models and implicit complexity ⋮ Ramified Corecurrence and Logspace ⋮ Logics for reasoning about cryptographic constructions ⋮ A proof-theoretic characterization of the basic feasible functionals ⋮ A complexity analysis of functional interpretations ⋮ 2006 Annual Meeting of the Association for Symbolic Logic ⋮ 2003 Annual Meeting of the Association for Symbolic Logic ⋮ A semantic proof of polytime soundness of light affine logic ⋮ Unnamed Item ⋮ CONSISTENCY PROOF OF A FRAGMENT OF PV WITH SUBSTITUTION IN BOUNDED ARITHMETIC ⋮ Two algorithms in search of a type-system ⋮ Proof Complexity of Non-classical Logics ⋮ Elementary explicit types and polynomial time operations ⋮ On the computational complexity of Longley's \(H\) functional ⋮ Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II ⋮ Feasible functionals and intersection of ramified types ⋮ Saturated models of universal theories ⋮ A Logical Autobiography ⋮ Implicit computation complexity in higher-order programming languages

Cites Work

• A feasibly constructive lower bound for resolution proofs
• The intractability of resolution
• Proof theory. 2nd ed
• The typed lambda-calculus is not elementary recursive
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Syntactic translations and provably recursive functions
• Provably total functions of intuitionistic bounded arithmetic
• The relative efficiency of propositional proof systems
• Intensional interpretations of functionals of finite type I
• Monadic Elementary Formal Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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