Timeline for Are there any undecidability results that are not known to have a diagonal argument proof?
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 10 at 12:11 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
Fixed error in the size estimate
|
| Sep 8, 2023 at 21:55 | comment | added | Joel David Hamkins | @TerryTao Thanks for accepting. I agree that this should be viewed as an ongoing project. Perhaps other better answers will come in later... For the moment, I think the interesting philosophical question here is: what counts as a diagonal argument? | |
| Sep 8, 2023 at 21:53 | comment | added | Terry Tao | I have provisionally accepted this answer as the leading candidate currently proposed for an undecidability result whose known proofs, while certainly containing diagonalization-like themes, do not seem to contain diagonalization (as narrowly interpreted) as an essential component. But I admit that this is a somewhat subjective call, and am open to being persuaded to other points of view. | |
| Sep 8, 2023 at 21:52 | vote | accept | Terry Tao | ||
| Sep 7, 2023 at 1:22 | comment | added | Terry Tao | @JasonRute I'm looking up the proofs of the reduction of the halting problem to the Kolmogorov complexity problem and they seem to rely on the Berry type argument that Joel provided in order to justify the reduction. If so, then I would say that this is a "gratuitious" way to shoehorn in a diagonalization. Do you know of a proof of reduction that doesn't contain something resembling Joel's argument? | |
| Sep 6, 2023 at 22:54 | comment | added | Joel David Hamkins | More seriously, I was attempting to rebut your claim that there might be no examples in model theory "descended from diagonalization". It seems to me that back-and-forth, saturation, universality, omitting types, and so on all fit the bill, with my way of understanding the nature of diagonalization. And I view these as core model-theoretic ideas. | |
| Sep 6, 2023 at 22:50 | comment | added | Joel David Hamkins | Yes, I'd agree with that. I guess I hadn't realized the extent to which y'all aren't really doing logic any more! :-) jk | |
| Sep 6, 2023 at 22:48 | comment | added | James E Hanson | @JoelDavidHamkins I agree that things like the omitting types theorem and other forcing-like stuff can be thought of in terms of diagonalization, provided that your view of diagonalization is broad enough to essentially encompass any application of the Baire category theorem (which I think mine is) but I still don't really see it for a lot of modern model theory like stability and neo-stability. | |
| Sep 6, 2023 at 22:43 | comment | added | Joel David Hamkins | @cody Who says that cut-eliminatio is not part of logic? Obviously it is. | |
| Sep 6, 2023 at 22:40 | comment | added | Joel David Hamkins | @JamesHanson To my way of thinking, the essence of diagonalization is performing a construction to meet various requirements, where the number of requirements is the same as the length of the construction, and they are met one by one. Many core model theory theorems are proved this way. This is the key idea of the back-and-forth construction and hence also the key to saturation, universality, and so forth, all core model-theoretic ideas. This abstract view of diagonalization thus seems to appear at the bottom of many model-theoretic ideas. | |
| Sep 6, 2023 at 19:58 | comment | added | cody | As a (sort of) proof theorist, I'm sad that cut-elimination is not considered to be part of logic... | |
| Sep 6, 2023 at 19:28 | comment | added | Jason Rute | But we can also show that Kolmogorov complexity solves the halting problem, and the halting problem isn’t computable, so Kolmogorov complexity isn’t computable. So transitivity it has a proof (not the standard one) by diagonalization. | |
| Sep 6, 2023 at 19:04 | comment | added | James E Hanson | I also take an extremely broad view of diagonalization, but I'm actually struggling to come up with examples in model theory of arguments that I would consider to really be descended from diagonalization. (Of course there are a few people both inside and outside of model theory who don't really consider it 'logic' at this point, but that's a separate issue.) | |
| Sep 6, 2023 at 18:39 | comment | added | Terry Tao | Nice example. I guess I can accept this type of argument (and similar "Berry's paradox" type arguments) as not strictly being a diagonal argument, though it certainly has a similar "self-defeating object" flavor to it, and I can't see a natural way to replace it with a more obviously diagonalization style argument. | |
| Sep 6, 2023 at 18:09 | history | answered | Joel David Hamkins | CC BY-SA 4.0 |