Копирую сюда свой пост с 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_def ≠ P.
Напоминаю, что «выдаст правильный результат» - это значит, сам алгоритм исполняется на указанных аргументах, в итоге останавливается и выдает соответствующий (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. И это делает очевидным NP ≠ 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 на их основе – неизмеримо сложнее.
Получается, что наш мир очень «вязкий» в логическом отношении. Возможно, это объясняет, почему порой случаются «революции» в той или иной научной сфере - это если кому-то повезло обнаружить новый «тоннель разрешимости» и по нему устремляются массы исследователей, пока не достигнут очередного предела - то есть обычной среды - невероятно «вязкой» в смысловом отношении.
