The provably total recursive functions and the MRDP theorem in Basic Arithmetic and its extensions

TL;DR

This paper investigates the provably total recursive functions in Basic Arithmetic and its extensions, showing their relation to primitive recursive functions and analyzing the validity of the MRDP theorem within these theories.

Contribution

It establishes the exact class of provably total functions for several extensions of Basic Arithmetic and clarifies the applicability of the MRDP theorem in these contexts.

Findings

Provably total functions of BA are a proper subset of primitive recursive functions.

Extensions BA+U, BA_c, and EBA have exactly the primitive recursive functions as provably total functions.

MRDP theorem does not hold in BA, BA+U, BA_c, but holds in EBA.

Abstract

We study Basic Arithmetic, BA introduced by W. Ruitenburg. 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 BA is a proper sub-class of the primitive recursive functions. Three extensions of BA, called BA+U, BA_c and 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 BA are exactly the primitive recursive functions. Moreover, among other things, it is shown that the well-known MRDP theorem does not hold in BA, BA+U, BA_c, but holds in EBA.