В продолжение записи
"Теорема Геделя на коленке".
Для тех, кого интересует эта тема:
я написал это доказательство также по-английски, и добавил к нему длинное предисловие о том, чем это доказательство интересно (ведь можно доказать неполноту через проблему остановки еще быстрее и проще). Если вкратце, то оно интересно тем, что в отличие от обычных "алгоритмических" доказательств теоремы Геделя, сохраняет лучшие свойства подхода Россера: минимальные требования к теории T, всего лишь непротиворечимость, и конструктивное построение утверждения, которое T не доказывает и не опровергает. При этом оно намного проще технически и понятнее концептуально, чем традиционное доказательство, с его "диагональной леммой" и "трюком Россера".
Поправки, замечания и вопросы принимаются, конечно же.