Timeline for Weakest choice principle required for Robertson-Seymour Graph Minor Theorem?
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 2, 2013 at 11:45 | comment | added | András Salamon | That seems to settle things -- thanks for elaborating. | |
| May 2, 2013 at 11:44 | vote | accept | András Salamon | ||
| May 2, 2013 at 11:20 | comment | added | Emil Jeřábek | BI is bar induction, formulated as the following schema in second-order arithmetic for any formulas $x\prec y$ and $\phi(x)$: if $\prec$ is a well order, then transfinite induction along $\prec$ holds for $\phi$. | |
| May 1, 2013 at 1:48 | comment | added | András Salamon | Andrey Bovykin's "Unprovability threshold for the planar graph minor theorem" from 2010 states that the upper bound for the Graph Minor Theorem is $\Pi_1^1-\text{CA}+\text{BI}$, from the Friedman/Robertson/Seymour paper mentioned in the question. I am not familiar with BI -- but is this just a fragment of second-order arithmetic? | |
| Apr 30, 2013 at 19:14 | comment | added | François G. Dorais | Nash-Williams's proof probably does use AC. Since ZFC is conservative over ZF for $\Pi^1_1$ statements, this does no harm and the result is still provable without AC. The key is that if $r$ codes a counterexample in $V$, then that must be a counterexample in $L[r]$ too, but AC is true in $L[r]$ so the Nash-Williams proof works in there. Furthermore, in this analysis, the definition of wqo being used is immaterial. | |
| Apr 30, 2013 at 17:51 | comment | added | Emil Jeřábek | Yes, I claim that Kruskal’s theorem for unlabelled finite trees is provable without AC. More generally, the same kind of argument should apply to Kruskal’s theorem for finite trees with labels coming from a countable wqo. | |
| Apr 30, 2013 at 17:29 | comment | added | Timothy Chow | Emil, I'm thinking of R–S as, "Finite unlabeled graphs form a wqo under the graph minor relation," and Kruskal's theorem as, "Finite unlabeled trees form a wqo under the graph minor relation." What I'm familiar with is Nash-Williams's proof of Kruskal's theorem, which proceeds by using AC to find a minimal bad sequence. Are you saying that AC isn't needed for this weak version of Kruskal's theorem? | |
| Apr 30, 2013 at 16:01 | comment | added | Emil Jeřábek | Yes, I understood that. And what I am trying to say is that the form of Krukal’s theorem which follows from the Graph minor theorem is most likely a different one than the form of Kruskal’s theorem which needs choice. | |
| Apr 30, 2013 at 15:53 | comment | added | András Salamon | Emil, I think Timothy was just trying to say that (some form of) Kruskal's Tree Theorem is a special case of (some form of) Graph Minor Theorem, yet KTT usually does seem to need some form of choice. | |
| Apr 30, 2013 at 15:43 | comment | added | Emil Jeřábek | Can you state exactly which form of Kruskal’s theorem you have in mind? In particular, the formulation on Wikipedia allows labelled trees, where the labels may come from an arbitrary wqo. I don’t see how to reduce this to R–S. I can well imagine that this might require some choice, and in particular the argument I’m using does not work as there is no obvious way how to handle the labels, but this does not seem to contradict anything I say about R–S. | |
| Apr 30, 2013 at 15:00 | comment | added | Timothy Chow | I'm confused about something here. R-S includes Kruskal's tree theorem, which as usually formulated requires a weak form of AC, doesn't it? How are you getting around this? It must be some subtlety in the definition of wqo that you're using? | |
| Apr 30, 2013 at 12:04 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |