Return to Answer

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: 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 the equational theory of $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).

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

Here is another proposal.

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 have a natural axiomatization that is recursive, I offer the following. Let $T$ be a consistent complete first order theory in the sense that for every sentence $\phi$ that is formulated in the language of $T$, $T$ proves precisely one of {$\phi$, $\neg\phi$}.

Then the deductive closure $\overline{T}$ of $T$ is recursive, but not overtly primitive recursive.

Examples of such theories $T$ include "identity theory with precisely $n$-elements in the domain of discourse" (where $n$ is some positive integer), "identity theory with an infinite universe", "dense linear order without endpoints", "Presburger arithmetic". "real closed fields", and "algebraically closed fields", and many others.

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: 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 the equational theory of $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).

Here is another proposal.

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.

Here is another proposal.

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 have a natural axiomatization that is recursive, I offer the following. Let $T$ be a consistent complete first order theory in the sense that for every sentence $\phi$ that is formulated in the language of $T$, $T$ proves precisely one of {$\phi$, $\neg\phi$}.

Then the deductive closure $\overline{T}$ of $T$ is recursive, but not overtly primitive recursive.

Examples of such theories $T$ include "identity theory with precisely $n$-elements in the domain of discourse" (where $n$ is some positive integer), "identity theory with an infinite universe", "dense linear order without endpoints", "Presburger arithmetic". "real closed fields", and "algebraically closed fields", and many others.