**Here is another proposal. In this edition, the PS has been completely changed**

Let $T_{ZFC}$ = arithmetical truths that $ZFC$ "knows about", i.e., the set of arithmetic sentences $\phi$ such that $ZFC$ proves $\phi^\omega$, where $\phi^\omega$ is the set-theoretical statement that expresses "$\phi$ holds in the von Neumann interpretation".

$T_{ZFC}$ is an example of a natural r.e. theory whose overt axiomatization is not primitive recursive. Note that $T_{ZFC}$ is much stronger than $PA$, since includes all kinds of statements that are left undecided by $PA$, such as $Con(PA)$, $Con(PA + Con(PA)$, etc.

Moreover, one could argue that this theory is in some sense more natural than $PA$ since it is, implicitly, what mathematicians are really interested in.

Three notes:

There are axiomatizations of $T_{ZFC}$ that do not use the Craig trick; see this FOM posting for more information.

As observed by Kreisel, $T_{ZF}$ = $T_{ZFC + GCH}$ (the argument uses Gödel's constructible universe and absoluteness considerations).

In light of Harvey Friedman's programme of unearthing the deep role of large cardinals in our knowledge of the finite realm, one can also consider natural variants $T_{ZFC^{+}}$, where $ZFC^{+}$ is the result of augmenting $ZFC$ with appropriate large cardinals.

**P.S.** Since the original question stipulated that the theory, when naturally presented, be *recursive*, I offer the following (thanks to Emil Jeřábek and Joel Hamkins for helping to improve this suggestion).

Let $f_G$ be the Goodstein function, i.e., $f_G(m)=n$ iff the length of the Goodstein sequence starting at $m$ is $n$. Note that $f_G$ is recursive, but not primitive recursive. Then perhaps the *equational* theory of $(\Bbb{N}, 0, 1, +, f_G)$ is recursive but not primitive recursive.

**Perhaps even the full theory of $(\Bbb{N}, 0, 1, +, f_G)$ is decidable (i.e., maybe Presburger arithmetic augmented with the Goodstein sequence is a decidable theory)**.