I'm working on the following problem at the moment:
Let $\mathcal{L} = \{R\}$, where $R$ is a binary relation symbol. Let $T$ be a consistent, decidable $\cal{L}$-theory, and let $p(x)$ be a decidable, nonprincipal 1-type of $T$. Show that $T$ has a model $\mathcal{A} = \langle A, R^\mathcal{A}\rangle$ such that both $A$ and $R^\mathcal{A}$ are recursive.
When it comes to mixing model theory and recursion theory, I'm kind of clueless. Is the idea behind these kinds of problems to perform Henkin-esque constructions but somehow guarantee that the result is decidable? Any hints or suggestions regarding this problem, or intuitions regarding recursive model theory more generally, would be extremely beneficial!
I assume that you follow the usual convention whereby a $1$-type is complete. Invent a new constant symbol $c$, and work with the complete theory $p(c)$ in the enlarged language. It's consistent, complete, and decidable. Now go through the Henkin construction: Adjoin Henkin constants (or Skolem functions, depending on which presentation of the Henkin construction you like), with their associated axioms, and then complete the resulting theory. The key observation is that the completion process can be carried out recursively, because, at each stage, you're looking at some sentence $\theta$ and adjoining it to your theory if and only if it is consistent with all you've done previously. This consistency is a matter of (un)provability of some sentence in $p(c)$, which is, by assumption decidable. So you get a decidable, complete, Henkin theory. The model determined by that theory will be a recursive model.