The provably total functions of basic arithmetic and its extensions

We study Basic Arithmetic, \(\textsf{BA}\) $\mathsf{BA}$ introduced by Ruitenburg (Notre Dame J Formal Logic 39:18–46, 1998). \(\textsf{BA}\) $\mathsf{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}\) $\mathsf{BA}$ is a proper sub-class of the primitive recursive functions. Three extensions of \(\textsf{BA}\) $\mathsf{BA}$ , called \(\textsf{BA}+\mathsf U\) $\mathsf{BA}+\mathsf{U}$ , \(\mathsf {BA_{\mathrm c}}\) ${\mathsf{BA}}_{\mathrm{c}}$ and \(\textsf{EBA}\) $\mathsf{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}\) $\mathsf{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}\) $\mathsf{BA}$ , \(\textsf{BA}+\mathsf U\) $\mathsf{BA}+\mathsf{U}$ , \(\mathsf {BA_{\mathrm c}}\) ${\mathsf{BA}}_{\mathrm{c}}$ , but holds in \(\textsf{EBA}\) $\mathsf{EBA}$ .