Question

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

Answer 1

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.

Answer 2

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.

Answer 3

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.