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.

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 n^th 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 n^th 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 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 p₀ and p₁ that enumerate them (in our universe). These programs are finite, and M agrees that p₀ and p₁ 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 p₀ before they are enumerated by p₁. 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, 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.

No, it cannot be computable. It's a theorem of Tennenbaum from the 50's that there is no computable, non-standard model of Peano arithmetic. If there were a computable model of ZFC, then it would give a computable, non-standard model of Peano arithmetic. Specifically, it would contain some non-standard model for PA, specified by a set of elements and two relations, and the computability of the model of ZFC would imply computability there. (If, say, you want the sum of elements a and b in the model of PA, search by brute force for an element c of the model such that (a,b,c) is in the sum relation. This may be terribly slow, but it will eventually terminate.)

Edit: That's a good point about the computability of (a,b,c), and I'm not sure how to compute that. Fortunately, it turns out not to be needed here. Specifically, if we define (a,b,c) = ((a,b),c) and define (u,v) = {{u}, {u,v}}, then even though it's not clear whether you can computably produce (a,b,c) given a, b, and c, given something you know a priori is a triple, you can try to check whether it comes from a,b,c by finding appropriate elements. (In the simpler case of pairs, to check whether w = (u,v) given that it is some ordered pair, we just need to find x and y such that both are in w, u is in x, and u and v are in y.) Now we just do major brute force: not only searching over all possible choices of c, but also over the auxiliary elements that would establish that (a,b,c) is in the relation. I hope there's a nicer way to do this, but I think it works.

This can also be done using Godel-Roesser instead of Tennebaum. Suppose M is a model of ZFC. There is an element $a$ of that M believes is the set of Godel codes for the sentences true of the integers of M. Of course $a$ may contain nonstandard Godel codes, but if we let T be the set of standard sentences with Godel codes in $a$, then T will be a complete consistent extension of Peano Arithmetic. If M is computable, then T would be computable, but there are no computable complete consistent extensions of Peano Arithmetic.

Of course the appeal to Godel-Roesser just hides Joel's argument about recursive inseparable r.e. sets.