Schlussfolgerungen aus der umgekehrten mathematischen Stärke des Graph Minor Theorems

Angenommen, wir haben eine Graph-Eigenschaft, die in nicht deterministischer Polynomzeit überprüft werden kann, und einen Beweis in einem schwachen formalen System (sagen wir RCA ₀ ), dass die Eigenschaft minor closed ist. Können wir etwas über die Stärke eines formalen Systems sagen, das beweisen kann, dass eine gegebene endliche Menge ausgeschlossener Minderjähriger die gegebene Grapheneigenschaft charakterisiert?

Ausgangssituation Es ist bekannt, dass bereits eine einfache Version (ohne gut geordnete Menge von Bezeichnungen) des Kruskalschen Baumsatzes in ATR ₀ nicht beweisbar ist, und dass der Graph-Minor-Satz eine Verallgemeinerung dieses Satzes ist, die in Π ¹ nicht einmal beweisbar ist ₁ -CA ₀ . Friedman verwendete diese einfache Version des Kruskal- Baumsatzes , um die schnell wachsende TREE (n) -Funktion zu konstruieren , und verwendete den Graph-Minor-Satz , um die noch schneller wachsende SSCG (n) -Funktion zu konstruieren . Das sind nette Demonstrationen von Schlussfolgerungen über Recheninhalte aus umgekehrter mathematischer Stärke, aber diese lassen die direktere Frage, die oben gestellt wurde, unbeantwortet.

In Verbindung mit dem Graph-Minor-Theorem wird nämlich der Beweis erbracht, dass kleinere geschlossene Eigenschaften in deterministischer kubischer Zeit getestet werden können, wenn man die Liste der ausgeschlossenen Minderjährigen für diese Eigenschaft kennt. Daher ist es selbstverständlich, sich zu fragen, wie "unmöglich" es ist, zu beweisen, dass man alle ausgeschlossenen Minderjährigen für ein gegebenes "leichtes" (wie in der Frage präzisiert) geschlossenes Nebenvermögen gefunden hat. Da dies eine "uneinheitliche" Aufgabe ist, ist mir nicht klar, ob die "Unmöglichkeit" dieser Aufgabe überhaupt mit der "Schwierigkeit" (dh der umgekehrten mathematischen Stärke) zusammenhängt, den Graph-Minor-Satz selbst zu beweisen.

Da die einfache Version des Kruskalschen Baumsatzes genau die gleichen Fragen wie der Graph-Minor-Satz aufwirft, können sich die Antworten auf dieses einfachere Problem konzentrieren, wenn sie wollen. Ich habe nur den Satz von Graph Minor verwendet, weil sich die Frage auf diese Weise natürlicher anfühlt. (Es ist möglich, dass diese Frage besser für MSE oder MSO geeignet war, zumindest um eine eindeutige Antwort zu erhalten. Die Motivation für diese Frage hängt jedoch eher mit TCS zusammen, weshalb ich mich entschied, sie hier zu stellen.)

Ich bin mir nicht sicher, ob ich Ihre Frage verstanden habe, aber wenn Sie sich fragen, wie schwierig es ist, die Anzahl der Hindernisse zu berechnen, sind Sie möglicherweise an folgenden Informationen interessiert: http://www.jucs.org/doi?doi=10.3217/jucs- 003-11-1194, wobei die Nicht- Kompatibilität auch dann nachgewiesen wird, wenn die Diagrammklasse MSOL-definierbar ist. In diesem Artikel http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub wird die Berechenbarkeit bewiesen, wenn die Diagrammklasse durch die HR-Grammatik vorgegeben wird.