lo.logic - 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.