[FOM] Graph minors

[Timothy Y. Chow]

If H is a (finite) graph, let MINOR(H) denote the family of graphs 
containing H as a minor.  Then it is a theorem (of Robertson and Seymour I 
think) that for any H, MINOR(H) is in P.  That is, whether a given graph G 
contains H as a minor can be determined in polynomial time.  My question 
is, what axioms are needed to prove this theorem?

Here's why I ask.  Suppose the above theorem is unprovable in some (sound) 
system S.  It is obvious, and presumably provable in any S you care to 
name, that for all H, MINOR(H) is in NP.  This would then seem to imply 
that if P = NP, then "P = NP" is independent of S.  For if P = NP, then S 
cannot prove P != NP since S is sound.  On the other hand, if S could 
prove P = NP, then in particular it should be able to prove that MINOR(H) 
is in P, which by hypothesis it can't.

The graph minor theorem is of course known to require strong axioms, but 
although the above result is related to the graph minor theorem, I don't 
know if it implies it.

A result of the form "if P = NP then it is independent of S" is perhaps 
not as interesting as a result of the form "if P != NP then it is 
independent of S," but I am not aware of any results of either type for 
"natural" choices of S.

Tim