Conclusions from reverse mathematical strength of graph minor theorem 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 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, and used the graph minor theorem to construct the even faster growing SSCG(n) 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.)
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.