Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

новое док-во неполноты

Наконец-то нашёл время, и внимательно прочитал и проверил интереснейшее новое доказательство первой теоремы о неполноте Гёделя. Доказательство на самом деле довольно старое, его придумал давно Крипке, но пару лет назад опубликовал наконец Патнэм (потому что Крипке лень было его публиковать, видимо).

Вроде всё верно, и очень красивая идея. Доказательство совершенно семантическое, и использует нестандартную модель PA (арифметики Пеано), но очень простым способом. Нестандартные модели арифметики чаще всего строят с помощью теоремы компактности логики первого порядка (т.к. тогда можно “задать” некоторые удобные свойства полученной модели), но в данном случае, для этого доказательства, можно взять более простое “алгебраическое” (а не “логическое”) построение нестадартной модели с помощью возведения стандартной модели в степень по модулю ультрафильтра.

О неполноте и разных видах теоремы Гёделя и её доказательств у меня была длинная запись почти год назад. В терминах той записи доказательство Крипке (и версия теоремы, которую оно доказывает) более всего походит на второй вариант: относительно “сильное” семантическое условие, и утверждение, которое демонстрирует неполноту, строится конструктивным образом. Более того, доказательство Крипке намного более “семантическое”, чем все три варианта, о которых я писал в старой записи, ещё с одной точки зрения: в нём вообще не рассматриваются формальные доказательства и их арифметизация. Для доказательства Крипке нам нужна арифметизация синтаксиса, но только для работы с формулами, для индуктивного разделения их на составляющие части. Нам не нужно кодировать формальные доказательства или доказывать их свойства.

Конечно, “семантический” характер условия этого варианта теоремы, и самого доказательства, означает, что его невозможно использовать для доказательства второй теоремы о неполноте (в старой записи я объясняю вкратце, почему это так). У доказательства Крипке, однако, есть ещё одна очень интересная особенность. Оно не использует “диагонализацию” во время построения ключевого утверждения (которое оказывается недоказуемым и неопровержимым в заданной формальной системе). Все другие известные варианты доказательства первой теоремы о неполноте используют диагонализацию — процесс построения такого утверждения, которое в известном смысле “говорит о себе самом”. То, что можно доказать теорему о неполноте без диагонализации — факт, несомненно, важный как минимум с философской точки зрения. Окажется ли он полезным с математической точки зрения? — пока, кажется, неясно.

P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 15 comments