![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
новое док-во неполноты
Наконец-то нашёл время, и внимательно прочитал и проверил интереснейшее новое доказательство первой теоремы о неполноте Гёделя. Доказательство на самом деле довольно старое, его придумал давно Крипке, но пару лет назад опубликовал наконец Патнэм (потому что Крипке лень было его публиковать, видимо).
Вроде всё верно, и очень красивая идея. Доказательство совершенно семантическое, и использует нестандартную модель PA (арифметики Пеано), но очень простым способом. Нестандартные модели арифметики чаще всего строят с помощью теоремы компактности логики первого порядка (т.к. тогда можно “задать” некоторые удобные свойства полученной модели), но в данном случае, для этого доказательства, можно взять более простое “алгебраическое” (а не “логическое”) построение нестадартной модели с помощью возведения стандартной модели в степень по модулю ультрафильтра.
О неполноте и разных видах теоремы Гёделя и её доказательств у меня была длинная запись почти год назад. В терминах той записи доказательство Крипке (и версия теоремы, которую оно доказывает) более всего походит на второй вариант: относительно “сильное” семантическое условие, и утверждение, которое демонстрирует неполноту, строится конструктивным образом. Более того, доказательство Крипке намного более “семантическое”, чем все три варианта, о которых я писал в старой записи, ещё с одной точки зрения: в нём вообще не рассматриваются формальные доказательства и их арифметизация. Для доказательства Крипке нам нужна арифметизация синтаксиса, но только для работы с формулами, для индуктивного разделения их на составляющие части. Нам не нужно кодировать формальные доказательства или доказывать их свойства.
Конечно, “семантический” характер условия этого варианта теоремы, и самого доказательства, означает, что его невозможно использовать для доказательства второй теоремы о неполноте (в старой записи я объясняю вкратце, почему это так). У доказательства Крипке, однако, есть ещё одна очень интересная особенность. Оно не использует “диагонализацию” во время построения ключевого утверждения (которое оказывается недоказуемым и неопровержимым в заданной формальной системе). Все другие известные варианты доказательства первой теоремы о неполноте используют диагонализацию — процесс построения такого утверждения, которое в известном смысле “говорит о себе самом”. То, что можно доказать теорему о неполноте без диагонализации — факт, несомненно, важный как минимум с философской точки зрения. Окажется ли он полезным с математической точки зрения? — пока, кажется, неясно.
P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
Вроде всё верно, и очень красивая идея. Доказательство совершенно семантическое, и использует нестандартную модель PA (арифметики Пеано), но очень простым способом. Нестандартные модели арифметики чаще всего строят с помощью теоремы компактности логики первого порядка (т.к. тогда можно “задать” некоторые удобные свойства полученной модели), но в данном случае, для этого доказательства, можно взять более простое “алгебраическое” (а не “логическое”) построение нестадартной модели с помощью возведения стандартной модели в степень по модулю ультрафильтра.
О неполноте и разных видах теоремы Гёделя и её доказательств у меня была длинная запись почти год назад. В терминах той записи доказательство Крипке (и версия теоремы, которую оно доказывает) более всего походит на второй вариант: относительно “сильное” семантическое условие, и утверждение, которое демонстрирует неполноту, строится конструктивным образом. Более того, доказательство Крипке намного более “семантическое”, чем все три варианта, о которых я писал в старой записи, ещё с одной точки зрения: в нём вообще не рассматриваются формальные доказательства и их арифметизация. Для доказательства Крипке нам нужна арифметизация синтаксиса, но только для работы с формулами, для индуктивного разделения их на составляющие части. Нам не нужно кодировать формальные доказательства или доказывать их свойства.
Конечно, “семантический” характер условия этого варианта теоремы, и самого доказательства, означает, что его невозможно использовать для доказательства второй теоремы о неполноте (в старой записи я объясняю вкратце, почему это так). У доказательства Крипке, однако, есть ещё одна очень интересная особенность. Оно не использует “диагонализацию” во время построения ключевого утверждения (которое оказывается недоказуемым и неопровержимым в заданной формальной системе). Все другие известные варианты доказательства первой теоремы о неполноте используют диагонализацию — процесс построения такого утверждения, которое в известном смысле “говорит о себе самом”. То, что можно доказать теорему о неполноте без диагонализации — факт, несомненно, важный как минимум с философской точки зрения. Окажется ли он полезным с математической точки зрения? — пока, кажется, неясно.
P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
no subject
no subject
no subject
no subject
no subject
no subject
no subject
Свинство со стороны Евклидовых Журналов не поддерживать Athens login:(
no subject
Если я не ошибаюсь, у теоремы Харрингтона-Париса есть доказательство (или даже таким было первое доказательство), не зависящее ни от теоремы Геделя, ни от диагонализации.
no subject
Если не ошибаюсь, первое доказательство Харрингтона-Париса использовало вторую теорему Гёделя, а после уже они придумали доказательство через нестадартные модели PA. Впрочем, очень может быть, что ошибаюсь.
no subject
no subject
no subject
no subject
no subject
прошу прощения, погорячился.
утешает, что таки нашлись люди, которым было понятно.
мне вот понравилось упомянутая континуум-гипотеза (яндекс маленько просветил).
не знаете ли, гденть есть подробности про решение?
попроще, для чайников.
вас просить объяснить не буду - обидно, человек старается-старается, а ты ничего не понимаешь.
no subject