Timeline for List of long open, elementary problems which are computational in nature
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 25, 2020 at 17:56 | comment | added | Timothy Chow | By the way, I should correct something I said about Faltings's theorem. In this case there are effective bounds on the number of solutions, just no effective bounds on their size. But the point remains that these results require extra insight into the problem in question; they don't follow from generalities about logic. | |
| Apr 25, 2020 at 17:43 | comment | added | Timothy Chow | @HenryTowsner : There's a potentially misleading sentence in that paper: "It has been shown that Theorem 1 is independent of constructive axiomatic systems." By this is meant that FRS showed independence from (say) RCA$_0$, but that's a separate question from ineffectivity. RCA$_0$ uses classical logic and can still prove ineffective theorems, and conversely, unprovability in RCA$_0$ does not imply ineffectivity. | |
| Apr 25, 2020 at 16:42 | comment | added | Henry Towsner | @cody: Theorem 8 of "On search, decision, and the efficiency of polynomial-time algorithms". Classical $\Pi^0_2$ statements are conservative over intuitionistic ones; $\Sigma^0_2$ statements are generally not. | |
| Apr 25, 2020 at 16:18 | comment | added | Timothy Chow | Intuitionistically speaking, I believe that all that has been proved is that the set of forbidden minors is not infinite. I don't think that there is an intuitionistic proof that the set is finite. | |
| Apr 25, 2020 at 15:36 | comment | added | cody | @HenryTowsner can you point me to the diagonal argument? I'm not sure I can follow it, but I do seem to recall that classical $\Sigma^0_2$ statements are conservative over intuitionistic ones, so I want to at least try to clarify my understanding. | |
| Apr 25, 2020 at 15:34 | comment | added | cody | @TimothyChow I was actually thinking about the $\mathrm{TREE}(n)$ numbers as an example! but Henry's answer has clarified things. | |
| Apr 25, 2020 at 13:41 | comment | added | Timothy Chow | By the way, if Robertson-Seymour seems like an intimidating black box that gives you the nagging worry that it's hiding something, I recommend that you look at something simpler, such as Kruskal's tree theorem, where you can grasp the whole proof. Then you can see for yourself that in general you can mine the proof until the cows come home, but you can't get an effective upper bound on the size of a finite forbidden set. | |
| Apr 25, 2020 at 13:34 | comment | added | Henry Towsner | @cody: The issue is not that it's non-constructive (proof mining often gets bounds from non-constructive proofs). The issue is that the statement is Sigma2 ("there exists a finite set of minors such that for all finite non-toroidal graphs..."), so proof mining gives a weaker statement than a bound on the finite number. We know this to optimal in this case, because there's a diagonalization argument showing that the bound can't be computed. One thing that is possible is an assignment of ordinals to finite families such that each time we add a new forbidden minor, the assigned ordinal decreases. | |
| Apr 25, 2020 at 13:27 | comment | added | Timothy Chow | @user36212 : I don't think you can argue that way. At the end of the day, the set of forbidden minors is finite, so its growth rate is zero. It's only in the reductio ad absurdum part of the proof that an infinite set is postulated. It's the same story with all those ineffective theorems in number theory, like Faltings's theorem. Just because the proof can be formalized in some weak system doesn't mean that you can get bounds on the size of provably finite sets. As long as you're using classical logic rather than intuitionistic logic, there's no guarantee of effectivity. | |
| Apr 25, 2020 at 9:42 | comment | added | user36212 | Isn’t it more or less true that the logical strength needed for the proof imposes an upper bound on how the number of forbidden minors can grow, since the logical strength is basically equivalent to the fastest growing function which the logic can define? And there is of course a feature of toroidal graphs which is relevant: they all admit an almost-embedding on a surface of genus 1 (which is the induction parameter in Robertson-Seymour). So one might be able to get something relevant by really looking at the proof. | |
| Apr 25, 2020 at 5:33 | comment | added | Timothy Chow | @cody : You can't always get a bound, since the proof is by contradiction. Assume the set S of forbidden minors is infinite. Then there must be 2 members of S such that one is a minor of the other; contradiction. This uses excluded middle and is ineffective. Now if you can prove that the set of forbidden minors must grow at some controlled rate r, then you can mine the proof to get a bound f(r) on how far you have to go to get the requisite 2 graphs. Here f is your astronomical function. But you still need control over r in the first place, and I don't think this is known for toroidal graphs. | |
| Apr 25, 2020 at 3:44 | comment | added | cody | Certainly, the proof that it is finite is a (non-constructive) proof that it is bounded by a natural number, based on the fact that it is closed by minors. My understanding is that such proofs can be proof mined to obtain constructive bounds, in this case, depending on the proof that it is minor closed, and the ambient logic of the proof. Again, this number is likely to be astronomical. | |
| Apr 24, 2020 at 18:21 | comment | added | Timothy Chow | @cody : I don't think so. Robertson and Seymour proved Wagner's conjecture that any minor-closed family has a finite forbidden minor characterization. If all you know is that a family is minor-closed, that does not imply any upper bound on the number of minors or the size of the minors. To get a bound, you would have to use some special fact about toroidal graphs, and I don't think anything like that is known. | |
| Apr 24, 2020 at 18:01 | comment | added | cody | I imagine that the proof can be mined to give an upper bound though right? Obviously, it's likely that that bound is hilariously large though. | |
| Apr 24, 2020 at 15:45 | history | made wiki | Post Made Community Wiki by Todd Trimble | ||
| Apr 24, 2020 at 15:39 | history | edited | Timothy Chow | CC BY-SA 4.0 | added 31 characters in body |
| Apr 24, 2020 at 13:48 | history | edited | Timothy Chow | CC BY-SA 4.0 | Added a reference |
| Apr 24, 2020 at 13:39 | history | answered | Timothy Chow | CC BY-SA 4.0 |