Intuitionistic formal theories with realizability in subrecursive classes
type: Item
instance of: scholarly article
title: Intuitionistic formal theories with realizability in subrecursive classes
zbMATH Open document ID: 0895.03017
DOI: 10.1016/S0168-0072(97)00002-X
published in: Annals of Pure and Applied Logic
publication date: 1998-09-14T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03D20
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q15
zbMATH DE Number: 1109912
zbMATH Keywords: computable function
zbMATH Keywords: intuitionistic theories
zbMATH Keywords: relationships between formal theories and complexity classes
zbMATH Keywords: polynomial time
zbMATH Keywords: strings over finite alphabets
zbMATH Keywords: induction
zbMATH Keywords: Turing machine
zbMATH Keywords: Kalmar elementary functions
zbMATH Keywords: Grzegorczyk class
author: Anatoly Petrivich Beltiukov
reviewed by: Joseph S. Ullian
MaRDI profile type: Publication
cites work: On the computational power of pushdown automata
cites work: Q3800030
cites work: Q5670174
cites work: Q5629622
cites work: Q5812175
Recommended article: General recursive realizability and intuitionistic logic
Recommended article: Realizability and intuitionistic logic
Recommended article: A Generalized Realizability and Intuitionistic Logic
Recommended article: Absolute \(L\)-realizability and intuitionistic logic
Recommended article: Subformula linking for intuitionistic logic with application to type theory
Recommended article: Complexity of subclasses of the intuitionistic propositional calculus
Recommended article: Q3075213
Recommended article: Realisability for infinitary intuitionistic set theory
Recommended article: Realization of Intuitionistic Logic by Proof Polynomials
Recommended article: Extensional realizability for intuitionistic set theory
description: scientific article; zbMATH DE number 1109912