Can a Decidable Theory Have Non-recursive Models? Tennenbaums' 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 prove recursively inseparable sets can be encoded as non-standard natural numbers. 
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 larger than any standard natural number. It is straight forward to argue Tennenbaum's theorem applies to non-standard finite fields.
Ax has proven the theory of finite fields is decidable. Non-standard finite fields admit almost quantifier elimination. If there exists a recursive non-standard finite field then Tennenbaum's proof by contradiction becomes a proof of contradiction. 
Is "almost quantifier elimination" enough to prove there exists a recusive non-standard finite field? Can a decidable theory have non-recursive models? If so, is there an algorithm to determine if a given model is recursive?
I previously asked this question on Stack Exchange.
 A: A decidable theory can certainly have noncomputable models. For example, consider a theory with an infinite set of 0-ary relation symbols $A_1, A_2, \ldots$; no other relation, function, or constant symbols; and no axioms. This theory is decidable - it is basically just propositional logic - and its countable models are in effective correspondence with the subsets of $\mathbb{N}$ in the obvious way. 
There is not an algorithm, in general, to tell whether a subset of $\mathbb{N}$ is computable.  The class of computable subsets of $\mathbb{N}$ is $\Sigma^0_3$, strictly. 
A: As explained in Carl Mummert’s answer, there are decidable theories with nonrecursive models. To answer the first question, every decidable theory also has a recursive model, and in fact, a model with a recursive satisfaction predicate (or in other words, decidable elementary diagram). The reason is that the usual Henkin completion procedure provides a recursive construction of a complete Henkin extension $T^+$ of $T$ as long as $T$ is decidable, and then $T^+$ is essentially identical to the elementary diagram of its canonical model.
However, since your “nonstandard finite fields” are not all models of the relevant first-order theory (pseudofinite fields of characteristic $0$), but only models of a very special form (those that can be obtained as quotients of models of PA), this does not mean that there are recursive “nonstandard finite fields”. In fact, countable “nonstandard finite fields” are exactly the recursively saturated pseudofinite fields of characteristic $0$, and there are no recursive, recursively saturated pseudofinite fields, as shown by Macintyre.
I don’t see what quantifier elimination has to do with anything. Quantifier elimination for pseudofinite fields, namely that every formula is equivalent to a Boolean combination of formulas of the form $\exists y\,f(x_1,\dots,x_n,y)=0$, where $f$ is a polynomial with integer coefficients, can certainly be made effective (although its most convenient model-theoretic proofs are nonconstructive). This follows automatically from the fact that the theory of pseudofinite fields is recursively axiomatizable (actually even decidable). However, this does not imply anything about recursivity of its models. To begin with, whether a model is recursive only calls for recursivity of the basic relations and functions, not more complex formulas, so eliminating quantifiers from the latter won’t help.
While quantifier elimination does not help with the existence of (non)recursive models, or with recognizing recursive models, it does have implications for other properties of recursive models. Specifically, if a model of the theory is recursive, then its satisfaction predicate has bounded complexity. In the case at hand, every recursive pseudofinite field has a $\Delta^0_2$ (more precisely, tt-reducible to $\emptyset'$) satisfaction predicate. Even more is true: pseudofinite fields are model-complete in a language expanded with constants for coefficients of irreducible polynomials of each degree, and this implies that for any fixed formula $\phi(x_1,\dots,x_n)$ and a recursive pseudofinite field $F$, the relation $\{\langle a_1,\dots,a_n\rangle:F\models\phi(a_1,\dots,a_n)\}$ defined by $\phi$ in $F$ is recursive.
A: To supply an example about a decidable theory having a non-recursive model: first-order theory of Boolean Algebra, established by Alfred Tarski in 1949 to be recursive. However, L.J.Feiner showed in his PhD thesis: Orderings and Boolean algebras not isomorphic to recursive ones (see http://dspace.mit.edu/bitstream/handle/1721.1/60738/29976019.pdf?sequence=1), 1967 that there exists a Boolean Algebra recursive in 0' but not recursive. However, if more restrictions are imposed on the given Boolean Algebra, we might expect the result to be true. For example, Rod Downey and Carl G. Jockusch showed: Every Low Boolean Algebra is Isomorphic to a Recursive One. http://www.jstor.org/discover/10.2307/2160766?uid=3738992&uid=2129&uid=2&uid=70&uid=4&sid=21103453523747
