Conclusions de la force mathématique inverse du théorème mineur des graphes

Supposons que nous ayons une propriété de graphe qui peut être vérifiée en temps polynomial non déterministe, et une preuve dans un système formel faible (disons RCA ₀ ) que la propriété est mineure fermée. Pouvons-nous dire quoi que ce soit sur la force d'un système formel, qui est capable de prouver qu'un ensemble fini donné de mineurs exclus caractérise la propriété de graphe donnée?

Contexte Il est bien connu que déjà une version simple (sans ensemble d'étiquettes bien quasi-ordonnées) du théorème d'arbre de Kruskal n'est pas démontrable dans ATR ₀ et le théorème du graphe mineur est une généralisation de ce théorème qui n'est même pas prouvable dans Π ¹ ₁ -CA ₀ . Friedman a utilisé cette version simple du théorème d'arbre de Kruskal pour construire la fonction TREE (n) à croissance rapide , et a utilisé le théorème du graphe mineur pour construire la fonction SSCG (n) à croissance encore plus rapide . Ce sont de belles démonstrations de conclusions sur le contenu informatique à partir de la force mathématique inverse, mais celles-ci laissent la question plus directe posée ci-dessus sans réponse.

À savoir, le théorème mineur du graphique est la preuve que les propriétés fermées mineures peuvent être testées en temps cubique déterministe, si l'on connaît la liste des mineurs exclus pour cette propriété. Il est donc naturel de se demander à quel point il est «impossible» de prouver que l'on a trouvé tous les mineurs exclus pour une propriété fermée mineure «facile» (comme précisé dans la question). Comme il s'agit d'une tâche "non uniforme", il n'est pas clair pour moi si "l'impossibilité" de cette tâche est liée du tout à la "difficulté" (c'est-à-dire la force mathématique inverse) de prouver le théorème du graphe mineur lui-même.

Puisque la version simple du théorème d'arbre de Kruskal pose exactement les mêmes questions que le théorème mineur du graphe, les réponses peuvent se concentrer sur ce problème plus simple, si elles le souhaitent. Je viens d'utiliser le théorème des graphes mineurs, car la question semble plus naturelle de cette façon. (Il est possible que cette question ait été plus appropriée pour MSE ou MSO, au moins en ce qui concerne l'obtention d'une réponse définitive. Mais la motivation de cette question est plus liée au TCS, j'ai donc décidé de la poser ici.)

Je ne suis pas sûr d'avoir compris votre question, mais si vous demandez à quel point il est difficile de calculer l'ensemble des obstructions, vous pouvez être intéressé par le http://www.jucs.org/doi?doi=10.3217/jucs- 003-11-1194 où la non calculabilité est prouvée même si la classe de graphe est définissable par MSOL. Dans cet article http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub la calculabilité est prouvée lorsque la classe de graphe est donnée par la grammaire HR.