Выводы из обратной математической силы теоремы о графе

Скажем, у нас есть свойство графа, которое можно проверить в недетерминированном полиномиальном времени, и доказательство в слабой формальной системе (скажем, RCA ₀ ), что свойство является минорным. Можем ли мы что-нибудь сказать о силе формальной системы, которая может доказать, что данный конечный набор исключенных миноров характеризует данное свойство графа?

Контекст Хорошо известно, что уже простая версия (без хорошо квазиупорядоченного набора меток) теоремы Крускала о дереве недоказуема в ATR _0, а теорема о второстепенном графе является обобщением этой теоремы, которая даже не доказана в § ¹ ₁ -CA ₀ . Фридман использовал эту простую версию теоремы Крускала о дереве для построения быстро растущей функции TREE (n) и использовал теорему о второстепенном графике для построения еще более быстро растущей функции SSCG (n) . Это хорошие демонстрации выводов о вычислительном содержании из обратной математической силы, но они оставляют без ответа более прямой вопрос, поставленный выше.

А именно, к теореме о второстепенном графе относится доказательство того, что второстепенные замкнутые свойства могут быть проверены в детерминистическом кубическом времени, если известен список исключенных миноров для этого свойства. Следовательно, естественно задаться вопросом, насколько «невозможно» доказать, что найдены все исключенные несовершеннолетние для данного «легкого» (как уточняется в вопросе) второстепенного закрытого свойства. Поскольку это «неоднородная» задача, мне не ясно, связана ли вообще «невозможность» этой задачи с «сложностью» (т. Е. Обратной математической силой) доказательства самой теоремы о второстепенном графе.

Поскольку простая версия теоремы Крускала о дереве ставит те же вопросы, что и теорема о второстепенном графе, ответы могут быть сосредоточены на этой более простой задаче, если они захотят. Я просто использовал теорему о графе, потому что этот вопрос кажется более естественным. (Возможно, что этот вопрос мог бы быть более подходящим для MSE или MSO, по крайней мере, в отношении получения определенного ответа. Но мотивация этого вопроса больше связана с TCS, поэтому я решил задать его здесь.)

Я не уверен, что понял ваш вопрос, но если вы спрашиваете, насколько сложно вычислить набор препятствий, вас может заинтересовать следующее http://www.jucs.org/doi?doi=10.3217/jucs- 003-11-1194, где не вычислимость доказана, даже если класс графов определим по MSOL. В этой статье http://www.sciencedirect.com/science/article/pii/S0012365X97830798?via%3Dihub вычислимость доказывается, когда класс графа задается грамматикой HR.