Предположим, что NP = co-NP, а полином ограничивает длину доказательства неудовлетворенности для экземпляра 3-CNF x . Тогда есть ли какие-либо результаты о том, в какой форме может быть получено любое доказательство неудовлетворенности для x длины ≤ p ( x ) ?
Т.е. в целом, должно ли такое доказательство использовать, например, всю мощь логики второго порядка над бесконечными структурами (я знаю, что предложение доказать - неудовлетворительная формула может быть выражено в логике второго порядка над конечные структуры, но промежуточные шаги в доказательстве, чтобы добраться до этого, могут потребовать рассуждений по бесконечным структурам)
Поскольку не существует эффективной, полной и надежной системы логического вывода для логики второго порядка, можно ли будет использовать такой результат для доказательства NP co-NP?
11
Ответы:
Если существует оптимальная pps (pps = система пропозициональных доказательств , оптимальная pps - это pps, которая может p-симулировать любую другую систему доказательств), то pps EF (Extended Frege) усилена пропозициональными аксиомами, утверждающими обоснованность оптимальной системы пропозициональных доказательств. будет оптимальным. В более общем смысле EF + обоснованность pps P может p-моделировать P для любого P. Таким образом, EF имеет своего рода общность: вам не нужно менять логику или базовую структуру pps, а просто добавить аксиомы высказываний, чтобы получить любую произвольные сильные pps.
В целом, нет необходимости выходить за пределы логики высказываний.
источник