Are there any natural recursively but not primitive-recursively axiomatized theories?

Question

In principle, we could have a recursively axiomatized theory for which the property numbers-an-axiom (even relative to some routine Gödel numbering scheme) is recursive but not primitive recursive. But are there any natural examples?

Of course, any such theory can be primitive-recursively reaxiomatized using Craig's trick. So we know that there can't be theories which are recursively axiomatizABLE but not primitive-recursively aziomatizABLE. But that's not the issue. The question is whether there is a theory T which when presented in a natural way requires open-ended searches to check whether a purported T-proof is indeed a proof according to that specification.

[I couldn't think of one when I wrote the first edition of my Gödel book, and I still can't as I work on the second edition. But maybe I'm just being dim/ignorant!]

Answer 1

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:

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

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

3. 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).

Answer 2

Here is one proposal.

Consider the natural theory of the Lindenbaum algebra of an undecidable theory $T$ (and natural examples of these abound). So the theory can refer to objects, which are sentences in the language of $T$, and there is an order relation axiomatized by $\varphi\leq \psi$ whenever $T\vdash\varphi\to\psi$. This is naturally a c.e. axiomatization of the theory, which can therefore be enumerated according a computable procedure, but this process does not seem to provide a primitive recursive axiomatization, except by means of the Craig's trick type reaxiomatization you mention.