Я устал, я не ухожу (с) почти Ельцин
Пардон, что долго молчал, но сейчас отчётный период и нет возможности сосредоточиться на математике кроме некоторых выходных. Да и трудно даётся решение вопросов не о смысле, а о форме его подачи (формализация), но это необходимо, конечно. Поэтому, чтобы не тянуть – изложу сейчас то, что готово.
Формулирую, что такое
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
– в деталях:
![$\forall \operatorname{Sol}(...) \forall p_+ (...) \exists AntiSol:$ $\forall \operatorname{Sol}(...) \forall p_+ (...) \exists AntiSol:$](https://dxdy-03.korotkov.co.uk/f/2/7/2/272dbab43733d6d76209a6c283e8ca0282.png)
![$\vee ( \exists y: L(\overline{AntiSol}, y) = 1 \& N_L \le p(|\overline{AntiSol}|) \& (\operatorname{Sol}(\overline{AntiSol}) \ne 1 \vee N_{Sol} > p_+ (|\overline{AntiSol}|) ) )$ $\vee ( \exists y: L(\overline{AntiSol}, y) = 1 \& N_L \le p(|\overline{AntiSol}|) \& (\operatorname{Sol}(\overline{AntiSol}) \ne 1 \vee N_{Sol} > p_+ (|\overline{AntiSol}|) ) )$](https://dxdy-03.korotkov.co.uk/f/e/4/2/e4220b96506e856818644a83de55fe2e82.png)
Тут
![$\operatorname{Sol}(...)$ $\operatorname{Sol}(...)$](https://dxdy-04.korotkov.co.uk/f/3/c/0/3c0350ef9a02f89da7355998f4a5d81c82.png)
– это алгоритм-решение, который должен был бы представлять данный язык в классе
![$\mathbb{P}$ $\mathbb{P}$](https://dxdy-01.korotkov.co.uk/f/8/6/5/865a2c771b7419b8742c1a4a04cc558482.png)
.
![$L(...,...)$ $L(...,...)$](https://dxdy-01.korotkov.co.uk/f/4/1/4/41424d6f89fe7761dd3d37bae0287eca82.png)
– это алгоритм проверки, который представляет данный язык в классе
![$\mathbb{NP}$ $\mathbb{NP}$](https://dxdy-01.korotkov.co.uk/f/4/7/b/47bfc2169c08d10e14fd91da7fa6aff982.png)
.
![$N_L$ $N_L$](https://dxdy-03.korotkov.co.uk/f/6/9/e/69e74dc491688989036f2322d173249882.png)
и
![$N_{Sol}$ $N_{Sol}$](https://dxdy-02.korotkov.co.uk/f/d/b/4/db40e9f5703575ff1abb30d9990bc62a82.png)
– время работы соответствующих алгоритмов.
При этом:
![$\forall \operatorname{Sol}(...) ... \operatorname{Sol}(a) = ...$ $\forall \operatorname{Sol}(...) ... \operatorname{Sol}(a) = ...$](https://dxdy-01.korotkov.co.uk/f/0/1/e/01ecf636fbb36fca07810fdf84b5583682.png)
- это я не «доигрался» до логики 2-го порядка, а это условное сокращение для записи вида
где алгоритм
![$\operatorname{Run}(x, a)$ $\operatorname{Run}(x, a)$](https://dxdy-03.korotkov.co.uk/f/a/d/7/ad79cc8f48276e24ce557ce2f5c02a0d82.png)
– это «универсальный алгоритм», который исполняет программный код из первого аргумента, передавая ему в качестве аргументов всё, начиная со 2-го аргумента в
![$\operatorname{Run}(...)$ $\operatorname{Run}(...)$](https://dxdy-04.korotkov.co.uk/f/3/8/9/389d5d2fe15e3246f96037fce901865982.png)
.
впрочем и последняя формула – тоже сокращение для:
![$\forall x ( \operatorname{IsAlg}(x) \& ... \operatorname{Run}(x, a) = ... )$ $\forall x ( \operatorname{IsAlg}(x) \& ... \operatorname{Run}(x, a) = ... )$](https://dxdy-04.korotkov.co.uk/f/b/c/5/bc55b6dd27cfda2e61d46f7b2cb0342d82.png)
.
Где
![$\operatorname{IsAlg}(x)$ $\operatorname{IsAlg}(x)$](https://dxdy-02.korotkov.co.uk/f/9/8/d/98d96a7526ac83bf4dacb365ca81199a82.png)
– это «условная компиляция», которая проверяет, действительно ли в
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
программный код в нужном формате или нечто ошибочное.
Как побочный эффект моего исследования вопроса – был найден способ свести вопрос о
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
к второй части детального представления этого
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
. А именно – Если будет доказана вторая часть
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
:
![$\forall \operatorname{Sol}(...) \forall p_+ (...) \exists AntiSol:$ $\forall \operatorname{Sol}(...) \forall p_+ (...) \exists AntiSol:$](https://dxdy-03.korotkov.co.uk/f/2/7/2/272dbab43733d6d76209a6c283e8ca0282.png)
![$( \exists y: L(\overline{AntiSol}, y) = 1 \& N_L \le p(|\overline{AntiSol}|) \& (\operatorname{Sol}(\overline{AntiSol}) = 0 \vee N_{Sol} > p_+ (|\overline{AntiSol}|) ) )$ $( \exists y: L(\overline{AntiSol}, y) = 1 \& N_L \le p(|\overline{AntiSol}|) \& (\operatorname{Sol}(\overline{AntiSol}) = 0 \vee N_{Sol} > p_+ (|\overline{AntiSol}|) ) )$](https://dxdy-01.korotkov.co.uk/f/4/1/a/41a00dec32c71595a5f97d7eee5ebd6d82.png)
то будет доказано и
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
. А
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
построены так, что заведомо известно, что для корректного
![$Sol(\overline{AntiSol})$ $Sol(\overline{AntiSol})$](https://dxdy-02.korotkov.co.uk/f/1/2/b/12b97bb41bab9e34bff1bf9006c6dd1882.png)
верно:
![$Sol(\overline{AntiSol}) = 0$ $Sol(\overline{AntiSol}) = 0$](https://dxdy-04.korotkov.co.uk/f/3/5/3/3537ba4cb8c8f1dcb435c2391f68fa4382.png)
Последнее позволяет не рассматривать 1-ю часть детального представления для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
. При этом эти
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
вовсе не какие-то заведомо недоказуемые утверждения, а как раз заведомо доказуемые при результате алгоритма-проверки
![$Sol(\overline{AntiSol}) = 0$ $Sol(\overline{AntiSol}) = 0$](https://dxdy-04.korotkov.co.uk/f/3/5/3/3537ba4cb8c8f1dcb435c2391f68fa4382.png)
, и вопрос только в размере доказательства.
Точнее: верно
![$Sol(\overline{AntiSol}) = 0$ $Sol(\overline{AntiSol}) = 0$](https://dxdy-04.korotkov.co.uk/f/3/5/3/3537ba4cb8c8f1dcb435c2391f68fa4382.png)
, а иначе будет выполнена 1-я часть детального представления (так построено утверждение
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
):
Вернемся теперь от побочной линии к основной.
Перепишем детальное представление для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
в новом виде:
![$\forall \operatorname{Sol}(..., ...) \forall p_+(..., ...) \exists s \exists t \exists a = \overline{\operatorname{Sol}(..., ...)}:$ $\forall \operatorname{Sol}(..., ...) \forall p_+(..., ...) \exists s \exists t \exists a = \overline{\operatorname{Sol}(..., ...)}:$](https://dxdy-03.korotkov.co.uk/f/a/4/8/a48dc5f753284fcd350dff5eef24294782.png)
![$\vee ( \exists y: L(t, a, s, y) = 1 \& N_L \le p(|t|, |s|) \& (\operatorname{Sol}(|t|, |s|) \ne 1 \vee N_{Sol} > p_+(|t|, |s|) ) )$ $\vee ( \exists y: L(t, a, s, y) = 1 \& N_L \le p(|t|, |s|) \& (\operatorname{Sol}(|t|, |s|) \ne 1 \vee N_{Sol} > p_+(|t|, |s|) ) )$](https://dxdy-02.korotkov.co.uk/f/5/7/a/57affdddb411af76db0f954fb82cd2b182.png)
.
Мы добавили к слову часть
![$s$ $s$](https://dxdy-03.korotkov.co.uk/f/6/f/9/6f9bad7347b91ceebebd3ad7e6f6f2d182.png)
– это ничего не меняет в принципе (просто разбили слово на 2 части, где новая часть ничего не несет, кроме возможности увеличить размер допустимых для рассмотрения сертификатов). Ещё мы обозначили здесь переменной
![$t$ $t$](https://dxdy-01.korotkov.co.uk/f/4/f/4/4f4f4e395762a3af4575de74c019ebb582.png)
«опровергающее утверждение» вместо обозначения
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
– так как это обозначение потребуется нам в дальнейшем для специального случая и будет обозначать некоторые конкретные «сконструированные» утверждение. Но ещё мы включили явную зависимость алгоритма проверки от того алгоритма-решения, к которому эта проверка относится:
У нас появилась часть
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
– содержащая программный код. Для одних слов она – сертификат, а для других – часть слова. И тоже, вроде, ничего принципиального – мы можем взять любой язык из класса
![$\mathbb{NP}$ $\mathbb{NP}$](https://dxdy-01.korotkov.co.uk/f/4/7/b/47bfc2169c08d10e14fd91da7fa6aff982.png)
с «классическим» алгоритмом проверки и добавить в этот алгоритм такую часть
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
, от которой ничего не зависит, кроме требования, чтобы к размеру сертификата (при расчете ограничений) добавлялся ещё и её размер. Но мы этим не ограничимся, разумеется, и рассмотрим язык не с таким слегка изменённым «квазиклассическим» алгоритмом проверки.
Ещё один нюанс – полиномы
![$p(|t|, |s|)$ $p(|t|, |s|)$](https://dxdy-03.korotkov.co.uk/f/a/9/5/a954a34b59d106c357463da50dbfb91782.png)
и
![$p_+(|t|, |s|)$ $p_+(|t|, |s|)$](https://dxdy-04.korotkov.co.uk/f/7/4/e/74e3826abf4bcf01e866a5e6878c2c3b82.png)
могут в некоторых случаях иметь степень ноль при аргументе
![$|s|$ $|s|$](https://dxdy-03.korotkov.co.uk/f/2/2/d/22dedd40b9198c21ce6132f6c0da79a882.png)
, если соответствующее им слово не будет зависеть от размера
![$|s|$ $|s|$](https://dxdy-03.korotkov.co.uk/f/2/2/d/22dedd40b9198c21ce6132f6c0da79a882.png)
, но это будет разбираться отдельно далее. Не принципиален для дальнейшего рассмотрения вопрос о зависимости
![$p(|t|, |s|)$ $p(|t|, |s|)$](https://dxdy-03.korotkov.co.uk/f/a/9/5/a954a34b59d106c357463da50dbfb91782.png)
ещё и от
![$|a|$ $|a|$](https://dxdy-04.korotkov.co.uk/f/3/6/7/36781718771d1427f81e624c36760b2582.png)
: Мы будем рассматривать такие
![$t$ $t$](https://dxdy-01.korotkov.co.uk/f/4/f/4/4f4f4e395762a3af4575de74c019ebb582.png)
, размер которых больше размера
![$|a|$ $|a|$](https://dxdy-04.korotkov.co.uk/f/3/6/7/36781718771d1427f81e624c36760b2582.png)
. Поэтому ограничение в любом случае оказывается в пределах
![$p(|t|, |s|)$ $p(|t|, |s|)$](https://dxdy-03.korotkov.co.uk/f/a/9/5/a954a34b59d106c357463da50dbfb91782.png)
.
Напоминаю, что
![$\exists a = \overline{\operatorname{Sol}(..., ...)}$ $\exists a = \overline{\operatorname{Sol}(..., ...)}$](https://dxdy-04.korotkov.co.uk/f/b/3/6/b36acc531c3843da730ac0f7debd83a882.png)
в логике – это аналог подстановки, так как
![$\exists x = b: A(x) \Leftrightarrow A(b)$ $\exists x = b: A(x) \Leftrightarrow A(b)$](https://dxdy-04.korotkov.co.uk/f/f/5/5/f554b8b1720ddcc7bb3344de911851f482.png)
.
При этом обозначение
![$\exists x = b: A(x)$ $\exists x = b: A(x)$](https://dxdy-03.korotkov.co.uk/f/e/7/1/e71dde973b5cfe894a72f126ad10ea8c82.png)
я использую в качестве сокращения для более правильного (но в котором больше скобок) обозначения:
![$\exists x (x = b \& A(x))$ $\exists x (x = b \& A(x))$](https://dxdy-02.korotkov.co.uk/f/d/c/8/dc8ef23aacca27ebcc77bc5d2306a63682.png)
.
В свете последнего детального представления для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
отмечу, что спецификой в реализации языка
![$LS$ $LS$](https://dxdy-02.korotkov.co.uk/f/d/c/1/dc173468919a4ca5a669690ff6b8748982.png)
является вот что: Часть данных, соответствующих программному коду алгоритма-решения
![$\overline{\operatorname{Sol}(... , ...)}$ $\overline{\operatorname{Sol}(... , ...)}$](https://dxdy-03.korotkov.co.uk/f/6/9/1/6910be30d79c0ecf07dccab36ffa34f882.png)
, является частью одного слова и частью сертификата для другого слова. И при этом те слова вида:
![$t, s$ $t, s$](https://dxdy-03.korotkov.co.uk/f/a/a/5/aa522481c54066df939cb8d6f2fb8cf082.png)
которые алгоритм
![$\operatorname{Sol}(... , ...)$ $\operatorname{Sol}(... , ...)$](https://dxdy-04.korotkov.co.uk/f/f/6/d/f6d3eefc1f173df060270b7841e30c3d82.png)
может подтвердить, как принадлежащие языку
![$LS$ $LS$](https://dxdy-02.korotkov.co.uk/f/d/c/1/dc173468919a4ca5a669690ff6b8748982.png)
, полностью соответствуют наличию подтверждающих сертификатов вида
![$a, y$ $a, y$](https://dxdy-01.korotkov.co.uk/f/8/6/f/86fa81e819782bb5d50f9f307802540f82.png)
, где
![$a = \overline{\operatorname{Sol}(... , ...)}$ $a = \overline{\operatorname{Sol}(... , ...)}$](https://dxdy-04.korotkov.co.uk/f/f/3/5/f35dd877f594e3bc52ef9b4c4212718782.png)
И, таким образом, возможность алгоритма-решения
![$\operatorname{Sol}(... , ...)$ $\operatorname{Sol}(... , ...)$](https://dxdy-04.korotkov.co.uk/f/f/6/d/f6d3eefc1f173df060270b7841e30c3d82.png)
подтвердить принадлежность языку
![$LS$ $LS$](https://dxdy-02.korotkov.co.uk/f/d/c/1/dc173468919a4ca5a669690ff6b8748982.png)
слова
![$t, s$ $t, s$](https://dxdy-03.korotkov.co.uk/f/a/a/5/aa522481c54066df939cb8d6f2fb8cf082.png)
имеется лишь тогда, когда «расширенное слово»
![$t, a, s$ $t, a, s$](https://dxdy-03.korotkov.co.uk/f/e/a/b/eabb6dc66322baaaafba655789ff171a82.png)
или слово
![$t, a$ $t, a$](https://dxdy-03.korotkov.co.uk/f/2/c/f/2cfbe047421f7cee212a045cb4d5172982.png)
принадлежит языку
![$LS$ $LS$](https://dxdy-02.korotkov.co.uk/f/d/c/1/dc173468919a4ca5a669690ff6b8748982.png)
.
Это «расширенное» слово отличается от слова, про которое алгоритм-решение должен дать ответ. Таким образом, удалось разделить 2 функции, которые исполняет одно и то же слово в «классическом» языке из
![$\mathbb{NP}$ $\mathbb{NP}$](https://dxdy-01.korotkov.co.uk/f/4/7/b/47bfc2169c08d10e14fd91da7fa6aff982.png)
по 2-м разным словам.
Думаю, уже достаточно написано формул, чтобы их обсуждать. Но дам картину в целом (не формально), какие формулы последуют далее, и что я доказываю в итоге (для справки, а не для обсуждения – пока нижесказанное не формализовано).
Далее я ввожу в рассмотрение специфическое утверждение
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
, взятое (его идея) из теоремы о неопределимости математической логики. И это такое утверждение, которое алгоритм-решение
![$\operatorname{Sol}(... , ...)$ $\operatorname{Sol}(... , ...)$](https://dxdy-04.korotkov.co.uk/f/f/6/d/f6d3eefc1f173df060270b7841e30c3d82.png)
не может доказать в принципе. Более того, от способа и времени получения алгоритмом
![$\operatorname{Sol}(... , ...)$ $\operatorname{Sol}(... , ...)$](https://dxdy-04.korotkov.co.uk/f/f/6/d/f6d3eefc1f173df060270b7841e30c3d82.png)
ответа (который в корректном случае может быть только
![$0$ $0$](https://dxdy-03.korotkov.co.uk/f/2/9/6/29632a9bf827ce0200454dd32fc3be8282.png)
), будет зависеть размер слова
![$t, s$ $t, s$](https://dxdy-03.korotkov.co.uk/f/a/a/5/aa522481c54066df939cb8d6f2fb8cf082.png)
, и, возможно, его принадлежность языку
![$LS$ $LS$](https://dxdy-02.korotkov.co.uk/f/d/c/1/dc173468919a4ca5a669690ff6b8748982.png)
.
Поэтому ограничение для времени поиска ответа для данного конкретного случая уже не может быть
![$p_+(..., ...)$ $p_+(..., ...)$](https://dxdy-03.korotkov.co.uk/f/e/0/5/e057332a074afbec47fdbb205b926fe182.png)
– от размера искомого слова: нельзя ставить время работы в зависимость от того, что само зависит от времени его работы.
К тому же, возможности алгоритма-решения
![$\operatorname{Sol}(... , ...)$ $\operatorname{Sol}(... , ...)$](https://dxdy-04.korotkov.co.uk/f/f/6/d/f6d3eefc1f173df060270b7841e30c3d82.png)
описываются НЕ искомым им словом, а соответствующим ему «расширенным» словом. Ведь нам удалось разделить 2 функции, которое исполняет слово в «классическом» случае на 2 разных слова, как уже упоминалось.
Поэтому в детальном представлении для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
появится зависимость от времени работы алгоритма проверки для специфического случая и «расширенного» слова. И это будет
![$p_{\exists}(\overline{AntiSol})$ $p_{\exists}(\overline{AntiSol})$](https://dxdy-01.korotkov.co.uk/f/8/7/d/87d179633a3dc8559237b45ee2c4dcef82.png)
, а соответствующее ему ограничение для алгоритма решения будет
![$p_{\exists +}(\overline{AntiSol})$ $p_{\exists +}(\overline{AntiSol})$](https://dxdy-01.korotkov.co.uk/f/c/e/b/cebb4ead7e70a43595b6bf514fc8906282.png)
. Кстати, для специфического случая мы будем иметь зависимость от слова, «которого нет» в языке
![$LS$ $LS$](https://dxdy-02.korotkov.co.uk/f/d/c/1/dc173468919a4ca5a669690ff6b8748982.png)
и судить о его размере можно лишь по времени работы алгоритма проверки. Вот на это время и будет опираться
![$p_{\exists +}(\overline{AntiSol})$ $p_{\exists +}(\overline{AntiSol})$](https://dxdy-01.korotkov.co.uk/f/c/e/b/cebb4ead7e70a43595b6bf514fc8906282.png)
.
Да, в пункте 6 потребуется поменять условие
![$s = ss(S)$ $s = ss(S)$](https://dxdy-04.korotkov.co.uk/f/f/1/a/f1ac2c5d9750bbba5dfb53373ac6098582.png)
на
![$|s| \le |ss(S)|$ $|s| \le |ss(S)|$](https://dxdy-01.korotkov.co.uk/f/8/9/f/89ffa08a2db6e02df811adf4c7f882ff82.png)
чтобы добиться зависимости размера слова от времени работы алгоритма-решения. Сам
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
остаётся тем же и сохраняет все свои свойства и в уточненном варианте – насколько я поверхностно проверил.
После этого будет доказано, что с такими раскладами при результате
![$0$ $0$](https://dxdy-03.korotkov.co.uk/f/2/9/6/29632a9bf827ce0200454dd32fc3be8282.png)
у алгоритма
![$\operatorname{Sol}(\overline{AntiSol}, ...)$ $\operatorname{Sol}(\overline{AntiSol}, ...)$](https://dxdy-04.korotkov.co.uk/f/b/d/b/bdb933a9bab77f826e8d672551ef91fd82.png)
за время
![$p_{\exists +}\overline{AntiSol}$ $p_{\exists +}\overline{AntiSol}$](https://dxdy-01.korotkov.co.uk/f/c/5/a/c5a50abd14a149afd2fb60cce5918b6082.png)
неизбежно (при достаточно больших по размеру
![$|\overline{AntiSol}|$ $|\overline{AntiSol}|$](https://dxdy-04.korotkov.co.uk/f/b/0/f/b0f04a911137f79f869ed3a66227f14d82.png)
) появится доказательство у утверждения
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
(за счёт того, что размер доказательства зависит в основном от
![$s$ $s$](https://dxdy-03.korotkov.co.uk/f/6/f/9/6f9bad7347b91ceebebd3ad7e6f6f2d182.png)
, которое не участвует в ограничивающем полиноме для времени работы).
И вот здесь ранее я останавливал своё доказательство. Я думал, что для устранения возможности появления доказательства для
![$AntiSol$ $AntiSol$](https://dxdy-01.korotkov.co.uk/f/8/6/6/8667e2c6558ab607f728ec2a4a92dbd882.png)
при результате
![$\operatorname{Sol}(\overline{AntiSol}, ...) = 0$ $\operatorname{Sol}(\overline{AntiSol}, ...) = 0$](https://dxdy-01.korotkov.co.uk/f/0/3/2/0327227c9d34d54dca047133c8e4247382.png)
от алгоритма
![$\operatorname{Sol}(\overline{AntiSol}, ...)$ $\operatorname{Sol}(\overline{AntiSol}, ...)$](https://dxdy-04.korotkov.co.uk/f/b/d/b/bdb933a9bab77f826e8d672551ef91fd82.png)
потребуется неполиномиально больше времени на решение, чем требуется времени на проверку того, какой результат (
![$0$ $0$](https://dxdy-03.korotkov.co.uk/f/2/9/6/29632a9bf827ce0200454dd32fc3be8282.png)
) будет в качестве этого решения. И это доказывало как раз задачу-первоисточник для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
– что для любого алгоритма-решения есть такие задачи, проверка решения которых на равенство правильному ответу неполиномиально проще (быстрее), чем поиск этого ответа данным алгоритмом-решением.
Но теперь я думаю, что имеется доказательство и для
![Smile :-)](./images/smilies/icon_smile.gif)
Просто всё детальное представление для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
строится из предположения о том, какие смыслы у
![$1$ $1$](https://dxdy-01.korotkov.co.uk/f/0/3/4/034d0a6be0424bffe9a6e7ac9236c0f582.png)
и
![$0$ $0$](https://dxdy-03.korotkov.co.uk/f/2/9/6/29632a9bf827ce0200454dd32fc3be8282.png)
должны быть у корректного алгоритма-решения. Но в специфическом случае для быстрого ответа смысл выводится логически. И смысл у
![$0$ $0$](https://dxdy-03.korotkov.co.uk/f/2/9/6/29632a9bf827ce0200454dd32fc3be8282.png)
для алгоритма
![$\operatorname{Sol}(\overline{AntiSol}, ...)$ $\operatorname{Sol}(\overline{AntiSol}, ...)$](https://dxdy-04.korotkov.co.uk/f/b/d/b/bdb933a9bab77f826e8d672551ef91fd82.png)
для специфического случая при быстром возврате им результата может быть только один – «доказательство есть» )))) Потому что логика выше условных договорённостей.
Но раз условные договоренности являются частью детального представления для
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
и корректный алгоритм-решение обязательно должен их нарушить – то он уже не будет соответствовать «стандартным» требованиям к алгоритму-решению из класса
![$\mathbb{P}$ $\mathbb{P}$](https://dxdy-01.korotkov.co.uk/f/8/6/5/865a2c771b7419b8742c1a4a04cc558482.png)
. А раз это произвольный алгоритм-решение – то нет ничего «стандартного» и при этом корректного среди алгоритмов, которые делали бы рассматриваемый язык языком класса
![$\mathbb{P}$ $\mathbb{P}$](https://dxdy-01.korotkov.co.uk/f/8/6/5/865a2c771b7419b8742c1a4a04cc558482.png)
в «стандартном» понимании.
Но сказанное в последней паре абзацев имеет отношение к той будущей дискуссии, которая лишь предстоит (после оставшейся формализации) и которая не затрагивает то, что я хотел доказать изначально (и доказываю, как мне кажется).
Но не могу удержаться от нескольких абзацев «в топку» будущей дискуссии о том, что важнее – условные договоренности или логика.
Пример из жизни. Тебя спрашивают:
«Ты можешь спрогнозировать ответ, который даст на твои слова человек-наоборот?». Понятно, что если ты скажешь «Могу», то человек-наоборот ответит «Не могу», а если ты скажешь «Не могу», то ответом тебе будет «Могу».
Из «алгоритма проверки» ты знаешь, что ты – именно ты – не можешь дать правильный ответ на поставленный вопрос. И вопрос адресуется именно тебе. Поэтому ты сообщаешь «Не могу», потому что именно такой ответ сообщает о твоей неспособности в соответствии со сведениями от «алгоритма проверки». И этот же ответ заведомо означает, что человек-наоборот ответит «Могу». И ты дал правильное сообщение (прогноз), потому что стандартное «соглашение о кодировании» твоего сообщения-прогноза не работает в данном случае в отношении «человека-наоборот».
Но «соглашение о кодировании» сообщения-результата в данном случае и не требуется, потому что правильный формат сообщения в данном случае логически выводится из информации о твоих собственных возможностях (точнее, неспособностях) в соответствии с тем форматом, который принят для проверки твоих возможностей (неспособностей). Притом информация о твоих возможностях получается быстро в данном случае.
И да – мы выходим на формализацию понятия рефлексии, когда алгоритму для правильного ответа надо понимать, что вопрос задан именно ему. Это – гораздо принципиальнее и интереснее, чем даже вопрос про
![$\mathbb{NP} \ne \mathbb{P}$ $\mathbb{NP} \ne \mathbb{P}$](https://dxdy-02.korotkov.co.uk/f/5/3/5/5357ec809677d4368f5c1b0a9f33d92882.png)
, потому что открывается возможность для математической формализации принятия решений «живыми» разумными системами, которая невозможна без рефлексии. То, что мы делаем по 100 раз на дню, выделяя и решая задачи, которые стоят именно перед нами. И то, что до сих пор никаким «боком» не было формализовано в математике.