<p>I am not sure I understood your question, but if you are asking how difficult it is to compute the set of obstructions, you may be interested in the following <a href="http://www.jucs.org/doi?doi=10.3217/jucs-003-11-1194" rel="noreferrer">http://www.jucs.org/doi?doi=10.3217/jucs-003-11-1194</a> where the non computabubility is proved even if the graph class is MSOL-definable. In this paper <a href="http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub" rel="noreferrer">http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub</a> the computability is proved when the graph class is given by the HR grammar. </p>

CC BY-SA 3.0
2017-10-30T09:21:00.353Z
Yes, I am asking how "impossible" it is to compute the set of obstructions. I am confident that your references will answer my questions.  ("MSOL-definable" and "can be checked in nondeterministic polynomial time" are essentially the same thing, in the context of graph properties.)
Thomas Klimpel
CC BY-SA 3.0
2017-10-30T08:50:15.617Z
2017-10-30T08:50:15.617Z
M. kanté
<p>Say we have a graph property which can be checked in nondeterministic polynomial time, and a proof in a weak formal system (say RCA<sub>0</sub>) that the property is minor closed. Can we say anything about the strength of a formal system, which is able to prove that a given finite set of excluded-minors characterises the given graph property?</p>

<hr>

<p><strong>Context</strong> It is well known that already a simple version (without well-quasi-ordered set of labels) of <a href="https://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem" rel="noreferrer">Kruskal's tree theorem</a> is unprovable in ATR<sub>0</sub> and the graph minor theorem is a generalisation of that theorem which isn't even provable in Π<sup>1</sup><sub>1</sub>-CA<sub>0</sub>. Friedman used that simple version of Kruskal's tree theorem to construct the fast growing <a href="https://cp4space.wordpress.com/2012/12/19/fast-growing-2/" rel="noreferrer">TREE(n) function</a>, and used the <a href="https://cp4space.wordpress.com/2013/01/13/graph-minors/" rel="noreferrer">graph minor theorem</a> to construct the even faster growing <a href="https://en.wikipedia.org/wiki/Friedman%27s_SSCG_function" rel="noreferrer">SSCG(n) function</a>. Those are nice demonstrations of conclusions about computational content from reverse mathematical strength, but those leave the more direct question posed above unanswered.</p>

<p>Namely, related to the graph minor theorem is the proof that minor closed properties can be tested in deterministic cubic time, if one knows the list of excluded minors for that property. Hence it is natural to wonder just how "impossible" it is to prove that one has found all excluded minors for a given "easy" (as made precise in the question) minor closed property. Since this is a "non-uniform" task, it is not clear to me whether the "impossibility" of this task is related at all to the "difficulty" (i.e. reverse mathematical strength) of proving the graph minor theorem itself.</p>

<p>Since the simple version of Kruskal's tree theorem poses exactly the same questions as the graph minor theorem, answers may focus on that simpler problem, if they want. I just used the graph minor theorem, because the question feels more natural that way. (It is possible that this question might have been more suitable to MSE or MSO, at least with respect to getting a definite answer. But the motivation of this question is more related to TCS, so I decided to ask it here.)</p>

<cc.complexity-theory><lo.logic>
Conclusions from reverse mathematical strength of graph minor theorem
Thomas Klimpel
# Conclusions from reverse mathematical strength of graph minor theorem

(Asked by: username_0 on 2017-10-28)

Say we have a graph property which can be checked in nondeterministic polynomial time, and a proof in a weak formal system (say RCA0) that the property is minor closed. Can we say anything about the strength of a formal system, which is able to prove that a given finite set of excluded-minors characterises the given graph property?

---

**Context** It is well known that already a simple version (without well-quasi-ordered set of labels) of [Kruskal's tree theorem](https://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem) is unprovable in ATR0 and the graph minor theorem is a generalisation of that theorem which isn't even provable in Π11-CA0. Friedman used that simple version of Kruskal's tree theorem to construct the fast growing [TREE(n) function](https://cp4space.wordpress.com/2012/12/19/fast-growing-2/), and used the [graph minor theorem](https://cp4space.wordpress.com/2013/01/13/graph-minors/) to construct the even faster growing [SSCG(n) function](https://en.wikipedia.org/wiki/Friedman%27s_SSCG_function). Those are nice demonstrations of conclusions about computational content from reverse mathematical strength, but those leave the more direct question posed above unanswered.

Namely, related to the graph minor theorem is the proof that minor closed properties can be tested in deterministic cubic time, if one knows the list of excluded minors for that property. Hence it is natural to wonder just how "impossible" it is to prove that one has found all excluded minors for a given "easy" (as made precise in the question) minor closed property. Since this is a "non-uniform" task, it is not clear to me whether the "impossibility" of this task is related at all to the "difficulty" (i.e. reverse mathematical strength) of proving the graph minor theorem itself.

Since the simple version of Kruskal's tree theorem poses exactly the same questions as the graph minor theorem, answers may focus on that simpler problem, if they want. I just used the graph minor theorem, because the question feels more natural that way. (It is possible that this question might have been more suitable to MSE or MSO, at least with respect to getting a definite answer. But the motivation of this question is more related to TCS, so I decided to ask it here.)

**Tags:** cc.complexity-theory, lo.logic


---

## 1 answers

### Answer by username_1 on 2017-10-30. Score: 10 | Accepted answer

I am not sure I understood your question, but if you are asking how difficult it is to compute the set of obstructions, you may be interested in the following <http://www.jucs.org/doi?doi=10.3217/jucs-003-11-1194> where the non computabubility is proved even if the graph class is MSOL-definable. In this paper <http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub> the computability is proved when the graph class is given by the HR grammar.

> **Comments:**
> **username_0**: Yes, I am asking how "impossible" it is to compute the set of obstructions. I am confident that your references will answer my questions.  ("MSOL-definable" and "can be checked in nondeterministic polynomial time" are essentially the same thing, in the context of graph properties.)  

---

