Mathematics desk
< July 23	<< Jun \| July \| Aug >>	Current desk >

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

July 24

Minimum complexity of countable models of various theories

I have the notion that it is not possible to have a computable countable model of (for example) ZFC (and I would guess even of second-order arithmetic). But I haven't been able to come up with a promising proof sketch.

I'd like to argue that such a model would let you read off a solution to the halting problem, and probably you could do that from the elementary diagram of such a model -- but you could also do it from the elementary diagram of a model of Peano arithmetic, which obviously does have a computable modelsee below. And Peano arithmetic is certainly way stronger than needed to figure out whether a program halts, so this "argument from strength" seems unpromising on reflection.

Tennenbaum's theorem gives us that you can't have a computable nonstandard model of PA, and therefore you can't have a computable model of PA+s where s is any false statement of arithmetic. But that won't help us with things like ZFC, which prove only true statements.

Could it even be that I'm wrong, that there is such a model? I would have thought I'd have heard of that. --Trovatore (talk) 23:02, 24 July 2021 (UTC)[reply]

Second-order arithmetic allows quantification over sets of natural numbers. According to our article Model (logic), a model is a set with a collection of finitary operations and relations. Can quantification over sets of natural numbers be considered a finitary operation? In a context of computability, sets can be modeled as (computable) characteristic predicates, but then set equality is undecidable, as well as the propriety of a proposed finite description of a characteristic predicate. So there seems to be no computable approach that allows one to model quantification over sets of natural numbers. --Lambiam 00:04, 25 July 2021 (UTC)[reply]

Well, there's definitely no obvious reason to think there is a computable model. What's missing is a proof that there isn't. --Trovatore (talk) 02:26, 25 July 2021 (UTC)[reply]

If it has a non-standard

\omega

, then it contains a nonstandard model of PA, so Tennenbaum's theorem applies. If it has a standard

\omega

, then since ZFC proves the existence of the elementary diagram of standard arithmetic, you can read the halting problem off from an appropriate element.--2404:2000:2000:8:2186:CE90:152E:88AB (talk) 21:51, 25 July 2021 (UTC)[reply]

That's beautiful! Thanks very much! --Trovatore (talk) 05:06, 26 July 2021 (UTC)[reply]

Resolved

Basically, the difference between this and PA is that ZFC proves the halting set exists, while that's not even expressible in the language of PA.--2404:2000:2000:8:2186:CE90:152E:88AB (talk) 00:03, 26 July 2021 (UTC)[reply]

Before this goes into the archives I want to call out a mistake I made so it doesn't go into someone's unconscious collection of things we think are true. I said you could read off a solution of the halting problem from the elementary diagram of a model of ZFC or even PA. But that isn't necessarily true, if the model is nonstandard, or at least it isn't necessarily true in the way I was thinking.
Basically, I was thinking that you could ask the model if a Turing machine halts, because that's expressible in the language. But if the model is nonstandard, it might think that a Turing machine halts even if it doesn't. For example, you can have a model of PA+~Con(PA), and if you ask it whether a Turing machine searching for a contradiction in PA halts, it will say "yes", even though the correct answer is "no". But a model with a standard ω will always answer correctly (note that no model of PA+~Con(PA) has a standard ω).
I still don't know whether a countable model of ZFC or second-order arithmetic needs to be at least as complicated as the halting problem. There are sets that are not computable but do not solve the halting problem. --Trovatore (talk) 18:47, 31 July 2021 (UTC)[reply]