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

[dmitgu]

Про класс $NP$ и про $NP_{primitive}$.

Меня тут ещё один вопрос озадачил. Вот я построил в прошлом доказательстве (доказательство ли это и доказательство чего - похоже дискуссионный вопрос - о чём скажу) алгоритм $\operatorname{AntiMt}()$, который всегда поступает вопреки алгоритму решения. Да, я там решал спорную задачу (но считаю пока что прав), но могу решать и с вполне конкретным алгоритмом проверки и алгоритм $\operatorname{AntiMt}()$ будет обладать тем же свойством.
Так вот вопрос - а если в теории (а моя задача теперь будет вполне конкретная математическая теория) я аксиоматизирую, чему должен быть равен алгоритм решения $\operatorname{Mt}()$ когда он разбирается с алгоритмом $\operatorname{AntiMt}()$? Притом аксиоматизирую корректно:

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

И в составе аксиом $Aks$ будет находится и само это равенство (я это сделаю при помощи диагонализации). Разве это не докажет моментально неполноту алгоритма решения $\operatorname{Mt}()$ и невозможность, таким образом, свести задачу к задаче класса P?

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

Но в данном случае «обманывающий» $\operatorname{Mt}()$ явно не отвечает теории - он поступает вопреки аксиоме $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) = knockout$ для того, чтобы «спрогнозировать» $\operatorname{AntiMt}()$. Вот если бы он выдал результат, расходящийся с логическим выводом, то мы бы признали алгоритм ошибочным? Да. И нас бы не остановила разница во времени работы проверки доказательства и его поиска. Это касается подстановки текстов алгоритмов в качестве аргумента в $\operatorname{Mt}()$.
Хорошо, а на саму работу алгоритма мы смотрим или нет? Если его собственный результат расходится с аксиомой, например? Да и по факты тут это неизбежно приводит к противоречию и расхождению с реальностью (противоречием теории). А по времени на сравнение - тут не больше, чем сравнивать работу $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$ как прогнозиста для $\operatorname{AntiMt}()$ , либо сравнивать работу $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()})$ с аксимой про сам $\operatorname{Mt}()$. Второй случай даже быстрее, потому что результат для $\operatorname{AntiMt}()$ надо ещё вывести (будет $Anti(knockout)$ - если посмотрите в прошлое доказательство).

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

Скажу кое-что про «окрестности» проблемы. Очень похоже (вообще я уверен, но мало ли...), что в теории алгоритмов есть парадокс (попросту ошибка), когда математики ставят состав математического объекта (класс задач $NP$) в зависимость от своих знаний. Об этом я писал в предварительном эвристическом варианте ( post954742.html#p954742 ). Суть в том, что они хотят, чтоб туда входили лишь задачи, чей алгоритм проверки они знают. Хотя есть задачи, чей алгоритм проверки удовлетворяет требованиям класса $NP$, но какой это алгоритм - решения в общем случае нет. И приведенное ранее (перед этим) мое доказательство для $NP \NE P$ (постановка задачи - post956171.html#p956171 , доказательство - post956292.html#p956292 ) существенно опирается на невозможность решить вопрос - какой там реально алгоритм в общем случае.

Но - вообще-то - есть и задачи из класса $NP$, чей алгоритм проверки действительно известен, либо который можно легко найти в общем случае. И для этого частного случая требуется отдельное доказательство, что этот $NP_{primitive}$ (назову так этот «псевдоподкласс» в $NP$) тоже не сводится к $P$.
Я бы назвал такие задачи «задачами с известным полиномиальным алгоритмом проверки», но так нельзя определять математические объекты, потому что вопрос - кому известный? Институту им. Стеклова, водопроводчику Фёдору или, например, межгалактической академии инопланетян? Может, правильно говорить о таких множествах задач из $NP$, которые объединены друг с другом заранее заданным алгоритмом проверки некоторой «основной» задачи и заранее заданной сводимостью к ней остальных задач (если в определяемом множестве больше, чем одна задача)? И подобное множество будет тогда не единственным, видимо. Но, вопрос с определением довольно тонкий, и предмет коллективного обсуждения.
Это к вопросу о терминах. Пока мне не объяснили где у меня ошибка (если она есть), я все же предпочел бы пользоваться обозначением $NP_{primitive}$ для задач из класса $NP$ с заранее заданным алгоритмом проверки.

Мое предыдущее доказательство не позволяет, например, дать ответ о (не)сводимости задачи выполнимости ДНФ (дизъюнктивной нормальной формы - уравнению из булевых переменных) к задаче из класса P. А ведь такой вопрос имеется.
В этом смысле я не претендую, что прошлым доказательством для $NP \ne P$ я решил «проблему тысячелетия». Потому что хоть они и спросили и я ответил (гм.. если..) именно на заданный вопрос (подходя формально), но все же хотели они спросить иное. Но если парадокс верен - который я обнаружил - то это существенно. И парадокс тоже надо решать. По крайней мере, раньше так делалось, судя по истории математики.

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

1. Имеется некоторая система аксиом $Aks$ (пусть непротиворечивая), расширяющая теорию Пеано. Эти аксиомы заданы некоторым списком (можно считать для начала что список расширения пуст). В качестве элементов списка стоят аксиомы или схемы аксиом (пример схемы аксиом - любая аксиома логики - там используются формульные переменные). И у нас есть быстрый способ добавления в любой такой список новой аксиомы - после чего получается новый список аксиом с теми же свойствами списка. Способ добавления аксиомы обозначим как $\operatorname{AddAks}(Aks, X)$ - в результате работы этот алгоритм вернет список аксиом $Aks$, расширенный аксиомой $X$. Иногда для простоты я буду писать $Aks + X$ вместо приведенной формулы - когда ясно, что речь об аксиомах.

2. В качестве проверяемого слова будем рассматривать пару текстов - список аксиом из п. 1 и $A()$ – записанный на языке теории текст алгоритма.

3. В качестве слова-свидетеля будем рассматривать текст доказательства для $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$ и/или $Aks$ выступает какой-то бессмысленный текст, то $R(Aks, x, y)$ возвращает «ложь».
Размеры всех упомянутых полиномов считаем достаточно большими для наших целей - по контексту будет видно, что это легко достижимо.

Берем нашу задачу из пунктов 1-3. Берем метод поиска слов-свидетелей $y$, подходящих для заданного слова $x$ (то есть, $|y| < Px(|x|)$ и $R(Aks, x, y)$ дает истину). Назовем наш метод поиска слов-свидетелей для слова $x$ - алгоритмом $Mt(Aks, x)$.
Для простоты считаем, что $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)$ конечно и ограничено некоторым всюду определённым полиномом $T(|Aks| + |x|)$.
Мы исходим из того, что $\operatorname{Mt}()$ подтверждает каждое проверяемое слово из нашей задачи, для которого есть соответствующее слово-свидетель, проходящее проверку $R()$ нашей задачи.
Если такого $\operatorname{Mt}()$ не существует, то $NP_{primitive} \ne P$. Мы будем доказывать «от противного» и поэтому работаем, словно $\operatorname{Mt}()$ в нашем распоряжении.

Если же для какого-то проверяемого слова $\operatorname{Mt}()$ выдаст результат $knockout$ , хотя подтверждающее слово-свидетель есть, то алгоритм $\operatorname{Mt}()$ будем называть не полным.
Если же $\operatorname{Mt}()$ выдал значимый результат (не $knockout$ ) для проверяемого слова, которое не имеет подтверждающего его слова-свидетеля, то $\operatorname{Mt}()$ будем называть не корректным.
И - очень важный момент - алгоритм будет не корректным, если в теории выведено утверждение о его работе, эта работа удовлетворяет ограничениям на время работы данного алгоритма решения, но алгоритм поступает в противоречии с этой аксиомой. Возможно, что дело в некорректности самой теории, но если при правильном поведении алгоритма противоречия не возникло бы, то проблема в самом алгоритме и он является не корректным.

Существует ли хоть один корректный $\operatorname{Mt}()$? Да - который всегда возвращает $knockout$ , например.
Чтобы $NP_{primitive} = P$ необходимо, чтобы существовал $\operatorname{Mt}()$ с полиномиальным временем работы - и к тому же корректный и полный.

Доказательство

Про диагонализацию см. в прошлой постановке задачи - post956171.html#p956171 , а про построение AntiMt см. начало прошлого доказательства - post956292.html#p956292 . И там же свойство AntiMt доказано в п. 5 для неравенства (фактического - по работе алгоритмов, а не по теории) вот такое:

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

В частности, для случая, когда $\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}()}) = knockout$ получится:

$\operatorname{AntiMt}() = \operatorname{Anti}(knockout)$

Про вывод последнего равенства - см. пункты 8 (как исходный), 9, 10 того вывода и пункт 1 (это про свойства диагонализации). Условия корректности из прошлого доказательства в нынешнем доказательстве не верны (пункты 6 и 7), поэтому и выводы из них здесь учитывать не следует.

Теперь - как строится Аксиома «диагонального нокаута».
Нам нужно построит утверждение, которое утверждало бы, что

$\operatorname{Mt}(Aks, \overline{\operatorname{AntiMt}(\ldots)}) = knockout$ ,

Но надо чтоб в составе $Aks$ было само это выражение. То есть, чтобы Аксиома задавала результат, который должен быть у Mt(Aks, «AntiMt(...)») при данном наборе аксиом.
Многоточие вместо аргумента в $\operatorname{AntiMt}()$ означает, что программа $\operatorname{AntiMt}()$, зависящая от аксиом - так же меняет свои аксиомы, как и переменная для аксиом в $\operatorname{Mt}()$ (где $Aks$).
То есть, в следующее выражение:

$\operatorname{Mt}(\operatorname{AddAks}(Aks, X), \overline{\operatorname{AntiMt}(...)}) = knockout$

нам надо добавить вместо $X$ такой текст, который выражал бы само это выражение. Это делается при помощи алгоритма $\operatorname{diag}()$ вот таким образом:

$\operatorname{Mt}(\operatorname{AddAks}(Aks, \operatorname{diag}[\overline{\operatorname{Mt}(\operatorname{AddAks}(Aks, \operatorname{diag}(x)), \overline{\operatorname{AntiMt}(...)}) = knockout}] ), \overline{\operatorname{AntiMt}(...)}) = knockout$

Назовем приведенное равенство так: $\operatorname{DiagKnockout}(Aks)$. Именно его текст добавляется к аксиомам. Что можно переписать так:

$\operatorname{Mt}(\operatorname{AddAks}(Aks, \overline{\operatorname{DiagKnockout}(Aks)}), \overline{\operatorname{AntiMt}(...)}) = knockout$

Получилось эквивалентное равенство, а не то же самое, потому что прошлое равенство и было $\operatorname{DiagKnockout}(Aks)$, а данное выражение - это как прошлое, но после того как сработал $\operatorname{diag}[]$ с квадратными скобками и вместо него - результат его работы.
Но в итоге мы добились чего хотели - у нас есть аксиома, которая говорит, чему должен быть равен результат $\operatorname{Mt}()$ при работе с $\operatorname{AntiMt}()$. И этот результат мы теперь вроде знаем сразу (если $\operatorname{Mt}()$ не поступит иначе и не сделает теорию противоречивой) и можем опираться на него в доказательствах - раз это аксиома.

Если найдется хоть одна непротиворечивая теория, которая будет расширена аксиомой диагонального нокаута и $\operatorname{Mt}()$ «согласится» с аксиомой диагонального нокаута, то он сразу будет неполон. Хотя, обосную - почему он будет неполон.
Рассмотрим работу алгоритма $\operatorname{Mt}(\operatorname{AddAks}(Aks, \overline{\operatorname{DiagKnockout}(Aks)}), \overline{\operatorname{AntiMt}(...)})$. Если он выдаст $knockout$ (что и означает «согласится»), то равенство

$\operatorname{Mt}(\operatorname{AddAks}(Aks, \overline{\operatorname{DiagKnockout}(Aks)}), \overline{\operatorname{AntiMt}(...)}) = knockout$

оказывается истинным. Значит, при расширении им как аксиомой любой непротиворечивой теории (с какими угодно аксиомами $Aks12345$) расширенная теория получится непротиворечивой. Получается, что наша непротиворечивая теория (ещё не расширенная) для которой составлялась новая аксиома $\operatorname{DiagKnockout}(Aks)$ - одна из таких теорий. И в эту теорию ставится в качестве новой аксиомы равенство, эквивалентное представленному равенству - если уж быть точным. А эквивалентно оно по лемме о диагонализации - только уже для предикатов. Потому что по сути мы и совершили диагонализацию равенства, а равенство - вариант предиката.

И в полученной таким образом расширенной теории $\operatorname{Mt}()$ неполон из-за своего $knockout$ , потому что в полученной непротиворечивой теории из-за аксиомы диагонального нокаута можно в соответствии с аксиомой $\operatorname{Mt}(NewAks, \overline{\operatorname{AntiMt}()}) = knockout$ в 2 шага (помимо вывода свойств для $\operatorname{AntiMt}()$ из леммы о диагонализации) вывести $\operatorname{AntiMt}() = \operatorname{Anti}(knockout)$ - о чём было сказано в начале нашего доказательства. И после этого в теории есть доказательство для результата работы $\operatorname{AntiMt}()$, которого нет у $\operatorname{Mt}()$. А это и есть неполнота.

Значит, случай, когда $\operatorname{Mt}()$ «согласился» хоть в одной теории с аксиомой диагонального нокаута мы рассмотрели и в таком случае $\operatorname{Mt}()$ неполон. А в случае если он «не согласился» - теория вообще заведомо противоречива, а его поведение не соответствует аксиомам.
Теорема доказана.

[dmitgu]

Похоже, мне удалось избавиться от расширительного толкования «проверки корректности» из предыдущей записи ( post960183.html#p960183 ) и - таким образом - дать доказательство для $NP_{primitive} \ne P$ в традиционных рамках.

Я знаю это доказательство несколько дней, но не хотелось делиться, потому что меня крайне озадачивало следствие из него. А именно, я не понимал, где «прокалывается» тогда алгоритм полного перебора доказательств? Вроде, он может предвидеть, когда встроенная в задачу проверка заметит противоречия (я включу такой элемент в алгоритм проверки) и избежать их, к тому же у него может быть любое преимущество по времени над проверкой. Ведь в приводимом доказательстве не играет никакой роли - как увидим - разница во времени между поиском слова-свидетеля и его проверкой. Есть ещё один удивительный эффект в доказательстве, который Вы увидите.

Но в итоге мне удалось обнаружить совершенно неожиданное обстоятельство, насколько понимаю. Назову его «обстоятельство $NP_{spirit}$». Оно же принципиально отличает задачу решения ДНФ (булевых уравнений) от задач из класса $NP_{primitive} $ на базе математических теорий - которые рассматриваю я. И принципиальную несводимость вторых к первой, а также то, что не учитывается в доказательстве теоремы Кука (о сводимости задач из $NP$ к некоторым $NP$-полным задачам).

Я говорю не о том, что теорема Кука не учитывает, что класс $NP$ включает в себя и задачи с неразрешимыми алгоритмами проверки - это было продемонстрировано раньше. Но даже и среди задач с заранее определенным алгоритмом проверки тоже нет такой сводимости, вообще говоря. Я обозначал тип таких задач как $NP_{primitive}$, но теперь прежнее название представляется пренебрежительным и я предпочту - $NP_{def}$, например. И в нём есть подтипы - назову их $NP_{atom}$ и $NP_{spirit}$. Задача решения ДНФ имеет подтип $NP_{atom}$, а рассматривая ниже задача - $NP_{spirit}$.
Что такое «обстоятельство $NP_{spirit}$» - я скажу после доказательства. В принципе, оно может доказательство и заменить в некотором смысле. Но всё же формальное доказательство необходимо, а потом уже - об «обстоятельстве $NP_{spirit}$». Будет интересно, увидите.

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

Итак, нам надо убрать расширенную проверку корректности (на противоречия с аксиомами) для алгоритма-решателя $Mt$. Вместо этого будем проверять противоречия слов-свидетелей. Чтобы в нашей задаче из предыдущей записи поиск противоречий стал частью встроенной проверки, добавим в постановку задачи п. 4 - проверку на противоречия $R2$. Общую проверку обозначим буквой $R$, а прежняя (часть новой) теперь будет $R1$ (вместо $R$) - поэтому изменения с п.3:

1. Имеется некоторая система аксиом $Aks$ (пусть непротиворечивая), расширяющая теорию Пеано. Эти аксиомы заданы некоторым списком. В качестве элементов списка стоят аксиомы или схемы аксиом (пример схемы аксиом - любая аксиома логики - там используются формульные переменные). И у нас есть быстрый способ добавления в любой такой список новой аксиомы - после чего получается новый список аксиом с теми же свойствами списка. Способ добавления аксиомы обозначим как $\operatorname{AddAks}(Aks, X)$ - в результате работы этот алгоритм вернет список аксиом $Aks$, расширенный аксиомой $X$. Иногда для простоты я буду писать $Aks + X$ вместо приведенной формулы - когда ясно, что речь об аксиомах.

2. В качестве проверяемого слова будем рассматривать пару текстов - список аксиом из п. 1 и $A()$ – записанный на языке теории текст алгоритма.

3. В качестве слова-свидетеля будем рассматривать текст доказательства для $A() = i$. Где $i$ – некоторое число (можно считать, что число записано в десятичном представлении, но тут это не принципиально). Если имеется слово $x$ и слово-свидетель $y$, то, как известно из логики, можно при помощи алгоритма автоматической проверки доказательств $R1(Aks, x, y)$ за полиномиальное время (число шагов) $P1y(|y|+|Aks|)$ от размеров $y$ и $Aks$ проверить, доказывает ли $y$ какое-то равенство $A() = i$ для $x$ на базе аксиом Пеано, расширенных аксиомами $Aks$. На размер $y$ накладывается стандартное для $NP$ ограничение некоторым полиномом $P1x(|x| + |Aks|)$. Разумеется, если в качестве $x$ и/или $y$ и/или $Aks$ выступает какой-то бессмысленный текст, то $R1(Aks, x, y)$ возвращает «ложь».

4. Помимо проверки $R1$ делается еще проверка $R2(Aks, x)$, выявляющая доказательство противоречия $1=0$ - если оно имеется - среди всех доказательств размером до $P1x(|x| + |Aks|)$ включительно. И это тоже - полиномиальная проверка с количеством шагов $P2y(|y|+|Aks|)$, где $|y| < P1x(|x| + |Aks|)$. Такая сложная проверка имеет полиномиальное решение по допущению нашего доказательства «от противного», что задачу из $NP_{def}$ можно свести к задаче из класса $P$.

5. Проверяемое слово (пара $Aks$ и $\overline{\operatorname{A}()}$) считается подтвержденным словом-свидетелем $y$, если положительный результат выдала проверка $R1$, а проверка $R2$ выдала отрицательный результат. В противном случае слово-свидетель не подтвердило проверяемое слово. Всю проверку назовём $R(Aks, x, y)$, она эквивалентна выражению $(R1 \wedge \neg R2)$ и время её работы ограничено полиномом $Py(|y|)$, где $|y| < Px(|x|+|Aks|)$.

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

Замечание 1. Как будет видно из доказательства - можно радикально ослабить проверку на противоречия в п.4. По сути, достаточно проверять непротиворечивость в аксиомах, но только вычислив внутри них некоторые алгоритмы (полиномиально быстрые, а точнее - $\operatorname{diag}()$). Ну, вроде замены предиката $P(f(a))$ на $P(i)$, где $f(a) = i$. И еще из полученного в аксиомах результатов сделать новый, применив 1 раз правило вывода $MP$. Так что в п. 4 избыточная перестраховка по принципу «Если рядом воробей, мы готовим пушку».

Доказательство.

Доказываю с конца прошлого доказательства (см. предыдущую запись post960183.html#p960183 ).

Если решение $Mt$ хоть для одного набора непротиворечивых аксиом $Aks + DiagKnockout(Aks)$ выдаст правильный результат: $\operatorname{Mt}(\operatorname{AddAks}(Aks, \overline{\operatorname{DiagKnockout}(Aks)}), \overline{\operatorname{AntiMt}(...)}) = knockout$, то, как было показано ранее - $Aks + \operatorname{DiagKnockout}(Aks)$ тогда непротиворечиво, а алгоритм $Mt$ тогда является неполным и $NP_{def} \ne P$.

Напоминаю, что «выдаст правильный результат» - это значит, сам алгоритм исполняется на указанных аргументах, в итоге останавливается и выдает соответствующий ($knockout$) результат. И вот только в этом случае он соответствует аксиоме $\operatorname{DiagKnockout}(Aks)$.
Но раз мы ориентируемся на встроенную проверку нашей задачи, то нас интересует непротиворечивость условная - чтобы проверка $R2$ не дала положительную реакцию в системе аксиом $Aks + \operatorname{DiagKnockout}(Aks)$ при проверке вывода для $\overline{\operatorname{ AntiMt }(\ldots)}$, которую находит наш алгоритм $Mt$, когда он работает вот так (знак неравенства):

$\operatorname{Mt}(\operatorname{AddAks}(Aks, \overline{\operatorname{DiagKnockout}(Aks)}), \overline{\operatorname{AntiMt}(\ldots)}) \ne knockout$

Иначе – если он выдаст $knockout$ даже в противоречивой, но при этом в условно-непротиворечивой теории – это все равно будет неполнотой: Раз по условиям нашей проверки $R2$ выдаёт «непротиворечиво», то тут возможен значимый (не $knockout$) прогноз про результат $\operatorname{ AntiMt }(\ldots)$ и он легко получается из аксиомы диагонального нокаута.
То есть, чтобы $Mt$ был полным решением из класса $P$ для нашей задачи из класса $NP_{def}$ необходимо, чтобы он всегда выдавал значимый (не $knockout$) прогноз для $\operatorname{ AntiMt }(\ldots)$, когда $R2$ «не заметит» что это противоречиво. А это значит, что теория вида $Aks + \operatorname{DiagKnockout}(Aks)$ всегда противоречива (значимый результат - это противоречие с аксиомой диагонального нокаута), когда $R2$ не замечает этого при проверке доказательства для $\operatorname{ AntiMt }(\ldots)$.

Этот вывод следует из того, что $Mt$ в разбираемом случае всегда нарушает $\operatorname{DiagKnockout}(Aks)$ ради полноты прогнозирования $\operatorname{ AntiMt }(\ldots)$, если только проверка $R2$ не объявляет любое подходящее по размерам доказательство для $\operatorname{ AntiMt }(\ldots)$ ложным в системе аксиом $Aks + \operatorname{DiagKnockout}(Aks)$.
То есть, если вдруг $Mt$ «соглашается» с $\operatorname{DiagKnockout}(Aks)$, то система аксиом $Aks$ изначально была противоречивой, а вместе с истинной (раз $Mt$ «согласился» с $\operatorname{DiagKnockout}(Aks)$) аксиомой $\operatorname{DiagKnockout}(Aks)$ стала настолько очевидно противоречивой, что это «заметила» проверка $R2$.

Значит, истинным в стандартной интерпретации является следующее предложение:

1. $\operatorname{DiagKnockout}(Aks) \to (Aks \to (1=0) )$

Это выражение и означает, что если уж $Mt$ «сподобился» согласиться с аксиомой диагонального нокаута, то значит в теории явные противоречия.
Считаю нужным заметить - что мы для стандартной интерпретации пишем не аксиомы, а «факты жизни». И «факт жизни» в том, что уж если алгоритм $\operatorname{Mt}(\operatorname{AddAks}(Aks, \overline{\operatorname{DiagKnockout}(Aks)}), \overline{\operatorname{AntiMt}(\ldots)})$ вернул $knockout$ - то это значит, что он сработал как алгоритм и такой результат у него - независимо ни от каких теории. Это алгоритм, который зависит

от списка $Aks + \operatorname{DiagKnockout}(Aks)$ и текста $\overline{\operatorname{ AntiMt }(\ldots)}$

и не более того. И он возвращает конкретные результаты. И запись $\operatorname{DiagKnockout}(Aks)$ здесь означает, что этот конкретный результат - $knockout$. И «факт жизни» в том, что $Mt$ выдаст такой результат, только если теория $Aks + \operatorname{DiagKnockout}(Aks)$ будет противоречивой и это противоречие найдет $R2$. Что тоже означает вполне конкретную строку среди строк определенного вида («формальных выводов») и т.п.

И да, если уж даже $R2$ нашла противоречие, то оно там есть, поэтому про $R2$ можно не упоминать в логическом предложении.
Если кого-то смущает, что противоречие $(1=0)$ выявлено проверкой $R2$ для системы аксиом

$Aks + \operatorname{DiagKnockout}(Aks)$, то можно написать и так:
$\operatorname{DiagKnockout}(Aks) \to ((Aks \wedge \operatorname{DiagKnockout}(Aks))\to (1=0) )$

просто пункт 1 нашего доказательства эквивалентен данному предложению. Что легко сообразить по «истинности посылок» вложенных импликаций - если верна 1ая, то во второй посылке $\operatorname{DiagKnockout}(Aks)$ тоже верен и всё зависит от $Aks$. Да и вывести легко из тавтологии:

$[ A \to ((B \wedge A) \to C) ] \to [ A \to (B \to C) ]$

Итак,

1. $\operatorname{DiagKnockout}(Aks) \to (Aks \to (1=0) )$

2. $(\operatorname{DiagKnockout}(Aks) \wedge Aks) \to (1=0)$ из п. 1 и тавтологии $(A \to (B \to C)) \to ((A \wedge B) \to C)$

3. $(1 \ne 0) \to \neg (\operatorname{DiagKnockout}(Aks) \wedge Aks)$ из п. 2 и контрапозиции $(A \to B) \to (\neg B \to \neg C)$

4. $\neg (DiagKnockout(Aks) \wedge Aks)$ из п. 3 по правилу MP из верной посылки $(1\ne 0)$

5. $\neg \operatorname{DiagKnockout}(Aks) \vee \neg Aks$ из п.4 по правилу раскрытия отрицания конъюнкции.

Собственно, интересен п. 4. Как только мы ставим диагональный нокаут - мы получаем новую (расширенную на $\operatorname{DiagKnockout}(Aks)$) противоречивую аксиоматику. Она будет противоречивой либо из-за изначальной противоречивости $Aks$, либо из-за тотальной «битвы за полноту» со стороны $Mt$ с его нарушением аксиомы $\operatorname{DiagKnockout}(Aks)$.
А вот из 5 пункта пишем эквивалентное представление (в соответствии с представлением импликации через дизъюнкцию):

6. $Aks \to \neg \operatorname{DiagKnockout}(Aks)$

А последний пункт означает, что при любой аксиоматике новая аксиома

$\neg \operatorname{DiagKnockout}(Aks)$

никак не влияет на противоречивость теории, потому что изначально выводится из неё. И, значит, добавляя её к непротиворечивой теории – мы получаем непротиворечивую теорию.
Тут и происходит ключевой «фокус» нашего доказательства - глубоко спрятанная (от $R2$) в длинных логических выводах «заготовка» для противоречия вытаскивается на самую вершину – в состав аксиом!

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

7. $X \to \neg \operatorname{DiagKnockout}(X)$

Собственно, мы и оперировали схемами аксиом – у нас $Aks$ были произвольными. Схемами аксиом оперируют в логике, например. Но поскольку мы оперировали набором аксиом как их конъюнкцией, то надо уточнить про схемы аксиом в таких конъюнкциях.
Схема аксиом с формульными переменными - истина для всех возможных подстановок в неё и в этом смысле она сама является конъюнкцией. Другое дело, что если среди аксиом несколько схем аксиом, то вместо отделенных друг от друга подстановок мы будем получать в качестве истины конъюнкцию для одной и той же подстановки из разных схем аксиом - если в схемах используются одинаковые обозначения для формульных переменных.
Если бы там было по одной подстановке в схеме, то это не важно, потому что конъюнкцию можно поделить на составляющие тавтологией $(A \wedge B) \to A$, но чтоб не думать, как там будет, когда подстановка в схеме не одна и есть различные формульные переменные - проще просто использовать в каждой схеме аксиом только те формульные переменные, которые не используются в другой схеме аксиом. Что, будем считать, соблюдается.
И тогда после добавления к истинному набору аксиом

$Aks + (X \to \neg \operatorname{DiagKnockout}(X))$ аксиомы диагонального нокаута:

8. $\operatorname{DiagKnockout}( Aks + (X \to \neg \operatorname{DiagKnockout}(X)) )$ – новая аксиома

Мы можем получить из $Aks + (X \to \neg \operatorname{DiagKnockout}(X))$ - старых аксиом в составе новой теории - вывод для

9. $\neg \operatorname{DiagKnockout}( Aks + (X \to \neg \operatorname{DiagKnockout}(X)) )$ - получено из исходных аксиом при помощи 7 и правила вывода MP, который убирает посылку импликации - аксиомы $Aks + (X \to \neg \operatorname{DiagKnockout}(X))$. И остается только заключение - представленное в п.9.

В схему аксиом можно подставлять любые аксиомы – в том числе и из другой теории, и из исходной до расширения. Просто для аксиом другой теории не удалось бы отбросить посылку импликации (исходные аксиомы) и оставить одно заключение из п.9.

Пункты 8 и 9 - противоречие, «видимое» даже и для $R2$ (Хотя строго говоря, нужна ещё часть вывода для получения 1=0, но это выводится из тавтологии $(A \wedge \neg A) \to (1=0)$ ).

И из-за $R2$ все доказательства для новой теории с $\operatorname{DiagKnockout}()$ будут ложными. При том, что до добавления $\operatorname{DiagKnockout}()$ теория была непротиворечивой и из гипотезы доказательства должна была при расширении на $\operatorname{DiagKnockout}()$ остаться условно-непротиворечивой (не «уличенной» $R2$), а $Mt$ должен был выдавать значимый прогноз для $\operatorname{ AntiMt }()$.

А теперь оказалось, что любой значимый прогноз отвергается из-за $R2$ в новой теории и - таким образом - нарушение $\operatorname{DiagKnockout}()$ оказывается явно (для $R2$) противоречивым, а алгоритм $Mt$ - некорректным, потому что он должен выдавать значимый прогноз для $\operatorname{ AntiMt }(\ldots)$ в данной теории по гипотезе доказательства, что противоречит $R2$. И гипотеза доказательства о полноте $Mt$ оказалась ошибочной.

Теорема доказана.

Самое интересное («обстоятельство $NP_{spirit}$») не поместилось - поэтому выложу, когда форум позволит (через 1 час, вроде).

[dmitgu]

Замечание 2. В отличие от моего первого формального доказательства тут ( post956292.html#p956292 ) я теперь рассматривал одну задачу из $NP$. В первом доказательстве я рассматривал разные задачи из $NP$, соответствующие математическим теориям – противоречивым и непротиворечивым. И у них были разные встроенные алгоритмы проверки. Так как непротиворечивые теории имеют свои модели и их доказательства истинны для каких-то миров (пусть искусственных), а противоречивые «теории» истинных доказательств не имеют.

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

Замечание 3. Построенная сейчас задача из $NP_{def}$ чем-то напоминает наши естественные «теории» для обычной жизни. Эти теории не являются строго непротиворечивыми, но на какую-то глубину проверки противоречий мы идём, у нас есть рефлексия (вариант диагонализации) и эта система в некотором смысле «логически устойчива» - в процессе доказательства будет показано, что постоянная ошибка, в конечном счете, обнаруживается. Да, и даже $NP$-природа построенной задачи имеет отношение к нашим подходам – мы не будем искать сверхдлинные решения, если вопрос не слишком важный. Просто мы добавляем в «размер задачи» всякие проблемы и выгоды, связанные с задачей. И чем крупнее размер задачи (по проблемам и выгодам) – тем больше длина решений, на поиск которых мы готовы. Кроме проблем типа нехватки времени, которая может сокращать размер (и качество) поиска.

Незавершенные вычисления

А теперь - объяснение парадокса, как мы смогли обойтись обнаружением противоречия внутри аксиом, почти не выйдя за их пределы в процессе проверки. Почему алгоритм поиска просчитывается короткой (в сравнении с ним) в смысле времени работы проверкой и в чём принципиальное упущение в теореме Кука.

Объяснение, которое пришло мне в голову - незавершенные вычисления. Пример, который приводился при постановке задачи в Замечании 1:

«вычислив внутри них некоторые алгоритмы... Ну, вроде замены предиката $P(f(a))$ на $P(i)$, где $f(a) = i$»

Так если задуматься - при погружении все дальше в доказательства и размеры аксиом - нам надо всё большее время для завершения таких подстановок и подобных им. И это связано с проблемой остановки, которая неразрешима. И не сделав необходимые вычисления - ты ничего не добьешься в смысловом шаге. Если твой запас длины доказательств кончился, когда $i$ ещё не посчитано -весь путь в направлении расчета $i$ оказывается бессмысленным. И ты не можешь заранее знать - вообще говоря - будет ли конец в данном направлении.
И построение доказательств придется вести сразу «во всех направлениях», потому что иначе не ясно, где будут сделаны законченные смысловые шаги. Завершаемые алгоритмы кончаются, нескончаемые - создают проблемы вечно. И чем дальше мы погружаемся в пучины аксиом, тем меньше альтернатив этой бездонной неразрешимости.

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

И тут становится понятно упущение в теореме Кука - там в доказательстве сводят сложные алгоритмы к решению задачи ДНФ. Но никакого сведения нет, потому что отдельные уравнения ДНФ обычно не соответствуют «единице смысла» исходной задачи. Кроме, конечно, таких же элементарных «атомизированных» задач, как сама ДНФ. И если ты и можешь решить каждое отдельное уравнение, то вопрос - а какое из них является подходящим и согласованным с задачей в целом - куда более сложный.
И нельзя пренебречь тем, что «ну, это же только незавершенные смысловые единицы выпадают из процесса сведения», потому что незавершенные вычисления и «просто пограничные эффекты» в мире логики - это «почти всё».

Это как мысль, идея, исследование - протяженное во времени и пространстве явление, которое имеет смысловое значение лишь в целостности. Ясно, что мысль соответствует некоему материальному процессу в мозге, но ведь мы даже не в состоянии воспринять её частями. Ну, какую часть мысли несет левая верхняя извилина? Никакую. А вот в целом - проявление души и со своей «законченной единицей» из мира идей.

Поэтому я и выделил из задач типа $NP_{def}$ подтипы $NP_{atom}$ и $NP_{spirit}$. И второе к первому никак не сводится.
Совершенно не факт, что для ДНФ (задачи решения булевых уравнений) не будет найдено полиномиального решения. Но математические теории и задачи из NP на их основе – неизмеримо сложнее.

Получается, что наш мир очень «вязкий» в логическом отношении. Возможно, это объясняет, почему порой случаются «революции» в той или иной научной сфере - это если кому-то повезло обнаружить новый «тоннель разрешимости» и по нему устремляются массы исследователей, пока не достигнут очередного предела - то есть обычной среды - невероятно «вязкой» в смысловом отношении.

-- 17.01.2015, 10:48 --

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

7. $Х \to \neg \operatorname{DiagKnockout}(X)$

Это опечатка в доказательстве. Наверно, Икс не видно, потому что это русское X. Правильно:
7. $X \to \neg \operatorname{DiagKnockout}(X)$

[dmitgu]

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

Да и вывести легко из тавтологии:

$[ A \to ((B \wedge A) \to C) ] \to [ A \to (B \toC) ]$

Опечатка в доказательстве (вместо "to C" набрал "toC" в формуле). Правильно, разумеется, так:

$[ A \to ((B \wedge A) \to C) ] \to [ A \to (B \to C) ]$

[Deggial]

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

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

7. $Х \to \neg \operatorname{DiagKnockout}(X)$

Это опечатка в доказательстве. Наверно, Икс не видно, потому что это русское X. Правильно:
7. $X \to \neg \operatorname{DiagKnockout}(X)$

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

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

Да и вывести легко из тавтологии:

$[ A \to ((B \wedge A) \to C) ] \to [ A \to (B \toC) ]$

Опечатка в доказательстве (вместо "to C" набрал "toC" в формуле). Правильно, разумеется, так:

$[ A \to ((B \wedge A) \to C) ] \to [ A \to (B \to C) ]$

Формулы поправил

[Xaositect]

Прошу прощения за то, что выпал из дискуссии. Постараюсь на выходных прочитать и прокомметировать.

[dmitgu]

Deggial в сообщении #963683 писал(а):

Формулы поправил

Спасибо!

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

Прошу прощения за то, что выпал из дискуссии. Постараюсь на выходных прочитать и прокомметировать.

Спасибо Вам за внимание! Никакой спешки нет. У меня у самого сейчас отчетный период и следующие выходные могут быть основательно заняты работой. Поэтому не исключено, что может не смогу ответить сразу и/или хорошо. Но на следующей неделе постараюсь исправиться тогда :)

[m(Ax)]

С проблемой равенства этих классов вот какая заковыка. Есть такое понятие - релятивизация относительно оракула. Определение давать не буду, но попробую немного пояснить, что это такое. В качестве оракула можем взять любое подмножество натyральных чисел, обозначим его $A$. Алгоритм (в качестве определения алгоритма можно взять например машину Тюринга) с оракулом $A$ работает следующим образом: работает как обычный алгоритм, но кроме этого ему еще разрешается задавать вопросы к оракулу вида "$x\in A?$". Теперь, если у нас есть какая то теорема об алгоритмах, как правило, можно получить аналогичную теорему об алгоритмах с оракулом $A$, соответвующей заменой в формулировке и докзательстве. Это и назвыется релятивизацией относительно оракула $A$.

Используя алгоритмы с оракулом $A$ можно определить классы $P^A$ и $NP^A$. Так вот, есть теорема, что существуют такие оракулы $A$ и $B$, что $P^A=NP^A$, a $P^B\neq NP^B$.

Поэтому, если есть решение проблемы равны ли $P$ и $NP$, то сразу возникает вопрос: а какая часть решения не релятивизуется? Я не уверен есть ли примеры таких доказательств.

[dmitgu]

m(Ax) в сообщении #967275 писал(а):

есть теорема, что существуют такие оракулы $A$ и $B$, что $P^A=NP^A$, a $P^B\neq NP^B$

Вполне возможно - вопрос только разрешимы ли эти $A$ и $B$. Просто всё довольно сомнительно с самим классов $NP$ - из-за чего собственно и возникла львиная часть трудностей при поиске доказательства. Вот например - у нас есть неполиномиальный (пусть экспоненциальный) алгоритм проверки. Из него можно легко сделать полиномиальный! А именно - давайте добавим к каждому проверяемому слову "1111111111...111111111111" экспоненциального размера, который никак не будет влиять на результат - и все срастется. И вот в доказательстве Кука о сводимости это никак не отслеживается - если я правильно понимаю. Поэтому мне кажется разумным для начала аккуратно разобраться с классом $NP$ в связи с выявленными противоречиями, затем пересмотреть доказательства, а потом уже двигаться дальше.

Вот кстати, в моем доказательстве (?) есть случаи, когда аксиомы $Aks$ противоречивы. В этом случае ситуация становится по сути неполиномиальной - потому что любые доказательство заведомо ошибочны. И если мы отбрасываем эту не значимую часть проверяемого слова (проверяемые алгоритмы $A()$), то зависимость проверки от размера списка аксиом оказывается вполне себе неполиномиальной. В то же время алгоритм проверки ДНФ не имеет такого блока, который в каких-то случаях может "выродится" в неполиномиальный (при отбрасывании "вырожденных" частей проверяемого слова). Вот поэтому - если пытаться двигаться к формализации - я и выделяю подтипы у типа $NP_{def}$ - $NP_{atom}$ и $NP_{spirit}$. Но эта тема требует аккуратного обсуждения без спешки. Грубо говоря, мы берем стакан неполиномиальности, выливаем его в океан однообразия (не значимого) и говорим, что теперь у нас океан полиномиальности. Хотя при этом стакан неполиномиальности вполне себе выделяется в этом океане и плавает там как медуза

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

[m(Ax)]

Естественно, $A$ и $B$ неразрешимы, добавление разрешимого оракула не дает ничего нового. По поводу превращение алгоритма проверки в полиномиальный. Я пока не понимаю в чем противоречие. Пусть есть у нас язык $L$, слова которого проверяются, для простоты, за $2^{|p|}$ шагов. Построим язык $L'=\{p1^{2^{|p|}}\mid p\in L\}$. Он уже проверяется за полиномиальное от $2^{|p|}$ время. Это никак не влияет на участь $L$. И в чем проблема? Задача искусственно раздувается и становится полиномиальной, но этот полином от раздутых размеров.

[dmitgu]

m(Ax) в сообщении #967516 писал(а):

Построим язык $L'=\{p1^{2^{|p|}}\mid p\in L\}$. Он уже проверяется за полиномиальное от $2^{|p|}$ время. Это никак не влияет на участь $L$. И в чем проблема? Задача искусственно раздувается и становится полиномиальной, но этот полином от раздутых размеров.

Я неаккуратно выразился. Противоречием, на мой взгляд, является зависимость операций с $NP$ от предположения, что мы заранее знаем алгоритм проверки (в той же теореме Кука). А алгоритм может быть и неизвестным - я фактически играл на этом в первом формальном доказательстве тут - строя на базе непротиворечивых теорий один алгоритм проверки, а на базе противоречивых - другой. Что касается "раздувания до полиномиальности" - то формально противоречия вроде нет, но теряется сам принцип предпочтения задачам из NP как доступным для проверки. По сути определение делает их практически неотличимыми от задач с неполиномиальной проверкой. Хорошо, а если еще накрутить длину проверяемого слова экспоненциально и не-значимо - то тогда мы и решать их сможем полиномиально! Это что - тоже допустимо? И тоже эквивалентно? Но тогда $NP = P$ при таких подходах? Может тут и решается всё достаточно понятно - но картина кажется мне странной.

[m(Ax)]

Верно, сможем и решать. Собственно, то что приведено в предыдущем сообщении верно и для класса $P$ и $NP$. Еще раз, у нас есть задача $L$ которая не решается (проверяется) полиномиально и есть некоторая задача $L'$, построенная по задаче $L$, которая уже становится разрешимой (проверяемой) за полиномиальное время. Ну и что? Задачи не полиномиально эквивалетны. Как тут не исхитряться, построить решение для $L$ зависящее полиномиально от размеров $L$ не удается. А $L'$ это совершенно другая задача, пусть она решается хоть мнгновенно. Переход от конкретной задачи (слова) из $L$ к конкретной задаче (слову) из $L'$ занимает экспоненциальное время от размеров задачи из $L$, что мы будем дальше делать уже не имеет значения.

[dmitgu]

m(Ax) в сообщении #967966 писал(а):

Переход от конкретной задачи (слова) из $L$ к конкретной задаче (слову) из $L'$ занимает экспоненциальное время от размеров задачи из $L$, что мы будем дальше делать уже не имеет значения.

В принципе, мое доказательство (итоговое) на такой принятый подход и рассчитано, но в данном случае речь о более широком вопросе:

Какая разница, будет ли переход полиномиальный или нет относительно размеров задачи $L$, если итоговая задача $L'$ полиномиальна, считается - поэтому - приемлемой для вычисления и переход к ней относительно её размера - полиномиален?

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

С точки зрения инженерной, надо чтоб мы имели дело с "чистыми", а не "раздутыми" задачами из $NP$ и $P$. Например, для $NP$:

Надо чтоб произвольное проверяемое слово разбираемой массовой задачи нельзя было свести (полиномиально?) к паре $(A + B)$ - где $B$ - любое размера до $L$, и $L$ неполиномиально велик относительно $|A|$, но в смысле проверки от этого $B$ ничего не зависит.

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

[m(Ax)]

Как раз от значимой части время проверки (решения) будет зависеть экспоненциально. Оно полиномиально зависит от полного размера "раздутой" задачи, а размер как раз есть экпонента от размера значимой части. Так что и с инженерной точки зрения все хорошо. Как ждали долго проверки практической задачи так и будем долго ждать.

[dmitgu]

m(Ax) в сообщении #968064 писал(а):

Оно полиномиально зависит от полного размера "раздутой" задачи, а размер как раз есть экпонента от размера значимой части. ... Как ждали долго проверки практической задачи так и будем долго ждать.

Вот - долго ждать! Экспоненциально. А задача якобы теперь из $P$. А класс $P$ - якобы быстрый, поэтому такая классификация представляется не завершенной. Если уж "быстро", так "полиномиально" - и от значимой части.

Кстати, про оракула. Вот есть множество троек (ну, например записано при помощи канторовых пар) представленных одним числом каждая. И первый член тройки - текст алгоритма проверки, второй - проверяемое слово, а третий - слово-свидетель (если есть) или 0 (считаем что 0 не является словом свидетелем, к чему можно свести дело). Вот это ведь вполне решение для любой задачи из NP. Или я где-то выхолащиваю принцип оракула?