A polynomially bounded recursive realizability, in which the recursive functions used in Kleene's realizability are restricted to polynomially bounded functions, is introduced. It is used to show that provably total functions of Ruitenburg's Basic Arithmetic are polynomially bounded (primitive) recursive functions. This sharpens our earlier result where those functions were proved to be primitive recursive. Also a polynomially bounded schema of Church's Thesis is shown to be polynomially bounded realizable. So the schema is consistent with Basic Arithmetic, whereas it is (...) inconsistent with Heyting Arithmetic. (shrink)

We study Basic Arithmetic, $$\textsf{BA}$$ introduced by Ruitenburg (Notre Dame J Formal Logic 39:18–46, 1998). $$\textsf{BA}$$ is an arithmetical theory based on basic logic which is weaker than intuitionistic logic. We show that the class of the provably total recursive functions of $$\textsf{BA}$$ is a proper sub-class of the primitive recursive functions. Three extensions of $$\textsf{BA}$$, called $$\textsf{BA}+\mathsf U$$, $$\mathsf {BA_{\mathrm c}}$$ and $$\textsf{EBA}$$ are investigated with relation to their provably total recursive functions. It is shown that the provably total (...) recursive functions of these three extensions of $$\textsf{BA}$$ are exactly the primitive recursive functions. Moreover, among other things, it is shown that the well-known MRDP theorem does not hold in $$\textsf{BA}$$, $$\textsf{BA}+\mathsf U$$, $$\mathsf {BA_{\mathrm c}}$$, but holds in $$\textsf{EBA}$$. (shrink)

We give a counterexample to the claim that every provably total function of Basic Arithmetic is a polynomially bounded primitive recursive function.