Я устал, я не ухожу (с) почти Ельцин 
  Пардон, что долго молчал, но сейчас отчётный период и нет возможности сосредоточиться на математике кроме некоторых выходных. Да и трудно даётся решение вопросов не о смысле, а о форме его подачи (формализация), но это необходимо, конечно. Поэтому, чтобы не тянуть – изложу сейчас то, что готово.
Формулирую, что такое 

 – в деталях: 

 
Тут 

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

. 

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

. 

 и 

 – время работы соответствующих алгоритмов. 
При этом:

 - это я не «доигрался» до логики 2-го порядка, а это условное сокращение для записи вида
 где алгоритм 

 – это «универсальный алгоритм», который исполняет программный код из первого аргумента, передавая ему в качестве аргументов всё, начиная со 2-го аргумента в 

. 
впрочем и последняя формула – тоже сокращение для:

. 
Где 

 – это «условная компиляция», которая проверяет, действительно ли в 

 программный код в нужном формате или нечто ошибочное. 
Как побочный эффект моего исследования вопроса – был найден способ свести вопрос о 

 к второй части детального представления этого 

. А именно – Если будет доказана вторая часть 

:


то будет доказано и 

. А 

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

 верно:

Последнее позволяет не рассматривать 1-ю часть детального представления для 

. При этом эти 

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

, и вопрос только в размере доказательства.
Точнее: верно 

, а иначе будет выполнена 1-я часть детального представления (так построено утверждение 

):
 Вернемся теперь от побочной линии к основной.
Перепишем детальное представление для 

 в новом виде:

 
. 
Мы добавили к слову часть 

 – это ничего не меняет в принципе (просто разбили слово на 2 части, где новая часть ничего не несет, кроме возможности увеличить размер допустимых для рассмотрения сертификатов). Ещё мы обозначили здесь переменной 

 «опровергающее утверждение» вместо обозначения 

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

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

 с «классическим» алгоритмом проверки и добавить в этот алгоритм такую часть 

, от которой ничего не зависит, кроме требования, чтобы к размеру сертификата (при расчете ограничений) добавлялся ещё и её размер. Но мы этим не ограничимся, разумеется, и рассмотрим язык не с таким слегка изменённым «квазиклассическим» алгоритмом проверки. 
Ещё один нюанс – полиномы 

 и 

 могут в некоторых случаях иметь степень ноль при аргументе 

, если соответствующее им слово не будет зависеть от размера 

, но это будет разбираться отдельно далее. Не принципиален для дальнейшего рассмотрения вопрос о зависимости 

 ещё и от 

: Мы будем рассматривать такие 

, размер которых больше размера 

. Поэтому ограничение в любом случае оказывается в пределах 

.
Напоминаю, что 

 в логике – это аналог подстановки, так как  

.
При этом обозначение 

 я использую в качестве сокращения для более правильного (но  в котором больше скобок) обозначения: 

. 
В свете последнего детального представления для 

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

 является вот что: Часть данных, соответствующих программному коду алгоритма-решения 

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

которые алгоритм 

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

, полностью соответствуют наличию подтверждающих сертификатов вида

, где 

И, таким образом, возможность алгоритма-решения 

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

 слова 

имеется лишь тогда, когда «расширенное слово»

 или слово 

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

.
Это «расширенное» слово отличается от слова, про которое алгоритм-решение должен дать ответ. Таким образом, удалось разделить 2 функции, которые исполняет одно и то же слово в «классическом» языке из 

 по 2-м разным словам. 
Думаю, уже достаточно написано формул, чтобы их обсуждать. Но дам картину в целом (не формально), какие формулы последуют далее, и что я доказываю в итоге (для справки, а не для обсуждения – пока нижесказанное не формализовано).
Далее я ввожу в рассмотрение специфическое утверждение 

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

 не может доказать в принципе. Более того, от способа и времени получения алгоритмом 

 ответа (который в корректном случае может быть только 

), будет зависеть размер слова 

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

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

 – от размера искомого слова: нельзя ставить время работы в зависимость от того, что само зависит от времени его работы.
К тому же, возможности алгоритма-решения 

 описываются НЕ искомым им словом, а соответствующим ему «расширенным» словом. Ведь нам удалось разделить 2 функции, которое исполняет слово в «классическом» случае на 2 разных слова, как уже упоминалось. 
Поэтому в детальном представлении для 

 появится зависимость от времени работы алгоритма проверки для специфического случая и «расширенного» слова. И это будет 

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

. Кстати, для специфического случая мы будем иметь зависимость от слова, «которого нет» в языке 

 и судить о его размере можно лишь по времени работы алгоритма проверки. Вот на это время и будет опираться 

.  
Да, в пункте 6 потребуется поменять условие 

 на 

 чтобы добиться зависимости размера слова от времени работы алгоритма-решения. Сам 

 остаётся тем же и сохраняет все свои свойства и в уточненном варианте – насколько я поверхностно проверил. 
После этого будет доказано, что с такими раскладами при результате 

 у алгоритма 

 за время 

 неизбежно (при достаточно больших по размеру 

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

 (за счёт того, что размер доказательства зависит в основном от 

, которое не участвует в ограничивающем полиноме для времени работы).
И вот здесь ранее я останавливал своё доказательство. Я думал, что для устранения возможности появления доказательства для 

 при результате 

 от алгоритма 

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

) будет в качестве этого решения. И это доказывало как раз задачу-первоисточник для 

 – что для любого алгоритма-решения есть такие задачи, проверка решения которых на равенство правильному ответу неполиномиально проще (быстрее), чем поиск этого ответа данным алгоритмом-решением.
Но теперь я думаю, что имеется доказательство и для 
 
Просто всё детальное представление для 

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

 и 

 должны быть у корректного алгоритма-решения. Но в специфическом случае для быстрого ответа смысл выводится логически. И смысл у 

 для алгоритма 

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

 и корректный алгоритм-решение обязательно должен их нарушить – то он уже не будет соответствовать «стандартным» требованиям к алгоритму-решению из класса 

. А раз это произвольный алгоритм-решение – то нет ничего «стандартного» и при этом корректного среди алгоритмов, которые делали бы рассматриваемый язык языком класса 

 в «стандартном» понимании. 
Но сказанное в последней паре абзацев имеет отношение к той будущей дискуссии, которая лишь предстоит (после оставшейся формализации) и которая не затрагивает то, что я хотел доказать изначально (и доказываю, как мне кажется).
 Но не могу удержаться от нескольких абзацев «в топку» будущей дискуссии о том, что важнее – условные договоренности или логика. 
Пример из жизни. Тебя спрашивают: 
«Ты можешь спрогнозировать ответ, который даст на твои слова человек-наоборот?». Понятно, что если ты скажешь «Могу», то человек-наоборот ответит «Не могу», а если ты скажешь «Не могу», то ответом тебе будет «Могу». 
Из «алгоритма проверки» ты знаешь, что ты – именно ты – не можешь дать правильный ответ на поставленный вопрос. И вопрос адресуется именно тебе. Поэтому ты сообщаешь «Не могу», потому что именно такой ответ сообщает о твоей неспособности в соответствии со сведениями от «алгоритма проверки». И этот же ответ заведомо означает, что человек-наоборот ответит «Могу». И ты дал правильное сообщение (прогноз), потому что стандартное «соглашение о кодировании» твоего сообщения-прогноза не работает в данном случае в отношении «человека-наоборот». 
Но «соглашение о кодировании» сообщения-результата в данном случае и не требуется, потому что правильный формат сообщения в данном случае логически выводится из информации о твоих собственных возможностях (точнее, неспособностях) в соответствии с тем форматом, который принят для проверки твоих возможностей (неспособностей). Притом информация о твоих возможностях получается быстро в данном случае. 
И да – мы выходим на формализацию понятия рефлексии, когда алгоритму для правильного ответа надо понимать, что вопрос задан именно ему. Это – гораздо принципиальнее и интереснее, чем даже вопрос про 

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