Недоказуемое поведение машины Тьюринга

Да, ваше понимание в основном правильное - это (насколько нам известно) возможный исход. Дело в том, что могут быть модели ZFC, в которых есть "нестандартные" натуральные числа. Эти нестандартные номера соответствуют нестандартным экземплярам SAT, которые алгоритм$\alpha$может не решить, даже если он решает все фактические экземпляры SAT.

Оказывается, нестандартное время работы не проблема - если$\alpha$работает за полиномиальное время$p$, рассмотрим алгоритм$\alpha'$который выполняет$\alpha$для$p$-много шагов, а затем - если он еще не остановился - останавливается и выводит 1 (скажем). Затем$\alpha'$решает все актуальные экземпляры SAT, и даже нестандартно$\alpha'$выполняется за полиномиальное время. Так что проблема действительно в нестандартных экземплярах SAT.

Это аналогично теореме Гёделя о неполноте: даже если не существует фактического натурального числа, кодирующего доказательство$0=1$из аксиом ZFC (надеемся :P) будет модель ZFC, содержащая некоторое нестандартное натуральное число$n$который (как думает модель) кодирует доказательство$0=1$от$ZFC$- то есть "нестандартное доказательство".

Может быть полезно различать различные возможные способы$P = NP$может быть правдой, но недоказуемой правдой. Для того чтобы$P = NP$, должна быть машина Тьюринга$T$который решает SAT за полиномиальное время. Но:

1. Доказать, что он всегда останавливается, может быть невозможно.
2. Возможно, можно доказать, что он всегда останавливается, но невозможно доказать, что он всегда дает правильный результат.
3. Можно было бы доказать, что он всегда останавливается, но невозможно доказать, что он останавливается за полиномиальное время.

Это не должно быть так странно. Многие нерешенные математические проблемы можно сформулировать в терминах вопросов о машине Тьюринга. Например, гипотеза Коллатца верна тогда и только тогда, когда некоторая машина Тьюринга всегда останавливается.

Есть одна возможность, что решение не является конструктивным: например, у вас есть вселенная, в которой ни одна машина Тьюринга не решает SAT за полиномиальное время, и у вас есть другая вселенная, в которой невозможно, чтобы все машины Тьюринга не решали SAT за полиномиальное время. Последнее конструктивно не эквивалентно нахождению машины Тьюринга, которая решает SAT за полиномиальное время; ты так и не нашел.

Это можно немного перефразировать. Теорема Ладнера утверждает, что если$\mathrm{P}\neq \mathrm{NP}$то существует NP-промежуточный язык (язык называется NP-промежуточным, если он находится в$\mathrm{NP}\setminus \mathrm{P}$и не является NP-полным). Поэтому теоретически можно доказать результат независимости следующим образом: построить универсум, в котором не существует NP-промежуточного языка (т.$\mathrm{P}=\mathrm{NP}$), и построить другой, в котором невозможно, чтобы все языки не были NP-промежуточными (поэтому$\mathrm{P}\neq \mathrm{NP}$). Опять же, машина Тьюринга не будет найдена.

(Из ответа Ноя видно, что если есть такое$\alpha$, алгоритм, который решает все реальные экземпляры SAT за полиномиальное время, то мы должны принять$\mathrm{P}=\mathrm{NP}$как истина , независимая от ZFC. Я не уверен, дан ли какой-либо алгоритм$\alpha$, выражение "$\alpha$решает SAT за полиномиальное время"$\Pi_1$(в PA/ZFC) или нет. Если да, то по определенному алгоритму$\alpha$, всякий раз, когда мы знаем, что$\phi:=$"$\alpha$решает SAT за полиномиальное время" не зависит от PA/ZFC, то фактически мы можем заключить, что$\phi$верно , так как PA / ZFC подтверждается$\Sigma_1$-предложения, а если$\neg\phi$были правдой, PA/ZFC доказали бы это.)