**Background**


Assuming ZFC is consistent, then by downward Löwenheim–Skolem, there is a countable model (M,$\in$) of ZFC. Since the universe M is countable, we may as well think of it as actually being the set of natural numbers, so $\in$ will be some binary relation on the natural numbers.



> 
> Can such a relation ever be computable?
> 
> 
> 


**Partial results**


~~One can show that the class of binary relations $R$ on the natural numbers such that $(\mathbb{N},R) \models ZFC$ forms a $\Pi\_0^1$ class, and will be nonempty so long as ZFC is consistent. This already gives us some interesting results. For example, by the low basis theorem, there is a low $R$ such that $(\mathbb{N},R) \models ZFC$. But I have been unable to determine whether such a function can be made computable; the best I can do is show that if such a function is computable, then there is no effective way of finding, given a finite set D of natural numbers, the element n such that D={m : mRn}.~~



Is there a computable model of ZFC?
The Tennenbaum phenomenon is amazing, and that is totally correct, but let me give a direct proof using the idea of [computable inseparability](http://en.wikipedia.org/wiki/Effectively_separable).


**Theorem**. There is no computable model of ZFC.


Proof: Suppose to the contrary that M is a computable model of ZFC. That is, we assume that the underlying set of M is ω and the membership relation E of M is computable. 


First, we may overcome the issue you mention at the end of your question, and we can computably get access to what M thinks of as the 
nth natural number, for any natural number n. To see this, observe first that there is a particular natural number z, which M believes 
is the natural number 0, another natural number N, which M believes to the set of all natural numbers, and another natural number s, which M 
believes is the successor function on the natural numbers. By decoding what it means to evaluate a function in set theory using ordered pairs, We 
may now successively compute the function i(0)=z and i(n+1) = the unique number that M believes is the successor function s of i(n). Thus, 
externally, we now have computable access to what M believes is the nth natural number. Let me denote i(n) simply by **n**. (We 
could computably rearrange things, if desired, so that these were, say, the odd numbers). 


Let A, B be any [computably inseparable](http://en.wikipedia.org/wiki/Effectively_separable) sets. That is, A and B are disjoint computably 
enumerable sets having no computable separation. (For example, A is the set of TM programs halting with output 0 on input 0, and B is the set of 
programs halting with output 1 on input 0.) Since A and B are each computably enumerable, there are programs p0 and p1 that 
enumerate them (in our universe). These programs are finite, and M agrees that **p0** and **p1** are TM programs that 
enumerate a set of what it thinks are natural numbers. There is some particular natural number c that M thinks is the set of natural numbers 
enumerated by **p0** before they are enumerated by **p1**. Let A+ = { n | **n** E c }, which is the set 
of natural numbers n that M thinks are enumerated into M's version of A before they are enumerated into M's version of B. This is a computable 
set, since E is computable. Also, every member of A is in A+, since any number actually enumerated into A will be seen by M to have 
been so. Finally, for the same reason, no member of B is in A+, because M can see that they are enumerated into B by a (standard) 
stage, when they have not been enumerated into A. Thus, A+ is a computable separation of A and B, a contradiction. QED


Essentially this argument also establishes the version of Tennenbaum's theorem mentioned by Anonymous, that there is no computable nonstandard 
model of PA. But actually, Tennenbaum proved a stronger result, showing that *neither* plus nor times individually is computable in a nonstandard model of PA. And this takes a somewhat more subtle argument.


**Edit (4/11/2017).** The question was just bumped by another edit, and so I thought it made sense to update my answer here by mentioning a generalization of the result. Namely, in recent joint work, 


* M. T. Godziszewski and J. D. Hamkins, [Computable quotient presentations of models of arithmetic and set theory](http://jdh.hamkins.org/computable-quotient-presentations-of-models-of-arithmetic-and-set-theory/), click through for pdf at the arxiv.


we prove that not only is there no computable model of ZFC, but also there is no computable quotient presentation of a model of ZFC, and indeed there is no c.e. quotient presentation of such a model, by an equivalence relation of any complexity. That is, there is no c.e. relation $\hat\in$ and equivalence relation $E$, of any complexity, which is a congruence with respect to $\hat\in$, such that the quotient $\langle\mathbb{N},\hat\in\rangle/E$ is a model of ZFC.


