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

.
Свойство 1 (верно, что):



тут – это просто подстановка, в качестве которой берется строка из символов «1» с длиной, равной числу (пусть десятичному), которое находится внутри строки

. Смысл не в подстановке, а в том, что при «достаточно быстрой» работе

с результатом

будет доказано как раз «не 0», а принадлежность слова

языку

. При этом «достаточно быстро» тут (алгоритм

является полиномом) – это даже не полиномиально малое количество шагов относительно размера

, но того же уровня полиномиальности (определение дам чуть ниже), что и размер

(то есть, экспоненциально дольше).
Максимальный размер доказательства

при данном

задаётся полиномом

.
Алгоритм

получает по утверждению

программный код алгоритма

и аргумент

, запускает

, переводит каждый шаг его работы в строки доказательства и в итоге получает доказательство результата его работы, а на базе этого – и доказательство для утверждения

или для его отрицания.
Насчёт аргумента

при работе

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

(эмуляции работы) при каждом обращении к ячейке памяти, где должен находится

возвращается символ «1». Поэтому времени на «создание»

тратится не больше, чем уходит шагов

на работу

– каким бы гигантским по своим размерам не был этот

.
На самом деле в последнем равенстве Свойства 1 можно заменить

на

,
где

и
Понятно, что здесь

– это функция, обратная к

, из-за чего

.
При этом

оказывается в полиномиальных пределах относительно размера

и величины

.
и в конце Свойства 1 будет тогда такое равенство:

Но для этой замены в п. 6 потребуется поменять

на:

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

и

имеют одинаковый уровень полиномиальности своих результатов тогда и только тогда, когда имеются такие полиномы

и

, что верно:

и

– при любых аргументах в данных алгоритмах.
То есть, алгоритмы взаимно полиномиально ограничивают друг друга.
Из Свойства 1 видно, что не время работы алгоритма-решения

Зависит от размера слова, с которым оперирует алгоритм проверки

,
Но как раз наоборот – размер слова зависит от времени работы алгоритма-решения.
При этом заранее известно –
Свойство 2.
Остановка следующего алгоритма-решения с результатом 1 является ошибочным:

– не корректная работа при произвольном

.
Что означает, что при выполнении данного утверждения будет верным:

То есть, необходимое условие для корректности алгоритма-решения

является истинность утверждения:

.
При этом данное утверждение вовсе не является достаточным для соответствия результата

алгоритма-решения

и непринадлежности слова

языку

- что видно из Свойства 1.
И даже если

проработает очень долго, но «примитивно» (будет пустой цикл крутить, например), то и в этом случае возникнут последствия, аналогичные Свойству 1.
Свойству 2 соответствует следующая информация от алгоритма проверки:
Свойство 3.

, при этом

, где

, а последнее означает время работы (количество шагов) алгоритма проверки тогда, когда первый аргумент (проверяемое утверждение) совпадает с одним из «антиутверждений» для второго аргумента – содержащего программный код алгоритма, которому соответствует его «антиутверждение». Аргумент

в этом случае не используется алгоритмом проверки – так как и без этого ясно, что алгоритм

не сможет стандартным способом подтвердить истинность

(не сможет выдать

в качестве подтверждения принадлежности слова

языку

).
Ранее я останавливался на свойстве 3 в своём доказательстве и видел достигнутую цель:
Алгоритм проверки выдаёт быстрый ответ о том, какой результат у алгоритма-решения (произвольного!) будет единственно правильным для некоторого конкретного утверждения – это Свойство 3. Но выдать этот результат, корректно данный алгоритм-решение может лишь за неполиномиально огромное количество шагов (зависящее от

– неполиномиально большого относительно «быстрого»

– это Свойство 1.
То есть – проверка решения оказывается неполиномиально быстрей самого решения и это – для произвольного алгоритма-решения. Это и есть «первопричина» появления красивой формулы

, от красоты которой была забыта первоначальная цель найти язык с «трудными задачами», неразрешимыми полиномиально быстро (относительно времени проверки) никаким алгоритмом-решением.
Однако, по ходу формализации обнаружились (вроде бы) дефекты в самой постановке вопроса о сводимости класса

к классу

, аналогичные тем дефектам, которые обнаружились в постановке вопроса о способе разрешить логическую теорию. Эти обнаруженные дефекты были тогда представлены в теоремах Гёделя о неполноте. И, вроде бы, по аналогичным причинам можно всё-таки доказать и неравенство

. Что я и попытаюсь в общих чертах сделать ниже (и из-за чего дополнительно «торможу» - дополнительно к недавнему отчётному периоду).
Аксиома рефлексии:
Собственный программный код алгоритма необходимо рассматривать в качестве данных, которыми этот алгоритм располагает, наряду и, в не меньшей степени, чем данные, которые он получает в своих аргументах.
Совершенно очевидная аксиома, которой мы пользуемся по 100 раз на дню, решая те задачи, которые адресованы именно нам и от которых зависимы именно мы, но при этом данная аксиома не была формализована в математике. Вот и исправим это упущение.
Заметим, что свойство 3 построено на базе свойства 2 и тесно связано с тем, что результат

- заведомо некорректен. Откуда корректным может быть только результат:

.
Из аксиомы рефлексии мы видим, что алгоритм-решение:

Располагает всей следующей информацией:

А это слово (и не только слово, пояснение – в 2-х следующих абзацах) заведомо не принадлежит языку

на основании Свойства 3. И – более того – время, за которое доступна данная информация у алгоритма проверки:

,
означает, что данное «слово, которого нет» в языке

имеет вид:

(будем называть его далее «персональным словом алгоритма

И на этом основании, если алгоритм

сводит язык

к классу

он должен дать ответ:

за время

.
Но при этом возникает коллизия со словом:

(будем называть его далее «общим словом»)
Которое в силу Свойства 1 при достаточно большом размере

должно принадлежать языку

. В самом деле, условие:

будет выполнено для достаточных больших

, так как там же (Свойство 1):

И правая часть неравенства у нас тут растёт экспоненциально быстрее левой (где

), что неизбежно сделает неравенство истинным начиная с какого-то момента.
Но, в чём состоит коллизия? В том, что с точки зрения принадлежности языку

слова

Алгоритм-решение:

Должен вернуть

?
Это «должен» опирается на условные договорённости о соответствии тому классу

, в котором алгоритм проверки для принадлежащего языку слова всегда выдаёт

. Что, кстати, вовсе не является единственным способом построения класса, в котором за полиномиальное количество шагов от размера слова можно вычислять (не)принадлежность слова языку. А как обстоят дела с точки зрения не условных договорённостей, а логики?
А логика говорит вот что (из Свойства 1):

То есть, при достаточно быстрой работе

его результат

может означать только одно – принадлежность слова

языку

. И это – логика, а не условные договорённости. А логика – выше условных договорённостей.

не ищет «со стороны» ответ о (не)принадлежности слова

языку

, а делает нечто противоположное: Алгоритм-решение

делает («насильственно», а не констатирует как «сторонний наблюдатель») слово

принадлежащим или не принадлежащим языку

.
И у нас правая часть импликации (заключение) вовсе не независима от левой (посылки) – если правая часть станет противоположной, то и левая часть тоже превратиться в своё отрицание (в соответствии с правилом контрапозиции):

.
Разумеется, причинно-следственные связи в детерминированном мире имеют смысл только в контексте переменной на месте

. Ведь в детерминированном мире всё является в некотором смысле окончательным и различие можно понять лишь в плане сравнения. И вот для разных

и соответствующих им

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

никаких вариаций в детерминированном мире нет. А вот для множества

есть вполне определённые закономерности.
То есть, при быстром ответе логика требует от нас считать результат

алгоритма-решения

признаком принадлежности слова

– при корректном значении

, разумеется (пояснения в следующем абзаце). И для слова

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

расходится с тем, что изначально требовалось для сведения нашей задачи к классу

.
Оговорка про «при корректном значении

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

в разбираемом случае – но это очевидно уже по тому, что в отношении «специального слова» результат

теперь несёт «специальный» смысл. При всём при этом полиномиальность времени проверки – с учётом «внешней» части – относительно размера

не нарушается, вообще говоря. В обсуждении Свойства 1 было сказано:

где

и

.
При этом

оказывается в полиномиальных пределах относительно размера

и величины

.
А поскольку и

в полиномиальных пределах относительно размера

при корректной работе

, то всё оказывается в полиномиальных пределах относительно этого

.
Мы рассмотрели случай, когда решение алгоритма

нацелено на персональное слово и результат получен полиномиально быстро относительно его размера. Тогда для персонального слова соблюдены условности в понимании смысла

(слово принадлежит языку) и

(слово не принадлежит языку). А для общего слова эти условности тогда отменены логикой. И по этой причине алгоритм

, нацеленный на персональное слово, не может стать алгоритмом проверки языка

– если бы язык

принадлежал классу

.
Если же решение нацелено на общее слово, то ответ получается неполиномиально долгим относительно размера персонального слова (очевидно из Свойства 1) и это - факт, который ничто не отменяет. И в этом случае алгоритм

оказывается не способным давать ответы за время, полиномиальное относительно размера персонального слова. То есть – тоже не может стать алгоритмом проверки языка

– если язык

принадлежит классу

. При этом такое «затягивание времени» принципиальным образом изменяет ситуацию в сравнении со случаем полиномиально быстрого ответа относительно размера персонального слова – общее слово перестаёт принадлежать языку

.
В предыдущих 2-х абзацах мы рассмотрели все возможные варианты ответа алгоритма

которые можно было «подозревать» как допускающие сводимость языка

к классу

посредством алгоритма

и убедились в обратном.
А поскольку алгоритм-решение

является произвольным, то язык

не сводится к классу

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

. А это и означает, что

.
Проще, конечно, было бы, если бы результат

так же прямо приводил к

, как

приводит к

. Но и вариант с 2-мя словами приводит к невозможности для

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

.
Впрочем, нельзя не отметить гораздо более принципиальный и интересный результат, чем

. Это – аксиома рефлексии. И она позволяет понять, кстати, какой из вариантов ответа

является правильным в принципе, а не с точки зрения соответствия классу

(оба не соответствуют):
1. Быстрый ответ, основанный на размере персонального слова или
2. Медленный ответ, нацеленный на то, чтобы слово

и соответствовало результату

.
Правильным, безусловно, является 1-й вариант. (20 тыс. знаков не хватило на последние абзацы, но они и не имеют прямого отношения к сказанному)