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