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

[mihaild]

dmitgu, тогда явно выпишите, пожалуйста, какие у какого алгоритма на каком множестве ограничение на время работы.

[dmitgu]

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

вопрос о существовании для некоторой вполне конкретной задачи (распознавание языка $\mathrm{SAT}$

Если верна теорема Кука. А она не верна, если надо учитывать вот такое:

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

$p_{\exists}(|S|)$

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

И для такого доказательства надо как-то рассматривать все алгоритмы решения одной задачи и для всех них доказать, что они плохие

Согласен - примерно то же я пытаюсь сделать в своём доказательстве (если там нет ошибок), но я представлял себе немного иной взгляд - такой универсальный алгоритм-решение, который решает любую задачу (каким-то стандартным образом сформулированную) из $NP$. И при таком подходе - вопрос о неразрешимости. Но да - это менее сильный случай. Может нет универсального, но есть частный алгоритм-решение для каждой задачи из NP- как в криптографии с окрытым ключом. Однако, если верен Ваш подход, то верен и мой (он - необходимое условие для Вашего). И в этом смысле я озвучил менее сильное требование, которое тоже имеет место быть. Вроде бы

[Xaositect]

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

Если верна теорема Кука. А она не верна, если надо учитывать вот такое:

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

Я, к сожалению, совершенно не понимаю, о чем Вы говорите со своими $p_{\forall}(|S|, |s|)$ и $p_{\exists}(|S|)$, но раз у Вас теорема Кука ломается, значит, наверное, их не надо учитывать.

[dmitgu]

mihaild в сообщении #1202917 писал(а):

dmitgu, тогда явно выпишите, пожалуйста, какие у какого алгоритма на каком множестве ограничение на время работы.

На самом деле это как раз та задача, которую я строю в своей теореме :) Только в ней есть ещё пара частей у слова. Итого:

$d$, $t$, $S$, $s$

Для множества

$d$, $\overline{Anti(d, S) = 0}$, $S$, $s$ ограничение при проверке -
$p_{\exists}(|d|, |S|)$

А общее ограничение при проверке - $p_{\forall}(|d|, |t|, |S|, |s|)$

[mihaild]

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

А Вы теперь утверждаете, что теорема Кука не верна?

Давно уже.

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

КНФ - не является $\mathbb{NP}$-полной задачей

У меня есть гипотеза: dmitgu хочет фиксированный полиномиальный алгоритм, который пару (полиномиальная недетерменированная машина Тьюринга, вход) сводит к $3-SAT$.

(такого скорее всего наверняка нет, если $NP=coNP$, то точно нет, но это совершенно другая задача)

[dmitgu]

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

А Вы теперь утверждаете, что теорема Кука не верна?

Не, с самого начала

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

о чем Вы говорите со своими $p_{\forall}(|S|, |s|)$ и $p_{\exists}(|S|)$

Предыдущий ответ для mihaild - об этом. Подмножество языка, на котором проверка неполиномиально быстрее, чем во всём. Помните, Вы ещё меня спрашивали, а точно ли алгоритм "Эдип" с программой в $d$ не сможет доказать $AntiOed_S() = 0$ ? Как раз случай игнорирования доказательства и аргумента $s$ - проверке заранее известно, что результат будет - 0. Вот для частного подмножества теорема Кука и не учитывает ограничение. Одной КНФ недостаточно - надо выбирать, не попадаешь ли ты в "скоростное" подмножество.

[mihaild]

dmitgu, что такое "ограничение при проверке"?
Выпишите, пожалуйста, явно:
-все нужные вам алгоритмы вместе со списками аргументов
-свойства этих алгоритмов: на каком входе они что выдают
-ограничение на время, за которое они это делают

[Xaositect]

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

Не, с самого начала

Так а где там ошибка в доказательстве?

[dmitgu]

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

Так а где там ошибка в доказательстве?

Не учитывается возможность существования "скоростного подмножества". Если считать, что КНФ при её решении в $P$ будет решать и исходную задачу - в которой "скоростное подмножество" есть и решение там должно быть неполиномиально быстрее общего.

Добавлю принципиальное:
То есть - для разных алгоритмов-решений будут разные КНФ вообще говоря. А это - терм. Надо выбрать нужный КНФ для правильного решения данного алгоритма-решения. А это не сводится к логике высказываний. Тут нужна индивидная переменная d

"Сводимость" к КНФ подразумевает ведь и сводимость решения к $P$ - если оно найдется?
А в исходной задаче я уже описывал возможную ситуацию:

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

Интересно узнать:
1. Если для бесконечного количества некоторых слов $(S, s)$ время поиска $p_M(|S|, |s|)$ сертификатов алгоритмом $M(S, s)$ неполиномиально дольше времени $p_{\exists}(|S|)$ проверки $R(S, s, y)$ тех же некоторых слов $(S, s)$, то $M(S, s)$ это - решение?

2. А если в целом у $R(S, s, y)$ время работы ограничено $p_{\forall}(|S|, |s|)$ ?

И как в терминах "языка" Вы выразите, что случай 1 тоже - не решение, даже если имеет место случай 2?

mihaild в сообщении #1202927 писал(а):

dmitgu, что такое "ограничение при проверке"?
Выпишите, пожалуйста, явно:
-все нужные вам алгоритмы вместе со списками аргументов
-свойства этих алгоритмов: на каком входе они что выдают
-ограничение на время, за которое они это делают

Не, сейчас не могу. Отчёты надо делать. Может позже. На будущее - я же вроде формулировал уже:

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

В предлагаемом языке «слову» соответствует теорема $t$, предельный размер доказательства для неё в 2-х представлениях $S$ и $s$, и аргумент долга (текст некоторого алгоритма-решения) $d$. Слово считается подтвержденным (существует «сертификат»), если длина строки $s$ равна числу $S$, имеется доказательство $y$ размером до $S$, и если теорема не равна утверждению $\overline{Anti(d, S) = 0}$ - это утверждение построено так, что алгоритм $d$ заведомо не может найти «сертификат» для него.

Скорость работы алгоритма проверки разная для разных случаев. Если имеет место $\overline{Anti(d, S) = 0}$, то полиномиальное ограничение на время работы $p_{Anti}(|d|, |S|)$ – что неполиномиально меньше чем у «общего» $Sph(d, t, S, s, y)$, чей ограничивающий полином – $p(|d|, |s|)$. Так как $|S|$ неполиномиально меньше, чем $|s|$.

Вы понимаете, что у нас есть 2 (Два) полиномиальных ограничения на время работы? Для задачи в целом он больше (дольше), а для подзадачи $Sph(d, \overline{Anti(d, S) = 0}, S, s, y)$ – он неполиномиально меньше. Меньшее может входить в большее, поэтому подзадача соответствует «общей» задаче и её полиномиальному ограничению, но для корректного «Эдипа» при решении вопроса о $\overline{Anti(d, S) = 0}$ «существует» такая задача из класса $NP$, которая неполиномиально быстрее «общей». И не выдать соответствующий быстрый ответ – значит, быть неспособным свести эту подзадачу из класса $NP$ к классу $P$.

А выдать быстро – значит, утратить соответствие (равенство результатов) между решаемой тобой задачей, соответствующей аргументу долга $\overline{Oed(\overline{Sph(..., ..., ..., ..., ...)}, \overline{-}, ..., ..., ...)}$ и такой же задачей, но в которой иной лишь аргумент долга – равный $\overline{-}$.

Я строю задачу, в которой любые алгоритмы-решения могут решать только «свои» задачи – потому что алгоритм-решение соответствует некоторой части «слова» разбираемого «языка». Но существенным (с иным результатом и/или ограничением на время работы проверки) этот нюанс становится лишь на утверждениях типа $\overline{Anti(d, S) = 0}$.

То есть – возврат 0 «Эдипом» при поиске сертификата для $\overline{Anti(d, S) = 0}$ – соответствует «языку». Хоть «Эдип» ищет доказательство для «слова» с теоремой $\overline{Anti(d, S) = 0}$ и аргументом долга
«объективно»,

но его работа соответствует аргументу долга
«Эдип с аргументом долга «объективно»».

Потому что дело не в том, для какого аргумента долга он ищет, а в том, «кто» ищет. Аргумент долга «Сфинкса» (то есть элемент слова в предлагаемом «языке») должен соответствовать фактам а не аргументу долга внутри «Эдипа».Так как: «Но словам ведь соответствуют понятия» (c) «Фауст». А частью «слова» у нас является алгоритм-решение с тем, что у него подставлено в качестве аргумента долга, а не то, что у него подставлено – независимо от самого алгоритма-решения.

[Xaositect]

У нас с Вами, к сожалению, нет общего языка, на котором мы разговариваем. Давайте Вы начнете с начала, определите снова всех Ваших Эдипов со Сфинксами, и покажете, как они соотносятся с общепринятыми определениями $\mathbf{NP}$.

Давайте установим некоторый фундамент:
- мы знаем, что такое машина Тьюринга и как кодировать машины и состояния машин словами. Код любого состояния машины меньше по длине, чем код самой машины.
- мы знаем, что такое время работы машины на заданном входном слове.
- у нас есть универсальная машина, которая получает на вход слово $m\sharp w\sharp 1^t$, где $m$ - код машины, $w$ - слово, и выдает результат вида $z\sharp u$. Результат расшифровывается так: после $t$ шагов вычисления машины с кодом $m$ на входе $w$ она находится в состоянии с кодом $z$, а на ее ленте ленте находится слово $u$. Время работы универсальной машины ограничено полиномом от длины входного слова $m\sharp w\sharp 1^t$.

-- Чт мар 23, 2017 17:49:11 --

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

Не учитывается возможность существования "скоростного подмножества". Если считать, что КНФ при её решении в $P$ будет решать и исходную задачу - в которой "скоростное подмножество" есть и решение там должно быть неполиномиально быстрее общего.

"Сводимость" к КНФ подразумевает ведь и сводимость решения к $P$ - если оно найдется?

Не понимаю. Есть много алгоритмов решения $\mathrm{SAT}$, и у многих из них есть бесконечные множества КНФ, на которых они работают полиномиальное время. Это ничего не говорит нам о плохих случаях.

Вы возможно, как-то неправильно понимаете сводимость. Сводимость языка $L$ к $\mathrm{SAT}$ - это вот что: у нас есть функция $f$, вычисляемая за полиномиальное время. Если $w \in L$, то $f(w)$ есть выполнимая КНФ, а если $w\notin L$ - то $f(w)$ есть невыполнимая КНФ. Теорема Кука говорит, что для любого языка из $\mathbf{NP}$ есть такая функция. Для каждого языка такая функция своя, и для каждого языка таких функций много - нам это неважно, нас интересует существование хотя бы одной.

Понятно, что если у языка $L$ есть какое-то хорошее подмножество, для которого есть быстрый алгоритм, то $f$ может посылать его в какое-то хорошее множество КНФ, для которого есть быстрый алгоритм. А может и не посылать - это неважно, нас все равно интересуют только самые плохие слова для каждой длины.

[dmitgu]

[quote="Xaositect в сообщении #1202936"]У нас с Вами, к сожалению, нет общего языка, на котором мы разговариваем. Давайте Вы начнете с начала, определите снова всех Ваших Эдипов со Сфинксами, и покажете, как они соотносятся с общепринятыми определениями $\mathbf{NP}$.

Вы правы – чтоб сблизить языки, я переписал статью с терминов «задач» в термины «языков» и классов их сложности (как смог) и на это и ушло полгода. Ужас ) Никаких семантических изменений не произошло при этой попытке «перевода». Так что не обещаю отвечать быстро – надо снова вспомнить всякие нюансы данного обсуждения. В аннотации я написал, какие препятствия тормозили – выложил новую версию на ЕДРИД «Языки логики и классы сложности. Рефлексия. $\mathbb{NP} \ne \mathbb{P}$» 28.9.2017. Но достаточно вот этого абзаца из аннотации:

Если интересен только вопрос о $\mathbb{NP} \ne \mathbb{P}$, то можно начинать читать заметку сразу с пункта 6 раздела «Язык $LS$ из класса $\mathbb{NP}$». До конца раздела (4 страницы) изложено построение несколько искусственного языка $LS$ из класса $\mathbb{NP}$ и то, почему его невозможно свести к классу $\mathbb{P}$. То есть, фактически даётся в общих чертах доказательство неравенства $\mathbb{NP} \ne \mathbb{P}$.

И дальше я копирую сюда пункт 6 (кое-что изменив) – до пункта 6.3 – если за один раз всё не «влезет», то будет видно, что ещё не всё скопировано и я жду час, пока тут можно записывать продолжение. Итак:

6. Для тех, кто решил читать заметку с этого пункта, дадим сводную информацию. Язык $LS$ из класса $\mathbb{NP}$ соответствует следующему алгоритму проверки (по которому язык $LS$ и можно отнести к классу $\mathbb{NP}$) – $\operatorname{Ls}(t, S, a, s, y)$. В неисключительных случаях (об исключительных будет в п. 6.1) аргументы «не подтвердят» слово языка и результат будет $0$ (Ноль), если не будет исполнено хоть одно из следующих условий:

$S$ – число, записанное в позиционном виде (например, в десятичном – вроде 3001) :
$s = \operatorname{ss}(S)$, где алгоритм $\operatorname{ss}(S)$ возвращает строку длиной $S$, состоящую только из символов «1»;
$a$ – текст (программный код) некоторого алгоритма типа $\overline{\operatorname{Sol}(... , ... , ...)}$ или же текст $\overline{-}$;
$t$ – текст некоторого утверждения на языке теории Пеано;
$y$ – текст некоторого доказательства на языке теории Пеано;
$|y|$ – размер текста y ограничен: $|y| \le q_S(S) - |a|$, где $q_S(S) = 1000 \cdot S^n$, $n$ – некоторая фиксированная степень, и, разумеется, условие на размер нарушено, если $ q_S(S) \le |a|$;

Утверждение с текстом в $t$ доказывается доказательством с текстом в $y$ в рамках теории Пеано (или любой другой заранее оговорённой теории арифметики, если она более полная и удобная для наших целей, чем теория Пеано);

Если случай не из пункта 6.1 и перечисленные условия выполнены, то:

$\operatorname{Ls}( t, S, a, s, y) = 1$.

Ещё мы условились, что записи вида $\overline{AntiSol_S}$ или $\overline{\operatorname{Sol}(... , ... , ...)}$ обозначают текст утверждения $AntiSol_S$ на заранее оговоренном языке логики и программный код (тоже текст, фактически) алгоритма $\operatorname{Sol}(..., ..., ...)$, записанный оговорённым способом представления алгоритмов в выбранной за основу языка $LS$ теории первого порядка (теория Пеано способна представлять алгоритмы, но не очень наглядно – тут есть что улучшать для практических нужд).

И, разумеется, мы пользуемся не «гёделевыми номерами», которые дают неполиномиально огромное представление для информации (число 10, например, имеет вид «1111111111»), а принятым в «человеческом» и «компьютерном» мире представлением в виде текстов и чисел в позиционном (десятичном, например) представлении.

Теперь – о времени работы алгоритма проверки для разных случаев, словах языка $LS$, сертификатах, их размере и исключениях:

6.1. Для случаев, подходящих под шаблон
$\operatorname{Ls}(\overline{AntiSol_S}, S, \overline{\operatorname{Sol}(... , ... , ...)}, ... , ...)$ количество шагов работы – в пределах полинома $p_{\exists}(|t|, |S|, |a|)$. В силу того, что в данном случае $t = \overline{AntiSol_S}$, чей размер полиномиально зависит от размера $|a| = |\overline{\operatorname{Sol}(... , ... , ...)}|$ и от размера $|S|$, а при этом $|\overline{\operatorname{Sol}(... , ... , ...)}| < |\overline{AntiSol_S}|$, то в $p_{\exists}(|t|, |S|, |a|)$ можно заменить $|a|$ на $|t|$ и ограничивающий алгоритм останется ограничивающим (количество шагов работы алгоритма проверки не превысит результат данного ограничивающего алгоритма) и при этом он останется полиномиальным. И его тогда можно переписать в виде:

$p_{\exists}(|\overline{AntiSol_S}|, |S|)$ (что равно $p_{\exists}(|t|, |S|)$).

Проверку под шаблон 6.1 алгоритм $\operatorname{Ls}(t, S, a, s, y)$ проводит в первую очередь и – если соответствие обнаружено – возвращает $0$ в пределах указанного времени (количества шагов).
Кстати, многоточия в конце $\operatorname{Ls}(\overline{AntiSol_S}, S, \operatorname{Sol}(... , ... , ...), ... , ...)$ стоят потому, что аргументы $s, y$ в данном случае не используются и тут алгоритм зависит, фактически, от трёх аргументов, возвращая $0$: $\operatorname{Ls}(\overline{AntiSol_S}, S, \operatorname{Sol}(... , ... , ...), ... , ...) = 0$.

И, напомню, случай 6.1 относится к тому слову (словам!), принадлежность которого отвергается и смысл этого отказа такой: «Алгоритм $\operatorname{Sol}(\overline{AntiSol_S}, S, ...)$ не может найти доказательство для утверждения $AntiSol_S$». Можно было бы добавить «…в пределах доказательств допустимого размера», но найти доказательство для утверждения $AntiSol_S$ алгоритм $\operatorname{Sol}(\overline{AntiSol_S}, S, ...)$ не может в принципе. Поэтому не может «вообще» и, в силу этого, «…в пределах доказательств допустимого размера» в том числе. Подробнее:

Алгоритм-решение $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ решает вопрос о принадлежности языку $LS$

слова вида 1: $\overline{AntiSol_S}, S, s$; с сертификатом вида 1: $a, y$.

При этом сам алгоритм-решение в этом решении соответствует части сертификата $a = \overline{\operatorname{Sol}(... , ... , ...)}$ и из пункта 6.1 за количество шагов в пределах $p_{\exists}(|\overline{AntiSol_S}|, |S|)$ можно узнать от алгоритма проверки $\operatorname{Ls}(\overline{AntiSol_S}, \operatorname{Sol}(... , ... , ...), ... , ...) = 0$, что никакого подтверждающего сертификата с такой частью $a$ для данного слова найти невозможно – что соответствует тому факту, что алгоритм $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ не может корректно подтвердить (выдать в качестве результата $1$) слово $\overline{AntiSol_S}, S, s$ (оно построено в соответствии с теоремой о неопределимости для данного алгоритма-решения).

При этом в языке $LS$ помимо слов вида 1, есть и

слова вида 2: $t, S, a, s$; с сертификатом вида 2: $y$.

И данный ответ алгоритма проверки из пункта 6.1:

$\operatorname{Ls}(\overline{AntiSol_S}, \operatorname{Sol}(... , ... , ...), ... , ...) = 0$

соответствует отсутствию в языке $LS$

слов вида 2: $\overline{AntiSol_S}, S, \overline{Sol(…, …, …)}, s$; с сертификатами вида 2: $y$.

То есть, хоть алгоритм-решение $\operatorname{Sol}(... , ... , ...)$ должен решать вопрос о принадлежности языку $LS$ слов вида 1, но при $\operatorname{Sol}(\overline{AntiSol_S}, S, s) = 0$ он даёт правильный ответ с точки зрения непринадлежности языку $LS$ слова вида 2: $\overline{AntiSol_S}, S, \overline{Sol(…, …, …)}, s$. Но непринадлежность языку данного слова вида 2 соответствует как раз невозможности найти подтверждающий сертификат с частью $a = \overline{\operatorname{Sol}(... , ... , ...)}$ для слова вида 1: $\overline{AntiSol_S}, S, s$.

В случае 6.1 ограничивающий алгоритм $p_{\exists}(|t|, |S|)$ не зависит от $s$, $y$. Но от них не зависит и работа $\operatorname{Ls}(\overline{AntiSol_S}, \operatorname{Sol}(... , ... , ...), ... , ...) = 0$ в случае, подходящем под шаблон пункта 6.1.

6.2. Для остальных случаев количество шагов работы алгоритма проверки – в пределах $p_{\forall}(|t|, |S|, |s|)$, впрочем, и пункт 6.1 соответствует пункту 6. Но случай 6.1 является более жёстким ограничением – неполиномиально более жёстким, так как в случае 6.2 членом полинома является размер $|s|$, растущий экспоненциально относительно размера $|S|$.

Случай 6.2. в равной степени относится к словам вида 1 и 2, не попадающими под шаблон пункта 6.1:

слова вида 1: $t, S, s$; с сертификатом вида 2: $a, y$.

слова вида 2: $t, S, a, s$; с сертификатом вида 2: $y$.

Для слов вида 1 суммарный размер сертификата ограничен (требование корректности) алгоритмом

$1000 \cdot S^n$, где $n$ – некоторая фиксированная степень:

$|a| + |y| \le 1000 \cdot S^n$, что повторяет сказанное в начале пункта 6 про размер доказательства $|y|$:

$|y| \le q_S(|s|) - |a|$,

а последнее ограничение соответствует сертификату вида 2. Для обоих вариантов, как видим, ограничение сертификата является полиномиальным относительно размера слова.

И кроме специальных случаев из 6.1 – при котором соответствующие слова языку $LS$ как раз не принадлежат – в остальном принадлежность слов вида 1 и вида 2 языку $LS$ (при корректных $a$) ничем не отличаются друг от друга. Такая «одинаковость» (кроме спец. случая) связана с тем, что в языке $LS$ мы учитываем только ту ограниченность возможностей алгоритмов-решений, которая следует из теоремы о неопределимости. Но эта ограниченность полностью исчерпывается специфическими случаями (хоть их и бесконечное количество для каждого алгоритма-решения) из пункта 6.1.

6.3. Если алгоритм-решение $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ для слова из специального случая 6.1 возвращает $1$ при корректном $s = \operatorname{ss}(S)$:

$\operatorname{Sol}(\overline{AntiSol_S}, S, s) = 1$ (случай 1),

то доказательства для утверждения $AntiSol_S$ нет, и, напротив, имеется доказательство для его отрицания. То есть, ответ данного алгоритма-решения на данном слове в этом случае заведомо не корректен.

Если же алгоритм-решение $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ для слова из специального случая 6.1 возвращает $0$ при корректном $s = \operatorname{ss}(S)$:

$\operatorname{Sol}(\overline{AntiSol_S}, S, s) = 0$ (случай 2),

то логическое доказательства для утверждения $AntiSol_S$ имеется, но, вопрос – соответствует ли размер данного доказательства допустимым размерам:

$|y| \le q_S(|s|) - |a|$.

Но если размер данного доказательства соответствует указанному пределу, то ответ данного алгоритма-решения на данном слове и в этом случае оказывается не корректным.

Если же алгоритм-решение $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ для слова из специального случая 6.1 не возвращает никакого ответа при корректном $s = \operatorname{ss}(S)$ (случай 3), то данное слово действительно не принадлежит языку $LS$ и это подтверждается при любых сертификатах алгоритмом проверки. То есть, и в данном случае работа алгоритма-решения $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ оказывается не корректной.

Значит, единственный случай, при котором алгоритм-решение $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ может выдать корректный результат – случай 2. И результат этот должен быть $0$. И этот результат соответствует результату работы алгоритма проверки $\operatorname{Ls}(\overline{AntiSol_S}, S, \operatorname{Sol}(... , ... , ...), ... , ...) = 0$ за полиномиальное количество шагов работы – в пределах $p_{\exists}(|\overline{AntiSol_S}|, |S|)$ (что равно $p_{\exists}(|t|, |S|)$).

Поэтому при сведении нашей задачи из класса $\mathbb{NP}$ в класс $\mathbb{P}$ полиномиальность времени проверки для случая 2 $p_{\exists}(|t|, |S|)$ должна превратиться в полиномиальность времени на обнаружение решения (или невозможности решения) вида $p_{\exists +}(|t|, |S|)$.

И вот идея доказательства для $\mathbb{NP} \ne \mathbb{P}$:

Здесь очевидно, что при достаточно больших $S$ данное предельное время работы алгоритма-решения из случая 2 экспоненциально мало по сравнению с допустимым размером доказательств: $|y| \le q_S(|s|) - |a|$, так как размер $|s| = |\operatorname{ss}(S)|$ экспоненциально велик по сравнению и с размером $|a|$, и с аргументами в $p_{\exists +}(|t|, |S|)$ при достаточно больших $S$.

А это значит, что для достаточно больших $S$ среди допустимых доказательств найдётся и то, в котором будет вывод и для случая 2: $\operatorname{Sol}(\overline{AntiSol_S}, S, \operatorname{ss}(S)) = 0$, и для вытекающего из него утверждения $AntiSol_S$. А это и будет означать, что алгоритм $\operatorname{Sol}(\overline{AntiSol_S}, S, \operatorname{ss}(S))$ не смог подтвердить истинность утверждения $AntiSol_S$ для которого есть доказательство среди доказательств допустимого размера.

А поскольку алгоритм $\operatorname{Sol}(..., ..., ...)$ произвольный, то это будет означать отсутствие корректных алгоритмов-решений, делающих язык $LS$ языком класса $\mathbb{P}$. То есть – оказывается доказанным неравенство $\mathbb{NP} \ne \mathbb{P}$.

Конечно, в нескольких абзацах выше изложено доказательство $\mathbb{NP} \ne \mathbb{P}$ в общих чертах, а детали – как строить вывод для утверждения $AntiSol_S$ при корректном времени работы алгоритма-решения $\operatorname{Sol}(\overline{AntiSol_S}, S, \operatorname{ss}(S)) = 0$ и почему размер вывода будет допустимого размера – изложены в следующем разделе.

[mihaild]

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

Язык $LS$ из класса $\mathbb{NP}$ соответствует следующему алгоритму проверки (по которому язык $LS$ и можно отнести к классу $\mathbb{NP}$) – $\operatorname{Ls}(t, S, a, s, y)$.

И что собственно из этого слова из языка, а что - подсказка? Напоминаю, что язык - это множество слов; при большом желании можно считать язык множеством кортежей слов. Т.е. как минимум нужно что-то типа "язык $LS$ - множество таких троек $t, S, a$, что существуют полиномиальной длины $s, y$ такие, что $\operatorname{Ls}$ на них выдает $1$" (только, наверное, с другим разбиением переменых).

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

$y$ – текст некоторого доказательства на языке теории Пеано;

Доказательства чего? Чего угодно?

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

Ещё мы условились, что записи вида $\overline{AntiSol_S}$ или $\overline{\operatorname{Sol}(... , ... , ...)}$ обозначают текст утверждения $AntiSol_S$

Что за утверждение $AntiSol_S$?

(без ответов на эти вопросы дальше читать не хочется)

[dmitgu]

mihaild в сообщении #1252351 писал(а):

нужно что-то типа "язык $LS$ - множество таких троек $t, S, a$,

Так вот же:

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

Случай 6.2. в равной степени относится к словам вида 1 и 2, не попадающими под шаблон пункта 6.1:

слова вида 1: $t, S, s$; с сертификатом вида 2: $a, y$.

слова вида 2: $t, S, a, s$; с сертификатом вида 2: $y$.

И в пункте 6.1 особые случаи.

mihaild в сообщении #1252351 писал(а):

Доказательства чего? Чего угодно?

Тоже есть:

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

Утверждение с текстом в $t$ доказывается доказательством с текстом в $y$ в рамках теории Пеано (или любой другой заранее оговорённой теории арифметики, если она более полная и удобная для наших целей, чем теория Пеано);

mihaild в сообщении #1252351 писал(а):

Что за утверждение $AntiSol_S$?

Упомянуто тут:

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

соответствует тому факту, что алгоритм $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ не может корректно подтвердить (выдать в качестве результата $1$) слово $\overline{AntiSol_S}, S, s$ (оно построено в соответствии с теоремой о неопределимости для данного алгоритма-решения).

А вообще если подробнее про это, то можно из следующего раздела:

У нас есть простое верное равенство для произвольного $S$:
$\operatorname{ContrSol}(S) = \operatorname{If}( \operatorname{Sol}(\overline{AntiSol_S}, S, \operatorname{ss}(S)) = 0, 1, 0)$
Это равенство описывает, как работает алгоритм $\operatorname{ContrSol}(S)$, лежащий в основе $AntiSol_S$ и «поступающий наоборот». Алгоритм
If(Условие, Результат при истине, Результат в ином случае)
широко известен в программировании.
...
равенство $\operatorname{ContrSol}(S) = 1$ и есть утверждение $AntiSol_S$

То есть, $\operatorname{ContrSol}(S)$ запускает $\operatorname{Sol}(\overline{AntiSol_S}, S, \operatorname{ss}(S))$ и поступает наоборот по отношению к тому результату, который выдаст данный алгоритм. Естественно, алгоритм $\operatorname{Sol}(\overline{AntiSol_S}, S, \operatorname{ss}(S))$ не может дать правильное доказательство - будет или не будет исполнено $\operatorname{ContrSol}(S) = 1$.

[mihaild]

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

Случай 6.2. в равной степени относится к словам вида 1 и 2, не попадающими под шаблон пункта 6.1:
слова вида 1: $t, S, s$; с сертификатом вида 2: $a, y$.
слова вида 2: $t, S, a, s$; с сертификатом вида 2: $y$.

Я не понимаю, что это значит (какой еще шаблон? какие случаи?), и в любом случае - это уже где-то дальше. Если вы при определении ссылаетесь на следующие пункты - очень легко попасть в цикл, который сложно заметить и невозможно распутать. Определения должны выписываться по порядку, и ссылаться только на предыдущие определения (на приведенные позже - нельзя).
Попробую угадать: язык состоит из четверок $(t, S, a, s)$ и троек $(t, S, s)$?

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

Утверждение с текстом в $t$ доказывается доказательством с текстом в $y$ в рамках теории Пеано

Что такое "утверждение с текстом в $t$"?
Верно ли, что вы имели в виду "$y$ - доказательство утверждения $t$ в $PA$"?
(извините, что так занудничаю, но иначе это всё выльется в еще 14 страниц, из которых так и не удастся вытащить достаточно понятное рассуждение, чтобы в нем можно было найти ошибку)

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

Для случаев, подходящих под шаблон
$\operatorname{Ls}(\overline{AntiSol_S}, S, \overline{\operatorname{Sol}(... , ... , ...)}, ... , ...)$

Что такое "случай", "шаблон", "подхождение случая под шаблон", $AntiSol_S$, $Sol$?
($\overline{x}$ - это, видимо, код $x$?)

Тут, видимо, должно быть написано что-то вроде "$\operatorname{Ls}$ - полиномиальный алгоритм, принимающий пятерки $t, S, s, a, y$ и возвращающий $1$, если выполнены какие-то ограничения на длину, $t$ - код некоторого утверждения в сигнатуре арифметики, $y$ - код доказательства этого утверждения и какие-то еще - какие? выпишите их явно в терминах $t, S, s, a, y$ условия".

[dmitgu]

mihaild в сообщении #1252361 писал(а):

язык состоит из четверок $(t, S, a, s)$ и троек $(t, S, s)$?

Да. Чего тут "угадывать"?

mihaild в сообщении #1252361 писал(а):

Верно ли, что вы имели в виду "$y$ - доказательство утверждения $t$ в $PA$"?

Да. Написано же:

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

Утверждение с текстом в $t$ доказывается доказательством с текстом в $y$ в рамках теории Пеано

mihaild в сообщении #1252361 писал(а):

Что такое "случай", "шаблон", "подхождение случая под шаблон", $AntiSol_S$, $Sol$?

Да всё просто - каждому $Sol$ и $S$ соответствует свой $AntiSol_S$ - по их текстам "вычисляется" текст $AntiSol_S$ и сравнивается с тем, что передано в аргументе $t$

mihaild в сообщении #1252361 писал(а):

($\overline{x}$ - это, видимо, код $x$?)

Написано же:

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

Ещё мы условились, что записи вида $\overline{AntiSol_S}$ или $\overline{\operatorname{Sol}(... , ... , ...)}$ обозначают текст утверждения $AntiSol_S$ на заранее оговоренном языке логики и программный код (тоже текст, фактически) алгоритма $\operatorname{Sol}(..., ..., ...)$, записанный оговорённым способом представления алгоритмов в выбранной за основу языка $LS$ теории первого порядка (теория Пеано способна представлять алгоритмы, но не очень наглядно – тут есть что улучшать для практических нужд).

mihaild в сообщении #1252361 писал(а):

если выполнены какие-то ограничения на длину, $t$ - код некоторого утверждения в сигнатуре арифметики, $y$ - код доказательства этого утверждения и какие-то еще - какие? выпишите их явно в терминах $t, S, s, a, y$ условия".

Да выписаны же:

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

В неисключительных случаях (об исключительных будет в п. 6.1) аргументы «не подтвердят» слово языка и результат будет $0$ (Ноль), если не будет исполнено хоть одно из следующих условий:

$S$ – число, записанное в позиционном виде (например, в десятичном – вроде 3001) :
$s = \operatorname{ss}(S)$, где алгоритм $\operatorname{ss}(S)$ возвращает строку длиной $S$, состоящую только из символов «1»;
$a$ – текст (программный код) некоторого алгоритма типа $\overline{\operatorname{Sol}(... , ... , ...)}$ или же текст $\overline{-}$;
$t$ – текст некоторого утверждения на языке теории Пеано;
$y$ – текст некоторого доказательства на языке теории Пеано;
$|y|$ – размер текста y ограничен: $|y| \le q_S(S) - |a|$, где $q_S(S) = 1000 \cdot S^n$, $n$ – некоторая фиксированная степень, и, разумеется, условие на размер нарушено, если $ q_S(S) \le |a|$;

Утверждение с текстом в $t$ доказывается доказательством с текстом в $y$ в рамках теории Пеано (или любой другой заранее оговорённой теории арифметики, если она более полная и удобная для наших целей, чем теория Пеано);

Если случай не из пункта 6.1 и перечисленные условия выполнены, то:

$\operatorname{Ls}( t, S, a, s, y) = 1$

и

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

Проверку под шаблон 6.1 алгоритм $\operatorname{Ls}(t, S, a, s, y)$ проводит в первую очередь и – если соответствие обнаружено – возвращает $0$ в пределах указанного времени (количества шагов).

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

$\operatorname{Ls}(\overline{AntiSol_S}, S, \overline{\operatorname{Sol}(... , ... , ...)}, ... , ...) = 0$

В последней строке цитаты исправил опечатку - $\overline{\operatorname{Sol}(... , ... , ...)}$ (добавил потерянную черту сверху). В том же абзаце ещё такая же опечатка и ещё такая - же в п. 6.3 абзац "Значит, единственный случай, ...". Я повторю весь пункт 6 когда перейдём на следующую страницу - с исправленными этими и другими (если найдём) опечатками.

Вам ограничения на время работы алгоритма $Ls$ тоже процитировать?