Conclusiones de la fuerza matemática inversa del teorema menor del gráfico

Supongamos que tenemos una propiedad gráfica que se puede verificar en tiempo polinomial no determinista, y una prueba en un sistema formal débil (digamos RCA ₀ ) de que la propiedad está cerrada de forma menor. ¿Podemos decir algo sobre la fortaleza de un sistema formal, que puede demostrar que un conjunto finito determinado de menores excluidos caracteriza la propiedad gráfica dada?

Contexto Es bien sabido que una versión simple (sin un conjunto de etiquetas bien ordenadas) del teorema del árbol de Kruskal no es demostrable en ATR ₀ y el teorema menor del gráfico es una generalización de ese teorema que ni siquiera es demostrable en Π ¹ ₁ -CA ₀ . Friedman usó esa versión simple del teorema del árbol de Kruskal para construir la función TREE (n) de crecimiento rápido , y usó el teorema menor del gráfico para construir la función SSCG (n) de crecimiento aún más rápido . Esas son buenas demostraciones de conclusiones sobre el contenido computacional de la fuerza matemática inversa, pero dejan sin respuesta la pregunta más directa planteada anteriormente.

A saber, el teorema menor del gráfico es la prueba de que las propiedades cerradas menores se pueden probar en tiempo cúbico determinista, si se conoce la lista de menores excluidos para esa propiedad. Por lo tanto, es natural preguntarse cuán "imposible" es demostrar que uno ha encontrado a todos los menores excluidos para una propiedad cerrada menor "fácil" (como se precisa en la pregunta). Dado que esta es una tarea "no uniforme", no me queda claro si la "imposibilidad" de esta tarea está relacionada en absoluto con la "dificultad" (es decir, la fuerza matemática inversa) de probar el teorema menor del gráfico.

Dado que la versión simple del teorema del árbol de Kruskal plantea exactamente las mismas preguntas que el teorema menor del gráfico, las respuestas pueden centrarse en ese problema más simple, si así lo desean. Acabo de usar el teorema del gráfico menor, porque la pregunta se siente más natural de esa manera. (Es posible que esta pregunta haya sido más adecuada para MSE o MSO, al menos con respecto a obtener una respuesta definitiva. Pero la motivación de esta pregunta está más relacionada con TCS, así que decidí hacerla aquí).

No estoy seguro de haber entendido su pregunta, pero si pregunta qué tan difícil es calcular el conjunto de obstrucciones, puede interesarle lo siguiente http://www.jucs.org/doi?doi=10.3217/jucs- 003-11-1194 donde se demuestra la no computabubilidad incluso si la clase de gráfico es definible por MSOL. En este artículo, http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub, la computabilidad se prueba cuando la gramática de recursos humanos da la clase de grafo.