Can A Decidable Theory Have Nonrecursive Models? Tennenbaum's theorem proves neither addition nor multiplication can be recursive in any countable non-standard model of arithmetic. Tennenbaum's proof applies to theories much weaker than PA.
Tennenbaum's proof is a proof by contradiction. If addition or multiplication is recursive in a non-standard model then it is possible to use a form of induction called overspill to prove recursively inseparable sets can be encoded as non-standard natural numbers. Overspill says if $f(n)$ is true for all standard natural numbers then $f(\alpha)$ is true for some non-standard natural number, $\alpha$. An example of a recursively inseparable set would be the set of standard natural numbers encoding a Turing machine that halts on blank input.
Let $\mathbb{N}^*$ be a countable non-standard model of PA and let $\mathbb{Z}^*$ be the integers extended from $\mathbb{N}^*$. A "non-standard finite field" would be a ring $\mathbb{Z}^* /p^* \mathbb{Z}^*$ where $p^*$ is a non-standard prime number larger than any standard natural number. Non-standard finite fields admit almost quantifier elimination. This means non-standard finite fields must be "almost recursive".
It can be shown Tennenbaum's theorem applies to non-standard finite fields. If there exists a recursive non-standard finite field then Tennenbaum's proof by contradiction becomes a proof of contradiction. It means we can recursively determine if a standard natural number, $n$, encodes a halting TM by checking if $n$ is a root of one of a finite set of polynomials.
Is "almost quantifier elimination" enough to prove a non-standard finite field is recursive? Even if it is not, this seems to be a big problem. James Ax proved the theory of finite fields is decidable. Can there be a recursive mapping from a recursive model of finite fields to a non-recursive model or could we once again derive a contradiction?
 A: I think there is a confusion here between two notions of "recursive".
Tennenabum's theorem deals with recursive structures. Let us assume for simplicity that that the language contains a single unary relation symbol $R$. Then a recursive  structure $\mathcal M$ for this language has underlying set $\mathbb N$ and with $R^{\mathcal M}$ a recursive subset of $\mathbb N$. The formal definition is more complicated than that, but intuitively, in a recursive structure there is a reasonable coding of the elements and we can reasonably do computations. For example, the usual natural numbers, the ring of polynomials over the rationals, or the set $\mathbb N$ with a predicate for the primes are all recursive structures. By contrast, if we equip $\mathbb N$ with a single unary relation symbol for some undecidable set, then this structure is not recursive.
Tennenbaum's theorem says that there is no nonstandard recursive model of the theory of the natural numbers. So while we have computer programs that add and multiply integers, there can be no computer program which can perform manipulations on nonstandard integers. 
Almost quantifier elimination deals with theories, not structures. If a theory has quantifier elimination, or something close, then we might expect that it is "easy" or closer to being decidable. But very complicated structures can have very simple theories. Take the example from before. The theory of an infinite set partitioned into two infinite sets is very simple and easy to understand. It is certainly decidable! But the structure $\mathbb N$ with a predicate for the set of those numbers coding a Turing machine which halts is complicated from this point of view, even though its theory is decidable.
A: Several answers to this question can be seen on MathOverflow at https://mathoverflow.net/questions/157624/can-a-decidable-theory-have-non-recursive-models/ . In particular, the answer to the title question is "yes". 
