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!]


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

| cite | improve this answer | |
  • $\begingroup$ Excellent example, Ali. Another similar example would just be the theory TA of true arithmetic. This is a commonly considered theory, but of course is not computably or even arithmetically axiomatizable. I would encourage Peter to accept your answer instead of mine...(or wait for even more examples!) $\endgroup$ – Joel David Hamkins Jun 30 '12 at 19:28
  • $\begingroup$ A lovely example, of course! But what exactly it is an example of? $T_{ZFC}$ is, as you say, a natural r.e. set of sentences of great interest. But it isn't, as presented, a recursively axiomatized theory in the sense in my question -- taking those sentences as the axioms, the property-of-numbering-an-axiom (i.e. of numbering an arithmetical consequence on ZFC) isn't recursive. And the nice reaxiomatizations are primitively recursively axiomatized, no? So the question remains doesn't it? Are there natural cases of decidable axiomatized theories, where the decision requires unbounded search? $\endgroup$ – Peter Smith Jul 3 '12 at 18:24
  • $\begingroup$ [Sorry for the seemingly unappreciative terseness, due to the constraints of the comment box!] $\endgroup$ – Peter Smith Jul 3 '12 at 18:25
  • $\begingroup$ Well, I agree, and it's back to the drawing board for both of us! At the same time, one might object that the question has little mathematics at stake, but rather only the interpretation of what counts as sufficiently "natural". $\endgroup$ – Joel David Hamkins Jul 3 '12 at 19:13
  • $\begingroup$ What we gave were examples of theories whose natural axiomatization is c.e. rather than decidable. But you want an analogous example separating decidable from primitive recursive... $\endgroup$ – Joel David Hamkins Jul 3 '12 at 19:55

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.

| cite | improve this answer | |
  • $\begingroup$ My comment, on reflection, is the same as for Ali Enayat's lovely case. Here too we have an r.e. set of sentences, but not recursively decidable as presented, so not a recursively axiomatized theory in the (I hope non-deviant) sense I was using. No? $\endgroup$ – Peter Smith Jul 3 '12 at 18:31
  • $\begingroup$ JDH: Since Lindenbaum algebras define $\forall$ as infinite conjunctions and $\exists$ as infinite disjunctions, what happens to the undecidable theory $T$ in question when such infinite conjunctions and disjunctions are removed and only finite conjunctions and disjunctions remain (bounded quantification)? If I understand correctly, all terms in the conjunctions and disjunctions are variable-free. Does this make this fragment of $T$ 'contentual' ('finitary' in Hilbert's terminology) and is this fragment always decidable? $\endgroup$ – Thomas Benjamin Dec 8 '15 at 11:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.