NP≠P. Док-во от противного-контрпример алгоритмов из NP

[dmitgu]

Теорема дедукции

В своем доказательстве я буду использовать теорему дедукции. Скажу как и для чего её применяют, а затем докажу. В логике часто используют такую схему вывода:
Шаг 1. Гипотеза: $C$
.... всякие логические выводы на основе правила вывода $MP$ (когда из истинных $(A \to B)$ и $A$ делают вывод об истинности $B$) и используя $C$ как истину...
Шаг N. Результат вывода из гипотезы $C$: $A$
Шаг N+1. Результат вывода без всякой гипотезы $C$: $(C \to A)$
Вот такая методика. Она основана на том, что на каждом шаге вывода есть некая текущая промежуточная формула $X$. И на каждом шаге эту промежуточную формулу можно заменить на истинную формулу $(C \to X)$. И уже без всякой гипотезы. Тогда Шаг N действительно превратиться в Шаг N+1, а Шаг 1 превратиться в тавтологию $(C \to C)$.
Как сделать такой переход, если используем только правило вывода $MP$? Достаточно разобрать один пример, чтоб понять. Пусть есть такой вывод пункта 3 из пунктов 1 и 2 по правилу $MP$:
1. Выведено раньше: $A \to B$
2. Выведено раньше: $A$
3. Из пп. 1 и 2 получим: $B$
А нужно заменить это на следующее:
1. Выведено раньше: $C \to (A \to B)$
2. Выведено раньше: $C \to A$
3. Из пп. 1 и 2 получим: $C \to B$
Но такую последовательность надо дополнить промежуточными шагами, чтобы использовать только правило вывода $MP$ и аксиомы теории. Для этого подойдет тавтология:
$C \to (A \to B) \to [ (C \to A) \to (C \to B) ]$
Тогда по правилу $MP$ в этой тавтологии убирается начало, совпадающее с п.1, затем начало от остатка, совпадающее с п.2 и остается то, что в п.3. Иногда данную тавтологию делают одной из аксиом логики (для удобства доказательства теоремы дедукции, видимо), впрочем, она не наглядна в качестве исходного истинного утверждения.
Поэтому там, где я буду использовать теорему дедукции – можно написать и «механический» вывод из истинных утверждений при помощи $MP$ без всяких гипотез. Кто хочет – может это легко проделать, но тут для краткости я будут использоваться теорему дедукции.

Нужная тавтология

Еще я буду использовать тавтологию $(X1 \to Y) \to [ (X2 \to Y) \to ( (X1 \vee X2) \to Y ) ]$. Разумеется, ее можно вывести из аксиом логики (из аксиом логики по теореме о полноте можно вывести любую тавтологию), но просто покажу, что это тавтология:
1. Раскроем данное утверждение, заменяя импликацию $(A \to B)$ на эквивалентную ей дизъюнкцию $(\neg A \vee B)$:
$\neg (\neg X1 \vee Y) \vee [ \neg (\neg X2 \vee Y) \vee ( \neg (X1 \vee X2) \vee Y ) ]$
2. Заменим $\neg (A \vee B)$ на эквивалентное утверждение $(\neg A \wedge \neg B)$, а $(\neg \neg A)$ на $(A)$ и уберем лишние скобки для ассоциативной операции $\vee$:
$(X1 \wedge \neg Y) \vee (X2 \wedge \neg Y) \vee (\neg X1 \wedge \neg X2) \vee Y$
3. Воспользуемся дистрибутивностью операции $\wedge$:
$((X1 \vee X2) \wedge \neg Y) \vee (\neg X1 \wedge \neg X2) \vee Y$
В результате мы получили утверждение, эквивалентное исходному утверждению. Оно истинное, если истинно $Y$ в силу последнего члена дизъюнкции $Y$. А если $Y$ ложное, то утверждение будет истинным при истинности любого из $X1$, $X2$ – в силу первого члена дизъюнкции $((X1 \vee X2) \wedge\neg Y)$. Но если и они ложные – то выражение все равно истинное в силу среднего члена дизъюнкции $(\neg X1 \wedge \neg X2)$. Поэтому – это тавтология.

Лемма о диагонализации

В доказательстве теоремы $NP \ne P$ будет использована возможность подставлять в алгоритм $A(x)$ текст самого алгоритма.
Чтоб отличить в формулах алгоритмы от их текстов, буду обозначать текст алгоритма чертой над обозначением алгоритма. Вот так, например: $\overline{\operatorname{AntiMt}()}$
Очевидно, что всегда можно сделать алгоритм $AA$, который сначала выписывает текст алгоритма $A(x)$, а затем запускает алгоритм $A(x)$ с этим текстом в качестве аргумента. Так вот, у этого алгоритма $AA$ тоже есть текст его «программы», и этот текст может быть получен из текста алгоритма $A$ по некоторому алгоритму $\operatorname{diag}(\overline{A(x)})$. Это довольно очевидно и такая возможность берется за исходную посылку. То есть - нам нужны достаточно выразительные теории, которые способны представлять алгоритмы и тогда алгоритм $\operatorname{diag}()$ - будет среди них.
В теории алгоритмов для аналогичных целей используется теорема о неподвижной точке, но там нумерация алгоритмов сплошная и неполиномиальная поэтому, а нам нужна нумерация в духе «тексты алгоритмов». Да, не все тексты будут текстами алгоритмов, но этот случай нас не пугает - тогда такие «алгоритмы» ничего не возвращают и это можно понять.
Поэтому за основу возьмем Лемму о диагонализации из книги «Вычислимость и логика» Дж. Булос, Р. Джеффри. Только там она для предиката доказана, а мы докажем ее для алгоритма. В остальном я практически переписываю доказательство. И еще один момент - там доказательство на основе «представлений», а я оперирую с алгоритмами - логика та же, просто через представления возникает дополнительный «этаж» манипуляций, но мы просто можем считать, что наша теория более выразительная, чем теория Пеано и можно оперировать прямо со свойствами алгоритмов.
Лемма о диагонализации. Для произвольного алгоритма $B$ найдется алгоритм $G$, такой что $G = B(\overline{G})$.
Доказательство.
Назовем алгоритмом $G()$ тот алгоритм, который выполняет расчет как $B(\operatorname{diag}(\overline{B(\operatorname{diag}(x))}))$. Собственно, $G()$ отличается от $B(\operatorname{diag}(\overline{B(\operatorname{diag}(x))}))$ только тем, что алгоритм $G$ сначала выписывает аргумент $\overline{B(\operatorname{diag}(x))}$, а затем запускает композицию функций $B(\operatorname{diag}(\ldots))$ с этим аргументом. И - текст этого алгоритма $G$ получается вот так: $\operatorname{diag}(\overline{B(\operatorname{diag}(x))})$. Ведь алгоритм $\operatorname{diag}()$ построен именно так, чтоб возвращать текст подобных алгоритмов.
1. По свойствам $\operatorname{diag}()$: $\overline{G()} = \operatorname{diag}(\overline{B(\operatorname{diag}(x))})$
2. По построению $G()$: $G() = B(\operatorname{diag}(\overline{B(\operatorname{diag}(x))}))$
3. Из п. 1 подстановкой частей равенства в $B()$: $B (\overline{G()}) = B(\operatorname{diag}(\overline{B(\operatorname{diag}(x))}))$
4. Из пп. 2 и 3: $B(\overline{G()}) = G()$
Лемма доказана.
Вот так мы переписали доказательство для предикатов в доказательство для алгоритмов. И вся разница между предикатом и алгоритмом в том - что вместо значка эквивалентности в последнем предложении стоит знак равенства. Но по сути тут огромное отличие. Ведь алгоритм выдает при одних и тех же аргументах один и тот же результат - и если он не останавливается, то он нигде не останавливается. И ни от какой теории это не зависит. И поэтому можно построить «Универсальный алгоритм», который полностью моделирует поведение алгоритма-аргумента (точнее, алгоритма, чей текст передан в качестве аргумента).
А вот у предиката нет возможности «не останавливаться» - у него нет своей «самостоятельной жизни» вне теории. Поэтому с предикатами нет возможности построить универсальный предикат, который получал бы текст другого предиката и был точно таким же истинным или ложным как он:
Ведь универсальный предикат при помощи отрицания становится универсальным анти-предикатом, который всегда возвращал бы противоположное, чем предикат-аргумент (точнее, предикат, чей текст получен в качестве аргумента). А это невозможно, потому что по лемме о диагонализации найдется эквивалентный предикат для данного анти-предиката. Значит, универсальный анти-предикат невозможен, значит, невозможен и универсальный предикат.
В ходе доказательства теоремы $NP \ne P$ мы увидим, как это различие между предикатами и алгоритмами выльется в существенное отличие получившейся неполноты от конструкции теорем Гёделя.

Постановка задачи

Рассмотрим следующую задачу из класса $NP$, сформулированную в 2-ух пунктах:
1. Имеется некоторая непротиворечивая (важно!) система аксиом $Aks$. В качестве слов будем рассматривать $A()$ – записанные на языке теории алгоритмы. В качестве слова-свидетеля будем рассматривать текст доказательства для $A() = i$. Где i – некоторое число (можно считать, что число записано в десятичном представлении, но это не принципиально). Если имеется слово $x$ и слово-свидетель $y$, то, как известно из логики, можно при помощи алгоритма автоматической проверки доказательств $R(Aks, x, y)$ за полиномиальное время (число шагов) $Py(|y|+|Aks|)$ от размеров $y$ и $Aks$ проверить, доказывает ли $y$ какое-то равенство $A() = i$ для $x$ на базе аксиом $Aks$. На размер $y$ накладывается стандартное для NP ограничение некоторым полиномом $Px(|x|)$. Разумеется, если в качестве $x$ и/или $y$ выступает какой-то бессмысленный текст, то $R(Aks, x, y)$ возвращает «ложь».
Размеры всех упомянутых полиномов считаем достаточно большими для наших целей - по контексту будет видно, что это легко достижимо.
2. Если система аксиом $Aks$ противоречива или это какой-то бессмысленный текст, то в качестве $R(Aks, x, y)$ выбран предикат, который всегда выдает «ложь» и явно быстрее, чем $Py(|y|+|Aks|)$.

Берем нашу задачу из пунктов 1 и 2. Берем метод поиска слов-свидетелей $y$, подходящих для заданного слова $x$ (то есть, $|y| < Px(|x|)$ и $R(Aks, x, y)$ дает истину). Назовем наш метод поиска слов-свидетелей для слова $x$ - алгоритмом $\operatorname{Mt}(Aks, x)$.
Есть мнение, что всегда есть метод поиска, который всегда находит нужное слово-свидетель, если оно вообще есть. Это - прямой перебор всех $y$, таких что $|y| < Px(|x|)$. Это мнение ошибочно, как мы увидим, в силу пункта 2 нашей задачи. А если бы было верно $NP = P$, то у нас был бы алгоритм поиска, который находил бы слово-свидетель (если оно есть) за полиномиальное время. Но мы докажем, что любой метод будет неполон - если он корректен, поэтому насчет полиномиальности скорости поиска мы даже не будем думать, главное, чтоб алгоритм поиска завершал свою работу в пределах заранее известного (от размера заданного слова и аксиом) времени.

Для простоты считаем, что $\operatorname{Mt}(Aks, x)$ выдает не текст доказательства (слово-свидетель), а результат этого доказательства (число$ i$в некотором представлении) как прогноз результата работы алгоритма $A()$. Напомню, что текст некоторого алгоритма $A()$ подставлен на место переменной $x$, когда решается вопрос про результат работы этого алгоритма.
Наше упрощение (результат вместо доказательства) вполне уместно, потому что мы будем опровергать полноту, а полный метод обнаружения доказательств давал бы возможность и для полного метода обнаружения результатов (для которых есть подходящее доказательство). Поэтому если нет полного метода для результата, то нет полного метода и для доказательств.

Если же нужного доказательства среди подходящих по размеру доказательств найти не удалось, то $\operatorname{Mt}(Aks, x)$ возвращает $knockout$. Ясно, что результаты $\operatorname{Mt}$ не прямо равны результатам $A()$ - просто потому, что результаты могут быть какие угодно, а нам надо еще занять место для $knockout$, который ведь тоже может выдаваться какими-то алгоритмами. Есть разные способы ставить значения в соответствие друг другу, например - канторова пара из признака 1 и результата работы $A()$, либо просто $0$ и $0$ - для $knockout$.

Просто введем следующее обозначение для соответствия результатов самих алгоритмов и результатов прогнозов для них от $\operatorname{Mt}$:
Если $A() = i$, и $\operatorname{Mt}(Aks, \overline{A()})$ выдает правильный прогноз, то $\operatorname{Mt}(Aks, \overline{A()}) = \operatorname{FormatMt}(i)$.
Разумеется, $\operatorname{FormatMt}(i)$ обратим - то есть, по нему можно узнать $i$. И $\operatorname{FormatMt}(i)$ никогда не возвращает $knockout$.

Теперь сформулируем частичное условие корректности для $\operatorname{Mt}(Aks, x)$ при $x = \overline{A()}$:

\begin{multline*} \operatorname{Check100Mt}(Aks, \overline{A()}) \to \\ \to ( [ \operatorname{Mt}(Aks, \overline{A()}) = \operatorname{FormatMt}(A()) ] \vee [ \operatorname{Mt}(Aks, \overline{A()}) = knockout ] ) \end{multline*}

Сначала рассмотрим заключение в данной импликации:

\begin{multline*} [ \operatorname{Mt}(Aks, \overline{A()}) = \operatorname{FormatMt}(A()) ] \vee [ \operatorname{Mt}(Aks, \overline{A()}) = knockout ] \end{multline*}

Очень важно, что $\operatorname{FormatMt}(A())$ не зависит от аксиом, хотя $\operatorname{Mt}$ зависит. И мы можем написать это равенство благодаря п.2 нашей задачи. Потому что если заданные аксиомы выдают абсурдные выводы про работы алгоритмов, то это противоречие и эти выводы не имеют значения и в силе будет $(\operatorname{Mt}(Aks, \overline{A()}) = knockout)$. Противоречие возникнет из-за 2х разных выводов про результат работы $A()$ - эталонного (который отражают теоремы Пеано без расширений, например) и ложного.
Но проблема в том, что алгоритм $A()$ может ведь и не остановится. И не будет эталона для сравнения. И в таких случаях есть угроза, что теория содержит непротиворечивую, хоть и абсурдную аксиому, что где-то в бесконечности алгоритм все же что-то вернет. Чтобы избежать таких накладок, мы будем рассматривать только алгоритмы с остановкой. И для этого у нас в частичной корректности есть посылка импликации:

$\operatorname{Check100Mt}(Aks, \overline{A()})$

Это такой алгоритм, который проверяет, что разбираемый алгоритм $A()$ делает меньше шагов, чем 100-кратное количество шагов работы у алгоритма $\operatorname{Mt}(Aks, \overline{A()})$. Технически это можно сделать последовательным исполнением того и другого по одному шагу. И если $\operatorname{Mt}(Aks, \overline{A()})$ отработал 100 раз, а $A()$ еще не закончил работу, то мы не можем пользоваться нашей частичной корректностью. Но зато когда можем - то мы уверены, что можем использовать для проверки $\operatorname{FormatMt}(A())$ - который независим от аксиом.
Утверждение частичной корректности можно переписать с использованием универсального алгоритма $U(x)$, который исполняет любой алгоритм по его тексту и возвращает результат (если остановится) в формате $\operatorname{FormatMt}(i)$. Если текст абсурден - то возвращает $knockout$. Как известно, универсальный алгоритм $U(x)$ существует и его легко построить - в отличие от универсального предиката. О чем уже было сказано в разделе «Лемма о диагонализации». Тогда мы могли бы вместо $\overline{A()}$ поставить $x$ и квантор общности, но нам частичная корректность потребуется только для одного алгоритма, поэтому сойдёт и так.

И, разумеется, время (количество шагов ) работы $\operatorname{Mt}(Aks, x)$ конечно и ограничено некоторым всюду определённым алгоритмом $\operatorname{T}(|Aks| + |x|)$.
То, что сформулировано про корректность - сформулировано «со стороны». Мы как бы рассматриваем $\operatorname{Mt}(Aks, x)$ в какой-то непротиворечивой теории, притом аксиомы этой теории не обязательно равны аксиомам $Aks$. И принцип корректности, кстати, распространяется и на противоречивые теории - в соответствии с пунктом 2. А противоречивую теорию можно рассмотреть только с точки зрения непротиворечивой.
Существует ли хоть одна корректная $\operatorname{Mt}$? Да - которая всегда возвращает knockout, например.

План доказательства такой:

Сначала мы изучаем свойства $\operatorname{Mt}(Aks, x)$ «со стороны» (всегда есть непротиворечивая теория, соответствующая арифметике в стандартной интерпретации , в которой можно изучить $\operatorname{Mt}(Aks, x)$ - с заданным в ней $Aks$), затем мы делаем выводы о поведении $\operatorname{Mt}(Aks, x)$ в целом - при любых $Aks$, на основании этого выписываем истинное в стандартной интерпретации арифметики свойство, берем его в качестве аксиомы, расширяем им непротиворечивую теорию. Теория остается при этом непротиворечивой, а затем в этой теории доказываем неполноту $\operatorname{Mt}(Aks, x)$. Перейдем к реализации этого плана.

(Тексты логических выводов перепишу в формулы $\LaTeX$ и выложу сегодня-завтра. Да и большой текст сразу выложить невозможно даже кусками - форум не дает)

[Xaositect]

dmitgu в сообщении #956171 писал(а):

Рассмотрим следующую задачу из класса $NP$, сформулированную в 2-ух пунктах:
1. Имеется некоторая непротиворечивая (важно!) система аксиом $Aks$. В качестве слов будем рассматривать $A()$ – записанные на языке теории алгоритмы. В качестве слова-свидетеля будем рассматривать текст доказательства для $A() = i$. Где i – некоторое число (можно считать, что число записано в десятичном представлении, но это не принципиально). Если имеется слово $x$ и слово-свидетель $y$, то, как известно из логики, можно при помощи алгоритма автоматической проверки доказательств $R(Aks, x, y)$ за полиномиальное время (число шагов) $Py(|y|+|Aks|)$ от размеров $y$ и $Aks$ проверить, доказывает ли $y$ какое-то равенство $A() = i$ для $x$ на базе аксиом $Aks$. На размер $y$ накладывается стандартное для NP ограничение некоторым полиномом $Px(|x|)$. Разумеется, если в качестве $x$ и/или $y$ выступает какой-то бессмысленный текст, то $R(Aks, x, y)$ возвращает «ложь».
Размеры всех упомянутых полиномов считаем достаточно большими для наших целей - по контексту будет видно, что это легко достижимо.
2. Если система аксиом $Aks$ противоречива или это какой-то бессмысленный текст, то в качестве $R(Aks, x, y)$ выбран предикат, который всегда выдает «ложь» и явно быстрее, чем $Py(|y|+|Aks|)$.

Так дело не пойдет.

Для того, чтобы задать задачу распознавания и показать, что она принадлежит $\mathrm{NP}$, надо сделать следующее:
1) выбрать некоторый алфавит $A$, на котором задается вход задачи
2) определить язык $L\subset A^*$, который содержит те входы, которые удовлетворяют условию задачи.
3) Доказать, что язык удовлетворяет определению $\mathrm{NP}$: указать многочлен $q(n)$ (ограничение длины сертификата) и алгоритм проверки $V$, который должен удовлетворять условию $x\in L \Leftrightarrow \exists y: |y| < p(|x|) \& V(x, y) = 1$.
4) Доказать полиномиальность времени выполнения алгоритма проверки (формально, относительно длины входа $|x| + |y|$, но раз $|y|$ полиномально зависит от $|x|$, можно доказывать полиномиальность по $|x|$)

У Вас я вижу только алгоритм проверки, но не вижу исходного языка, которому он соответствует.

dmitgu в сообщении #954742 писал(а):

Лемма о диагонализации. Для произвольного алгоритма $B$ найдется алгоритм $G$, такой что $G = B(\overline{G})$.

Тут поподробнее. Равенство - это текстовое равенство алгоритмов, или равенство реализуемых ими функций? Алгоритмы предполагаются принимающими 1 слово на вход?

[dmitgu]

Xaositect в сообщении #956239 писал(а):

1) выбрать некоторый алфавит $A$, на котором задается вход задачи
2) определить язык $L\subset A^*$, который содержит те входы, которые удовлетворяют условию задачи.
3) Доказать, что язык удовлетворяет определению $\mathrm{NP}$: указать многочлен $q(n)$ (ограничение длины сертификата) и алгоритм проверки $V$, который должен удовлетворять условию $x\in L \Leftrightarrow \exists y: |y| < p(|x|) \& V(x, y) = 1$.
4) Доказать полиномиальность времени выполнения алгоритма проверки (формально, относительно длины входа $|x| + |y|$, но раз $|y|$ полиномально зависит от $|x|$, можно доказывать полиномиальность по $|x|$)

1. Запись обобщенных рекурсивных функций в логике
2. Что такое входы?
3. Проверка доказательств по их текстам. Там же есть правила вывода и каждый пункт следует из аксиом или предыдущих пунктов
4. Эта проверка полиномиальна. Это операции с текстами. Все это использовалось еще при доказательстве т. Гёделя, но там они номера писали как произведения простых числе. А позже стали использовать аналоги текстов - так проще. Поиск нужного пункта в тексте логического вывода, второго, сравнение с результатом вывода из них. Блуждание по тексту логического вывода ну от силы куб операций от его размера. Чуть сложнее сортировки "пузырьком". А пример - я как раз дам вывод такого рода в доказательства (который я ещё на язык $LaTeX$ не перевел).

Xaositect в сообщении #956239 писал(а):

Тут поподробнее. Равенство - это текстовое равенство алгоритмов, или равенство реализуемых ими функций? Алгоритмы предполагаются принимающими 1 слово на вход?

Нет, текст - это у меня черта сверху. А тут именно равенство результатов работы алгоритмов. И $B()$ зависит от одного переменного, а G не зависит.

А вот про распознование - это я думаю парадокс и ошибка в теории алгоритмов. В моем случае полином есть - только для каждой отдельной задачи это может потребовать специальных усилий определить - пункт 1 там или 2. Я об этом писал в эвристическом доказательстве
post954742.html#p954742
которое перед нынешним техническим. Собственно по теническому я еще только задачу и план доказательства тут запостил.

[Xaositect]

dmitgu в сообщении #956247 писал(а):

1. Запись обобщенных рекурсивных функций в логике
2. Что такое входы?

Ну, задача распознавания (в частности, любая задача из класса $\mathrm{NP}$) - это задача вида "принадлежит ли заданная строка языку $L$". Вообще, говорят не о "задачах", а о языках. Например, $\mathrm{SAT}$ (выполнимость КНФ) задается в алфавите $x, 0, 1, \vee, (, )$, языку $\mathrm{SAT}$ принадлежат строки, являющиеся корректными КНФ на переменных $x0, x1, x00, x01, x10, x11, \dots$, для которых существуют значения переменных, обращающие КНФ в 1. Вот в вашем случае строки в каком алфавите рассматриваются и какие из них "правильные"?

[dmitgu]

Xaositect в сообщении #956259 писал(а):

Например, $\mathrm{SAT}$ (выполнимость ДНФ) задается в алфавите $x, 0, 1, \vee, (, )$, языку $\mathrm{SAT}$ принадлежат строки, являющиеся корректными ДНФ на переменных $x0, x1, x00, x01, x10, x11, \dots$, для которых существуют значения переменных, обращающие ДНФ в 1. Вот в вашем случае строки в каком алфавите рассматриваются и какие из них "правильные"?

Тут есть определенный произвол в выборе выразительных средств. В принципе за текст можно взять программу на примитивном "бейсике" для программирования машины Тьюринга. И есть способ пределить, является этот текст программой для машины Тьюринга или нет. Так же как в аксиоматике Пеано можно представлять алгоритмы через предикаты. И опять же есть способ понять - рекурсивная (обобщенно) функция тут написана или нет. Разумеется, это не тривиальные алгоритмы типа как в ДНФ. Но это все делалось в логике - там же с этим оперируют.

[Xaositect]

Хорошо, будем считать, что у нас есть некоторый алфавит для записи алгоритмов и некоторый способ определить, является ли строка в этом алфавите корректной записью алгоритма или нет. Это можно сделать даже за полиномиальное время. Также будем считать, что есть универсальная машина, то есть по записи алгоритма и некоторой строке мы можем получить результат работы алгоритма на этой строке, если он на ней останавливается. Причем если время работы алгоритма на заданном входе было полиномиальным, то и время работы универсальной машины будет полиномиальным (от общей длины входа).

Теперь, какие записи алгоритмов будут принадлежать нашему языку, а какие не будут?

[dmitgu]

Xaositect в сообщении #956276 писал(а):

Теперь, какие записи алгоритмов будут принадлежать нашему языку, а какие не будут?

Слово-свидетель (столько вариантов этого термина - сертификат ещё) - это текст доказательства. Вывод. Опять же есть проверка - текст ли это вывода или бессмыслица. И проверяем коректность. Он опирается на аксиомы Aks и в конце должен иметь результат вывод $A()=i$, где $A()$ совпадает с проверяемым словом. Размер доказательства должен соответствовать, правила вывода исполнены и тогда у нас слово подтвердилось и мы даже узнали, чему равен результат этого "слова" (алгоритма).

[Xaositect]

Аксиомы, насколько я понимаю, мы можем менять? То есть у нас есть некоторая базовая система (PA?) и мы к ней можем добавлять произвольные наборы?
То есть язык состоит из пар (список аксиом, запись алгоритма), для которых есть доказательство остановки заданного алгоритма в базовой системе аксиом из заданного списка аксиом, причем оно имеет полиномиальную длину относительно общей длины входа.
Я согласен, что этот язык принадлежат $\mathrm{NP}$, при оговорках на то, что мы должны определить, как именно задаются наши системы аксиом и что такое доказательство остановки. Если это будет важно, я попрошу Вас это сделать.

[dmitgu]

Ок.

-- 04.01.2015, 18:32 --

Завершаю техническое доказательство, начатое зхдесь: post956171.html#p956171
(некоторые интересные замечания есть в предварительном эвристическом варианте post954742.html#p954742 и не вошли в данный)
Доказательство «со стороны»

Как было намечено планом доказательства в предыдущем разделе, рассмотрим свойства алгоритма $\operatorname{Mt}(Aks, x)$ силами некой непротиворечивой теории-обоснования. Ее аксиомы не обязательно совпадают с $Aks$, но соответствуют стандартной модели арифметики. Тогда выводы, сделанные про работу алгоритма $\operatorname{Mt}(Aks, x)$ будут верны независимо от теории.

Для начала построим алгоритм $\operatorname{AntiMt}()$, который будет «обманывать» $\operatorname{Mt}(Aks, x)$. Идея в том, что $\operatorname{AntiMt}()$ запускает внутри себя копию $\operatorname{Mt}(Aks, x)$, передав в качестве $x$ свой собственный текст и выдает противоположное тому, что получит от своей копии $\operatorname{Mt}(Aks, x)$. Тогда $\operatorname{Mt}(Aks, x)$ не сможет прогнозировать результат $\operatorname{AntiMt}()$.
$\operatorname{AntiMt}$ - это алгоритм, текст которого можно получить так: $\operatorname{diag}(\overline{Anti(\operatorname{Mt}(Aks, x))}), где Anti(x)$ преобразует результат в $0$, если аргумент отличается от $\operatorname{FormatMt}(0)$, и в $1$, если аргумент совпадает с $\operatorname{FormatMt}(0)$. Сделано так, чтоб выдать противоположное, чем об этом мог бы «сказать» $\operatorname{Mt}$.

По лемме о диагонализации имеем: $Anti(\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})) = \operatorname{AntiMt}()$.

Очевидно, что построенный $\operatorname{AntiMt}()$ удовлетворяет посылке $\operatorname{Check100Mt}(Aks, \overline{\operatorname{AntiMt}()})$ в частичной корректности и частичную корректность можно переписать так (исключив посылку по правилу вывода $MP$):

$[ \operatorname{Mt}(Aks, \overline{A()}) = \operatorname{FormatMt}(A()) ] \vee [ \operatorname{Mt}(Aks, \overline{A()}) = knockout ]$ или, иначе:
$\neg ( \operatorname{Mt}(Aks, \overline{A()})=\operatorname{FormatMt}(A()) ) \to ( \operatorname{Mt}(Aks, \overline{A()}) =knockout )$ или, то же самое:
$( \operatorname{Mt}(Aks, \overline{A()}) \ne \operatorname{FormatMt}(A()) ) \to ( \operatorname{Mt}(Aks, \overline{A()}) = knockout )$

Теперь можно переходить к выводу утверждений, которые будут использованы в доказательстве неполноты алгоритма $\operatorname{Mt}(z, x)$ на соответствующем ему (по аксиомам $z$) $\operatorname{AntiMt}()$
.
Теорема. $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) = knockout$, в то время как $\operatorname{AntiMt}() = Anti(knockout)$
Доказательство.

1. По построению $\operatorname{AntiMt}()$: $Anti(\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})) = \operatorname{AntiMt}()$.
Это означает, что то, что возвращает $\operatorname{Mt}$ про результат работы $\operatorname{AntiMt}()$ не совпадает с реальным результатом $\operatorname{AntiMt}()$ и, возможно, противоположно (из-за функции $Anti())$ реальному результату. Но это мы аккуратно выведем далее.

2. $\operatorname{FormatMt}(Anti(x)) \ne x$
Ниже будет подробно рассмотрен вывод этого пункта – он длиннее всего остального, хотя само неравенство очевидно – ведь алгоритм $Anti()$ как раз так построен, чтобы из результата работы алгоритма $\operatorname{Mt}$ делать иное значение в смысле формата $\operatorname{Mt}$ – чтобы «оспорить» результат работы $\operatorname{Mt}$, который получил на вход текст алгоритма $\operatorname{AntiMt}$. Поэтому в п.2 я оставил очевидное неравенство без вывода, чтоб не загромождать основной вывод и не снижать его ясность. А чтобы сохранить техническую полноту доказательства, вывод для пункта 3 приведен сразу вслед за текущим (основным) выводом.

3. Из п. 1, применяя $\operatorname{FormatMt}()$ к обеим частям равенства:
$\operatorname{FormatMt}(Anti(\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}))) = \operatorname{FormatMt}(\operatorname{AntiMt}())$

4. Из п.2 - заменив x на $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$ получим:
$\operatorname{FormatMt}(Anti(\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}))) \ne \operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$

5. Из пп. 3, 4 и аксиомы для равенства получим:
$\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) \ne \operatorname{FormatMt}(\operatorname{AntiMt}())$

6. Свойство корректности: $( \operatorname{Mt}(Aks, \overline{A()}) \ne \operatorname{FormatMt}(A()) ) \to ( \operatorname{Mt}(Aks, \overline{A()}) = knockout )$, где $\overline{A()}$ - текст произвольного алгоритма, удовлетворяющего $\operatorname{Check100Mt}(Aks, \overline{A()})$.

7. Из п. 6 подстановкой $\overline{\operatorname{AntiMt}()}$ (она удовлетворяет $\operatorname{Check100Mt}(Aks, \overline{ AntiMt ()})$, как было отмечено при ее построении) вместо $\overline{A()}$ получим:

$( \operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) \ne \operatorname{FormatMt}(\operatorname{AntiMt}()) ) \to ( \operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) = knockout )$

8. Из пп.5 и 7 по правилу вывода $MP$: $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) = knockout$

9. Из п.8, применяя к обеим сторонам равенства $Anti()$ получим:
$Anti(\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})) = Anti(knockout)$

10. Из пп.1 и 9 получим: $\operatorname{AntiMt}() = Anti(knockout)$

С учетом того, что алгоритм $Anti()$ является крайне примитивным и быстрым, результат $Anti(knockout)$ вычисляется моментально. А это значит, что в рассматриваемой теории-обосновании доказано, что в результате своей работы алгоритм $\operatorname{AntiMt}()$ даст результат $Anti(knockout)$, о чем заведомо не в состоянии сообщить алгоритм $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$, так как он в данном случае в соответствии с п.8 выдает результат $knockout$ (который не может соответствовать никакому значению).

Теперь – обещанный вывод неравенства $( \operatorname{FormatMt}(Anti(X)) \ne X )$ из п. 2. Вывод – из свойств $Anti()$ и свойств результатов, которые выдает алгоритм $\operatorname{Mt}$. Эти свойства сформулированы в первых трех пунктах вывода:

2a. Свойство алгоритма $Anti()$: $( x \ne \operatorname{FormatMt}(0) ) \to ( Anti(x) = 0 )$
2b. Свойство алгоритма Anti(): $( x = \operatorname{FormatMt}(0) ) \to ( Anti(x) = 1 )$
2c. Свойство обратимости для $\operatorname{FormatMt}()$: $\operatorname{FormatMt}(0) \ne \operatorname{FormatMt}(1)$
2d. Гипотеза: $x \ne \operatorname{FormatMt}(0)$
2e. Из пп. 2a и 2d по правилу вывода $MP$: $Anti(x) = 0$
2f. Из п. 2e, применяя к обеим сторонам $\operatorname{FormatMt}$: $\operatorname{FormatMt}(Anti(x)) = \operatorname{FormatMt}(0)$
2g. Из пп. 2d, 2f и аксиом равенства: $\operatorname{FormatMt}(Anti(x)) \ne x$
2h. Из пп. 2d, 2g и теоремы дедукции: $( x \ne \operatorname{FormatMt}(0) ) \to ( \operatorname{FormatMt}(Anti(x)) \ne x )$. После этого гипотеза 2d исключена из рассмотрения. В процессе использования гипотезы никакие правила вывода кроме $MP$ не применялись (это упоминание о нюансе в формулировке теоремы дедукции, что упрощает её применение).
2i. Гипотеза: $x = \operatorname{FormatMt}(0)$
2j. Из пп. 2b и 2i по правилу вывода $MP$: $Anti(x) = 1$
2k. Из п. 2j, применяя к обеим сторонам $\operatorname{FormatMt}$: $\operatorname{FormatMt}(Anti(x)) = \operatorname{FormatMt}(1)$
2l. Из пп. 2c, 2i и аксиом равенства: $x \ne \operatorname{FormatMt}(1)$
2m. Из пп. 2k и 2l: $\operatorname{FormatMt}(Anti(x)) \ne x$
2n. Из пп. 2i, 2m и теоремы дедукции: $( x = \operatorname{FormatMt}(0) ) \to ( \operatorname{FormatMt}(Anti(x)) \ne x )$. После этого гипотеза 2i исключена из рассмотрения. В процессе использования гипотезы никакие правила вывода кроме $MP$ не применялись (это упоминание о нюансе в формулировке теоремы дедукции, что упрощает её применение).
2o. Тавтология: $(X1 \to Y) \to [ (X2 \to Y) \to ( (X1 \vee X2) \to Y ) ]$
2p. Если положить, что $X1$ это $[ x \ne \operatorname{FormatMt}(0)]$, $X2$ это $[x = \operatorname{FormatMt}(0)]$, а $Y$ это $[\operatorname{FormatMt}(Anti(x)) \ne x]$, то 2h будет иметь вид $(X1 \to Y)$ и из пп. 2h, 2о по правилу $MP$ получим:
$(X2 \to Y) \to ( (X1 \vee X2) \to Y )$
2r. С теми же обозначениями, что в п. 2p пункт 2n будет иметь вид $(X2 \to Y)$ и из пп. 2n, 2p по правилу $MP$ получим: $( X1 \vee X2) \to Y$
2s. Теперь раскрываем оговоренные в п. 2p обозначения применительно к п. 2r и получаем:
$([x \ne \operatorname{FormatMt}(0)] \vee [x = \operatorname{FormatMt}(0)]) \to [\operatorname{FormatMt}(Anti(x)) \ne x]$
2t. В тавтологию $(X \vee \neg X)$ подставим вместо $X$ выражения $[x = \operatorname{FormatMt}(0)]$ и получим:
$([x \ne \operatorname{FormatMt}(0)] \vee [x = \operatorname{FormatMt}(0)])$
2u. Из пп. 2s, 2t и правила вывода $MP$ получим: $\operatorname{FormatMt}(Anti(x)) \ne x$
Вот мы и получили пункт 2:
2. $\operatorname{FormatMt}(Anti(x)) \ne x$
Теорема доказана.

Завершение доказательства

Теорема. $\operatorname{Mt}(z, x)$ является неполной. То есть, найдется непротиворечивая теория с аксиомами $Aks$, в которой доказан результат работы некоторого алгоритма $A()$ и размер этого доказательства меньше $Px(|\overline{A()}|)$, но алгоритм $\operatorname{Mt}(Aks, \overline{A()})$ возвращает $knockout$.

Доказательство.
Мы выяснили, что $\operatorname{Mt}(х, \overline{\operatorname{AntiMt}()}) = knockout$ истинно всегда (точнее сказать «для достаточно выразительных теорий», для строгости можно рассматривать только расширения теории Пеано). Просто так работает алгоритм. Значит, это утверждение можно добавлять в непротиворечивые теории арифметики и будут получаться непротиворечивые теории арифметики. Берем достаточно выразительную теорию арифметики, добавляем в неё эту аксиому (замечу, что никаких утверждений корректности уже не требуется) и получаем некоторую новую непротиворечивую теорию с аксиомами $Aks$.

А теперь подставим в эту аксиому $\operatorname{Mt}(z, \overline{\operatorname{AntiMt}()}) = knockout$ вместо $z$ эти самые $Aks$.

При подстановке вместо $z$ текстов аксиом $Aks$ получаем $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) = knockout$. Берем пункты 8, 9 и 10 из предыдущего раздела (тут доказательство уже не «со стороны») и получаем доказательство для результата $\operatorname{AntiMt}()$. Правда, в п. 10 есть ссылка на п.1, но это ссылка на свойства диагонализации - которая является общим свойством для всех алгоритмов и доказывается для любого из них в достаточно выразительной теории. И небольшой размер этого доказательства тоже известен (кстати, его тоже можно аксиоматизировать для краткости - тут всё истинно).

Итак, в непротиворечивой теории с аксиомами $Aks$ есть короткое доказательство для результата $\operatorname{AntiMt}()$. Для того результата, который при всей его краткости не может сообщить $\operatorname{Mt}$. Это значит, что задачу из класса $NP$, которая имеет подходящие слово и слово-свидетель, не удается решить силами алгоритма $\operatorname{Mt}$ - если этот алгоритм корректен. А это значит, что $NP \ne P$.
Теорема доказана.

Замечание. Фокус доказательства в том, что фактически мы можем проверить (со стороны!) что вернет $\operatorname{AntiMt}()$ и что вернет $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$. И противоречий не должно возникнуть. И $\operatorname{Mt}$ это «понимает» и «понимает», что если он даст какой-то значимый результат для $\operatorname{AntiMt}()$, то теория получится противоречивой и ему всё равно «придется» выдавать $knockout$. В результате он «не спорит» с аксиомой $\operatorname{Mt}(х, \overline{\operatorname{AntiMt}()}) = knockout$, потому что всё равно «проиграет».

И ещё один интересный момент. При желании, видимо, можно ослабить требования пунктов 1 и 2 в постановке задачи. Ведь в утверждении корректности нам не требуется противоречие через неограниченное количество шагов. Поэтому пункт 1 можно, наверно, ослабить до требования «условной непротиворечивости» - на глубину работы проверяемых $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$ и $\operatorname{AntiMt}()$, а пункт 2 - до уровня грубой противоречивости - которую можно выявить на той же глубине поверки. Однако это внесло бы дополнительную громоздкость в доказательства, а нас же тут интересует сам принцип, а не широта вариантов.

[Xaositect]

Ой.
Нет.
Я ошибся. У Вас в определении написано, что Ваш алгоритм проверки должен узнавать, противоречива ли Ваша система аксиом. Это задача неразрешимая. Вашего алгоритма $R$ не существует.

[dmitgu]

Xaositect в сообщении #956296 писал(а):

ошибся. У Вас в определении написано, что Ваш алгоритм проверки должен узнавать, противоречива ли Ваша система аксиом. Это задача неразрешимая. Вашего алгоритма $R$ не существует.

Конечно нераззрешима! Но алгоритм-то проверки существует. Просто мы не всегда знаем какой. Вот об этом я и писал в эвристическом доказательстве. Это парадокс на мой взгляд и противоречие в теории алгоритмов, когда они ставят в зависимость принадлежность задачи классу NP от того, знают ли они алгоритм проверки. А математические объекты от знаний зависеть не могут. И поэтому из этого противоречия они доходят до приравнивая теорий арифметики примитивным пропозициональным уравнениям.

[Xaositect]

Нет, тут никакого незнания нет. Алгоритма $R$ не существует, потому что я могу свести к нему проблему останова. И значит, Ваш язык не принадлежит классу $NP$, потому что это требовало бы существование алгоритма $R$.

[dmitgu]

Xaositect в сообщении #956356 писал(а):

Нет, тут никакого незнания нет. Алгоритма $R$ не существует, потому что я могу свести к нему проблему останова.

В смысле? Как свести и что из этого следует?

И алгоритм-то существует! И определенный. Потому что каждая теория либо противоречива, либо нет.

[Xaositect]

dmitgu в сообщении #956360 писал(а):

И алгоритм-то существует! И определенный. Потому что каждая теория либо противоречива, либо нет.

Любая машина либо останавливается, либо нет. Но алгоритма решения проблемы останова не существует. Вот и тут то же самое.

[dmitgu]

Xaositect в сообщении #956369 писал(а):

Любая машина либо останавливается, либо нет. Но алгоритма решения проблемы останова не существует. Вот и тут то же самое.

В этом смысле да - так же. Ну и что? Алгоритм проверки не занимается выбором где ему быть. У комивояжера один алгоритм а у ДНФ другой и т.д. Это вопрос формулировки задачи и решения "со стороны" относительно алгоритма. А требование существования алгоритма проверки выполнено. А что что мы не знаем какое именно - так в любом случае это из $NP$