Wikipedia:Reference desk/Archives/Mathematics/2021 July 24
| 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[edit]
Minimum complexity of countable models of various theories[edit]
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)
- 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)
- If it has a non-standard , then it contains a nonstandard model of PA, so Tennenbaum's theorem applies. If it has a standard , 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)
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)
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)