Is there a computable model of ZFC? - MathOverflow most recent 30 from http://mathoverflow.net2013-05-25T19:43:26Zhttp://mathoverflow.net/feeds/question/12426http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfcIs there a computable model of ZFC?David Diamondstone2010-01-20T16:38:48Z2010-05-05T14:16:37Z
<p><strong>Background</strong></p>
<p>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.</p>
<blockquote>
<p>Can such a relation ever be computable?</p>
</blockquote>
<p><strong>Partial results</strong></p>
<p>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}.</p>
http://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc/12431#12431Answer by Anonymous for Is there a computable model of ZFC?Anonymous2010-01-20T17:44:19Z2010-01-20T18:54:43Z<p>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.)</p>
<p>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.</p>
http://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc/12434#12434Answer by Joel David Hamkins for Is there a computable model of ZFC?Joel David Hamkins2010-01-20T18:09:09Z2010-01-20T18:15:23Z<p>The Tennenbaum phenomenon is amazing, and that is totally correct, but let me give a direct proof using the idea of <a href="http://en.wikipedia.org/wiki/Effectively%5Fseparable" rel="nofollow">computable inseparability</a>.</p>
<p><b>Theorem</b>. There is no computable model of ZFC.</p>
<p>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. </p>
<p>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<sup>th</sup> 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<sup>th</sup> natural number. Let me denote i(n) simply by <b>n</b>. (We
could computably rearrange things, if desired, so that these were, say, the odd numbers). </p>
<p>Let A, B be any <a href="http://en.wikipedia.org/wiki/Effectively%5Fseparable" rel="nofollow">computably inseparable</a> 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<sub>0</sub> and p<sub>1</sub> that
enumerate them (in our universe). These programs are finite, and M agrees that <b>p<sub>0</sub></b> and <b>p<sub>1</sub></b> 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 <b>p<sub>0</sub></b> before they are enumerated by <b>p<sub>1</sub></b>. Let A<sup>+</sup> = { n | <b>n</b> 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<sup>+</sup>, 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<sup>+</sup>, because M can see that they are enumerated into B by a (standard)
stage, when they have not been enumerated into A. Thus, A<sup>+</sup> is a computable separation of A and B, a contradiction. QED</p>
<p>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 <em>neither</em> plus nor times individually is computable in a nonstandard model of PA. And this takes a somewhat more subtle argument.</p>
http://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc/23591#23591Answer by Dave Marker for Is there a computable model of ZFC?Dave Marker2010-05-05T14:16:37Z2010-05-05T14:16:37Z<p>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.</p>
<p>Of course the appeal to Godel-Roesser just hides Joel's argument about recursive inseparable r.e. sets.</p>