Polynomially bounded recursive realizability

DOI10.1305/NDJFL/1134397659MaRDI QIDQ817959zbMATH OpenOpenAlexWikidataFDO

Authors Saeed Salehi

Publication date 23 March 2006

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1305/ndjfl/1134397659

zbMATH Keywords

basic arithmeticbasic logicpolynomially bounded recursive functionprimitive recursive functionProvably total functionrealizability

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50)

Review text

The strength of a theory can be measured by characterizing its provably total functions. Those of Heyting Arithmetic (HA), for example, are known to be specified as recursive according to Kleene's recursive realizability. The author proved in his earlier work that provably total functions of Basic Arithmetic (BA) are primitive recursive, where BA was introduced by Ruitenburg in a similar way as HA by featuring his Basic Logic in place of intuitionistic logic. In this paper the author introduces a polynomially bounded recursive realizability by restricting the recursive functions used in Kleene's realizability to the polynomially bounded ones, and proves that the earlier result is sharpened by them, where the polynomially bounded ones are primitive recursive. It is also shown that a polynomially bounded schema of Church's Thesis is realizable in the polynomially bounded sense. The schema, therefore, is consistent with BA, whereas it is inconsistent with HA.

Recommendations

• Provably total functions of Basic Arithmetic
• Functional interpretations of feasibly constructive arithmetic
• scientific article; zbMATH DE number 440477
• Minimal readability of intuitionistic arithmetic and elementary analysis
• Strictly primitive recursive realizability, I

Cites work

• Arithmetic complexity of the predicate logics of certain complete arithmetic theories
• Basic predicate calculus
• Constructivism in mathematics. An introduction. Volume I
• Elementary interpretations of negationless arithmetic
• Elementary realizability
• How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q
• scientific article; zbMATH DE number 65747 (Why is no real title available?)
• scientific article; zbMATH DE number 1144041 (Why is no real title available?)
• scientific article; zbMATH DE number 2019914 (Why is no real title available?)
• Minimal readability of intuitionistic arithmetic and elementary analysis
• On the scheme of induction for bounded arithmetic formulas
• Provably total functions of Basic Arithmetic
• Recursively enumerable sets and degrees. A study of computable functions and computably generated sets. Translated from the English. Translation edited and with a preface by M. M. Arslanov.
• Strictly primitive recursive realizability, I
• Strictly primitive recursive realizability. II: Completeness with respect to iterated reflection and a primitive recursive -rule

Cited in

(6)

• A strong induction scheme that leads to polynomially computable realizations
• A counterexample to polynomially bounded realizability of basic arithmetic
• Bounded theories for polyspace computability
• Provably total functions of Basic Arithmetic
• Functional interpretations of feasibly constructive arithmetic
• The provably total functions of basic arithmetic and its extensions

This page was built for publication: Polynomially bounded recursive realizability

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