Is there a "computable" countable model of ZFC?

Question

Assuming ZFC is consistent (has a model), does there exist a set $S$ and a binary relation $\in_S$ on $S$ that satisfy the following?

1. $S \subseteq \{0,1\}^*$ (this is the Kleene star, and in particular $S$ is countable);

2. $S$ is decidable, i.e. there exists a Turing machine $C$ such that on input any binary string $x$, $C$ halts and accepts when $x \in S$ and halts and rejects otherwise;

3. $\in_S$ is decidable, i.e. there exists a Turing machine $D$ such that on input any ordered pair $(x,y) \in S \times S$, $D$ halts and accepts when $x \in_S y$, and halts and rejects otherwise;

4. $(S, \in_S)$ is a model of the axioms of ZFC.

Details

Essentially, I'm interested in whether every consistent theory has a "computable" model in the above sense. Of course, it is easy to see that theories like DLOWE (dense linear orders without endpoints) and even first-order Peano Arithmetic have such models--just let $S$ be the set of rational numbers and integers, respectively, encoded in binary in some canonical way, and it is a standard result that $<, +, \cdots$, etc. are computable operations. So I thought ZFC might be a good harder example to try--but I haven't been able to argue for the existence a model of the required form.

I posed this question to a friend and they objected that maybe every countable set, with any binary operation, can be considered computable in this sense--after all, you're allowed to assign the elements of the countable set to binary strings in any way you like. However, this is not true. Let $S$ be the vertices of a directed graph which consists of a single directed cycle for each integer $n$, where the cycle has length busy beaver of $n$. Let $\in_S$ be the binary relation corresponding to this directed graph. Then I have proven that $\in_S$ is not a decidable relation, no matter how you assign vertices in $S$ to strings. So it is conceivable that a countable model of set theory is similarly not computable.

Great question! This was already considered at Mathoverflow; the answer is no. See https://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc.

I've made this community wiki so I don't get a reputation bonus from others' hard work; I would vote to close as a duplicate, but the system won't let me, since the duplicate question isn't on math.stackexchange.

Note that, despite this, we can ask: how complicated must a countable model of ZFC be? Since ZFC is a computable first-order theory, any PA degree computes such a model, and there are many such degrees; in fact, there are PA degrees which are low, that is, whose jump is Turing reducible to the Halting problem (= as small as possible). Conversely, the arguments at the mathoverflow question cited above show that any countable model of ZFC is of PA degree, so this is an exact characterization.

Note that very little specifically about ZFC is used here! Specifically, and addressing your general question: Henkin's construction shows that any PA degree computes a model of any computable first-order theory, and that conversely any degree which is not PA fails to compute a model of some computable first-order theory; though of course, for specific theories, the set of degrees of models of that theory might be more complicated. This set, by the way, has been studied a little; it is called the spectrum of the theory. See http://www.math.wisc.edu/~andrews/spectra.pdf.