Вроде всё верно, и очень красивая идея. Доказательство совершенно семантическое, и использует нестандартную модель PA (арифметики Пеано), но очень простым способом. Нестандартные модели арифметики чаще всего строят с помощью теоремы компактности логики первого порядка (т.к. тогда можно “задать” некоторые удобные свойства полученной модели), но в данном случае, для этого доказательства, можно взять более простое “алгебраическое” (а не “логическое”) построение нестадартной модели с помощью возведения стандартной модели в степень по модулю ультрафильтра.
О неполноте и разных видах теоремы Гёделя и её доказательств у меня была длинная запись почти год назад. В терминах той записи доказательство Крипке (и версия теоремы, которую оно доказывает) более всего походит на второй вариант: относительно “сильное” семантическое условие, и утверждение, которое демонстрирует неполноту, строится конструктивным образом. Более того, доказательство Крипке намного более “семантическое”, чем все три варианта, о которых я писал в старой записи, ещё с одной точки зрения: в нём вообще не рассматриваются формальные доказательства и их арифметизация. Для доказательства Крипке нам нужна арифметизация синтаксиса, но только для работы с формулами, для индуктивного разделения их на составляющие части. Нам не нужно кодировать формальные доказательства или доказывать их свойства.
Конечно, “семантический” характер условия этого варианта теоремы, и самого доказательства, означает, что его невозможно использовать для доказательства второй теоремы о неполноте (в старой записи я объясняю вкратце, почему это так). У доказательства Крипке, однако, есть ещё одна очень интересная особенность. Оно не использует “диагонализацию” во время построения ключевого утверждения (которое оказывается недоказуемым и неопровержимым в заданной формальной системе). Все другие известные варианты доказательства первой теоремы о неполноте используют диагонализацию — процесс построения такого утверждения, которое в известном смысле “говорит о себе самом”. То, что можно доказать теорему о неполноте без диагонализации — факт, несомненно, важный как минимум с философской точки зрения. Окажется ли он полезным с математической точки зрения? — пока, кажется, неясно.
P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
