dmitgu (dmitgu) wrote,
dmitgu
dmitgu

NP_primitive ≠ P. Завершение доказательства (надеюсь)

Копирую сюда свой пост с dxdy.ru - http://dxdy.ru/post963495.html#p963495
Но последний раздел ("Незавершенные вычисления") я выложу туда чуть позже - пока их форум не пропускает - слишком большая запись.

Похоже, мне удалось избавиться от расширительного толкования «проверки корректности» из
предыдущей записи ( http://dxdy.ru/post960183.html#p960183 ) и - таким образом - дать доказательство для NP_primitive ≠ 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 (пусть непротиворечивая), расширяющая теорию Пеано. Эти аксиомы заданы некоторым списком. В качестве элементов списка стоят аксиомы или схемы аксиом (пример схемы аксиом - любая аксиома логики - там используются формульные переменные). И у нас есть быстрый способ добавления в любой такой список новой аксиомы - после чего  получается новый список аксиом с теми же свойствами списка. Способ добавления аксиомы обозначим как 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 и «A()») считается подтвержденным словом-свидетелем y, если положительный результат выдала проверка R1, а проверка R2 выдала отрицательный результат. В противном случае слово-свидетель не подтвердило проверяемое слово. Всю проверку назовём R(Aks, x, y), она эквивалентна выражению (R1 Ù ~ R2) и время её работы ограничено полиномом Py(|y|), где |y| < Px(|x|+|Aks|).

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

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

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

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

Если решение Mt хоть для одного набора непротиворечивых аксиом Aks + DiagKnockout(Aks) выдаст правильный результат:  Mt(AddAks(Aks, «DiagKnockout(Aks)»), «AntiMt(...)») = knockout, то, как было показано ранее - Aks + DiagKnockout(Aks) тогда непротиворечиво, а алгоритм Mt тогда является неполным и NP_defP.

Напоминаю, что «выдаст правильный результат» - это значит, сам алгоритм исполняется на указанных аргументах, в итоге останавливается и выдает соответствующий (knockout) результат. И вот только в этом случае он соответствует аксиоме DiagKnockout(Aks).

Но раз мы ориентируемся на встроенную проверку нашей задачи, то нас интересует непротиворечивость условная - чтобы проверка R2 не дала положительную реакцию в системе аксиом Aks + DiagKnockout(Aks) при проверке вывода для «AntiMt(...)», которую находит наш алгоритм Mt, когда он работает вот так (знак неравенства):

Mt(AddAks(Aks, «DiagKnockout(Aks)»), «AntiMt(...)») knockout

Иначе – если он выдаст knockout даже в противоречивой, но при этом в условно-непротиворечивой теории – это все равно будет неполнотой: Раз по условиям нашей проверки R2 выдаёт «непротиворечиво», то тут возможен значимый (не knockout) прогноз про результат AntiMt(...) и он легко получается из аксиомы диагонального нокаута.

То есть, чтобы Mt был полным решением из класса P для нашей задачи из класса NP_def необходимо, чтобы он всегда выдавал значимый (не knockout) прогноз для AntiMt(...), когда R2 «не заметит» что это противоречиво. А это значит, что теория вида Aks + DiagKnockout(Aks) всегда противоречива (значимый результат - это противоречие с аксиомой диагонального нокаута), когда R2 не замечает этого при проверке  доказательства для AntiMt(...).

Этот вывод следует из того, что Mt в разбираемом случае всегда нарушает DiagKnockout(Aks) ради полноты прогнозирования AntiMt(...), если только проверка R2 не объявляет любое подходящее по размерам доказательство для AntiMt(...) ложным в системе аксиом Aks + DiagKnockout(Aks).

То есть, если вдруг Mt «соглашается» с DiagKnockout(Aks), то система аксиом Aks изначально была противоречивой, а вместе с истинной (раз Mt «согласился» с DiagKnockout(Aks)) аксиомой DiagKnockout(Aks) стала настолько очевидно противоречивой, что это «заметила» проверка R2.

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

1. DiagKnockout(Aks) => (Aks => (1=0) )

Это выражение и означает, что если уж Mt «сподобился» согласиться с аксиомой диагонального нокаута, то значит в теории явные противоречия.

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

списка  Aks + DiagKnockout(Aks) и текста  «AntiMt(...)»

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

И да, если уж даже R2 нашла противоречие, то оно там есть, поэтому про R2 можно не упоминать в логическом предложении.

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

Aks + DiagKnockout(Aks), то можно написать и так:

DiagKnockout(Aks) => ((Aks Ù DiagKnockout(Aks))=> (1=0) )

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

[ A => ((B Ù A) => C) ] => [ A => (B => C) ]

Итак,

1. DiagKnockout(Aks) => (Aks => (1=0) )

2. (DiagKnockout(Aks) Ù Aks) => (1=0) из п. 1 и тавтологии (A => (B => C)) => ((A Ù B) => C)

3. (1≠0) => ~(DiagKnockout(Aks) Ù Aks))  из п. 2 и контрапозиции   (A => B) => (~B => ~C)

4. ~(DiagKnockout(Aks) Ù Aks) из п. 3 по правилу MP из верной посылки (1≠0)

5. ~DiagKnockout(Aks) Ú ~Aks из п.4 по правилу раскрытия отрицания конъюнкции.

Собственно, интересен п. 4. Как только мы ставим диагональный нокаут - мы получаем новую (расширенную на DiagKnockout(Aks)) противоречивую аксиоматику. Она будет противоречивой либо из-за изначальной противоречивости Aks, либо из-за тотальной «битвы за полноту» со стороны Mt с его нарушением аксиомы DiagKnockout(Aks).

А вот из 5 пункта пишем эквивалентное представление (в соответствии с представлением импликации через дизъюнкцию):

6. Aks => ~DiagKnockout(Aks)

А последний пункт означает, что при любой аксиоматике новая аксиома  ~DiagKnockout(Aks) никак не влияет на противоречивость теории, потому что изначально выводится из неё. И, значит, добавляя её к непротиворечивой теории – мы получаем непротиворечивую теорию.

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

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

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

Поэтому записываем истинную схему аксиом:

7. Х => ~DiagKnockout(X)

Собственно, мы и оперировали схемами аксиом – у нас Aks были произвольными. Схемами аксиом оперируют в логике, например. Но поскольку мы оперировали набором аксиом как их конъюнкцией, то надо уточнить про схемы аксиом в таких конъюнкциях.

Схема аксиом с формульными переменными - истина для всех возможных подстановок в неё и в этом смысле она сама является конъюнкцией. Другое дело, что если среди аксиом несколько схем аксиом, то вместо отделенных друг от друга подстановок мы будем получать в качестве истины конъюнкцию для одной и той же подстановки из разных схем аксиом - если в схемах используются одинаковые обозначения для формульных переменных.

Если бы там было по одной подстановке в схеме, то это не важно, потому что конъюнкцию можно поделить на составляющие тавтологией (A Ù B) => A, но чтоб не думать, как там будет когда подстановка в схеме не одна и есть различные формульные переменные - проще просто использовать в каждой схеме аксиом только те формульные переменные, которые не используются в другой схеме аксиом. Что, будем считать, соблюдается.

И тогда после добавления к истинному набору аксиом

Aks + (X =>~DiagKnockout(X)) аксиомы диагонального нокаута:

8. DiagKnockout(Aks + (X =>~DiagKnockout(X)) ) – новая аксиома

Мы можем получить из (Aks) + (X =>~DiagKnockout(X)) - старых аксиом в составе новой теории -вывод для

9. ~DiagKnockout( Aks + (X =>~DiagKnockout(X)) ) - получено из исходных аксиом при помощи 7 и правила вывода MP, который убирает посылку импликации - аксиомы Aks + (X =>~DiagKnockout(X)) ). И остается только заключение - представленное в п.9.

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

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

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

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

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

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

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

Из этого понятно, что в понимании класса 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 на их основе – неизмеримо сложнее.

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

Tags: NP≠P дискуссии, ЖЖвЖЖ математика
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments