Если P = NP, можем ли мы получить доказательства гипотезы Гольдбаха и т. Д.?

Это наивный вопрос, из моего опыта; заранее извиняюсь.

Гипотеза Гольдбаха и многие другие нерешенные вопросы математики могут быть записаны в виде кратких формул в исчислении предикатов. Например, статья Кука "Могут ли компьютеры регулярно находить математические доказательства?" формулирует эту гипотезу как

\forall n [(n > 2 \land 2 | n) \supset \exists r \exists s (P (r) \land P (s) \land n = r + s)]

$\forall n [( n > 2 \wedge 2 | n) \supset \exists r \exists s (P(r) \wedge P(s) \wedge n = r + s) ]$

Если мы ограничим внимание полиномиально длинными доказательствами, то теоремы с такими доказательствами находятся в NP. Поэтому, если P = NP, мы могли бы определить, является ли, например, гипотеза Гольдбаха истинной в полиномиальное время.

Мой вопрос таков: сможем ли мы показать доказательство за полиномиальное время?

Редактировать . Согласно комментариям Питера Шора и Каве, я должен был квалифицировать свое утверждение, что мы могли бы определить, верна ли гипотеза Гольдбаха, если это действительно одна из теорем с коротким доказательством. Что, конечно, мы не знаем!

cc.complexity-theory proof-complexity automated-theorem-proving proof-search Джозеф О'Рурк
источник

Во-первых, чтобы представить краткое (<1000 страниц?) Доказательство гипотезы Гольдбаха, должно быть краткое доказательство. P = NP не имеет к этому никакого отношения.

Питер Шор

@Suresh, @Kaveh: Вы, кажется, ошибаетесь. Здесь у нас есть конкретный пример проблемы поиска NP. Уместным здесь является квантификатор - это существование доказательства (в подходящей формальной системе) теоремы.

Кристофер Арнсфельт Хансен

Другое замечание заключается в том, что на самом деле мы можем записать алгоритм, который, если P = NP, найдет доказательство для данного утверждения, если оно существует за многочлен времени по длине оператора и длине кратчайшего доказательства. (этот многочлен является границей, которая выполняется для всех теорем), однако это будет «астрономический» алгоритм.

Кристофер Арнсфельт Хансен

@Joe: нет, я могу написать алгоритм прямо сейчас! (Даже не зная, если P = NP). Идея состоит в том, что известно как Универсальный поиск Левина.

Кристоффер Арнсфельт Хансен

@Kristoffer: Круто! Не знал о ЛС. Я вижу, что у Маркуса Хаттера есть своего рода улучшение в LS: «Самый быстрый и самый короткий алгоритм для всех четко определенных задач». Международный журнал основ компьютерных наук, 13 (3): 431-443, 2002.

Джозеф О'Рурк

Ответы:

Верно!

Если P = NP, мы не только можем решить, существует ли доказательство длины n для гипотезы Гольдбаха (или любого другого математического утверждения), но мы также можем найти его эффективно!

Зачем? Потому что мы можем спросить: есть ли доказательство, обусловленное первым битным существом ..., тогда, есть ли доказательство, обусловленное первым двоичным существом ..., и так далее ...

А как ты узнал? Вы просто попробуете все возможности в порядке возрастания. Когда мы делаем шаг в i-й возможности, мы также пытаемся сделать шаг в каждой из возможностей 1 .. (i-1).

Дана Мошковиц
источник

Разве это не универсальный алгоритм поиска Левина?

Мухаммед Аль-Туркистани

@turkistany: да, это так!

Дана Мошковиц

Дана ответила на вопрос. Но вот некоторые комментарии с практической стороны.

Обратите внимание, что неразрешимо проверить, доказуемо ли данное предложение в ZFC. не имеет для этого никакого значения. (фактически ) означает, что легко найти доказательства для высказывательных тавтологий , а не предложений первого порядка, таких как GC. $P=NP$ $P=NP$ $P=coNP$

Это чтобы проверить, есть ли доказательство данного предложения данной длины (в унарном виде) в фиксированной теории (например, ZFC). Так что, если , то есть алгоритм polytime, чтобы проверить это. Принятие как некоторого фиксированного многочлена в длине предложения приведет к алгоритму polytime. $NP$ $l$ $P=NP$ $l$

Практически (это упоминается Годелем в его знаменитом письме фон Нейману): если , то существует алгоритм с полиномиальным временем, который дает предложение первого порядка и (в унарном), алгоритм может найти, если предложение имеет размер доказательство в ZFC. Идея Годеля заключалась в том, что в этом случае, если эквивалентность действительно выполнима (т. Е. Алгоритм - это не просто а, скажем, $P=NP$ $l$ $l$ $P=NP$ $P$ $DTime(n^2)$ ), тогда можно взять этот алгоритм и запустить его, чтобы проверить доказательства возможной, но очень большой длины, которая будет больше, чем любое доказательство, которое когда-либо сможет придумать любой человек, и если алгоритм не находит ответа, то Приговор практически невозможно доказать. Уловка, о которой упоминала Дана, также сработает, чтобы найти доказательство.

Для практических средств:

$P=NP$ $DTime(10000n^{10000})$
оно найдет доказательство только в том случае, если оно есть (то есть предложение не является неразрешимым предложением в ZFC), более того, доказательство должно быть практически коротким.
$P\neq NP$ $NP=DTime(n^{\log^* n})$

Кава
источник

Ваш пункт 1. слишком пессимистичен. DTIME

(n^{10})

$(n^{10})$ тоже не поможет!

Ануш