новое док-во неполноты
Apr. 21st, 2004 10:58 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaНаконец-то нашёл время, и внимательно прочитал и проверил интереснейшее новое доказательство первой теоремы о неполноте Гёделя. Доказательство на самом деле довольно старое, его придумал давно Крипке, но пару лет назад опубликовал наконец Патнэм (потому что Крипке лень было его публиковать, видимо).
Вроде всё верно, и очень красивая идея. Доказательство совершенно семантическое, и использует нестандартную модель PA (арифметики Пеано), но очень простым способом. Нестандартные модели арифметики чаще всего строят с помощью теоремы компактности логики первого порядка (т.к. тогда можно “задать” некоторые удобные свойства полученной модели), но в данном случае, для этого доказательства, можно взять более простое “алгебраическое” (а не “логическое”) построение нестадартной модели с помощью возведения стандартной модели в степень по модулю ультрафильтра.
О неполноте и разных видах теоремы Гёделя и её доказательств у меня была длинная запись почти год назад. В терминах той записи доказательство Крипке (и версия теоремы, которую оно доказывает) более всего походит на второй вариант: относительно “сильное” семантическое условие, и утверждение, которое демонстрирует неполноту, строится конструктивным образом. Более того, доказательство Крипке намного более “семантическое”, чем все три варианта, о которых я писал в старой записи, ещё с одной точки зрения: в нём вообще не рассматриваются формальные доказательства и их арифметизация. Для доказательства Крипке нам нужна арифметизация синтаксиса, но только для работы с формулами, для индуктивного разделения их на составляющие части. Нам не нужно кодировать формальные доказательства или доказывать их свойства.
Конечно, “семантический” характер условия этого варианта теоремы, и самого доказательства, означает, что его невозможно использовать для доказательства второй теоремы о неполноте (в старой записи я объясняю вкратце, почему это так). У доказательства Крипке, однако, есть ещё одна очень интересная особенность. Оно не использует “диагонализацию” во время построения ключевого утверждения (которое оказывается недоказуемым и неопровержимым в заданной формальной системе). Все другие известные варианты доказательства первой теоремы о неполноте используют диагонализацию — процесс построения такого утверждения, которое в известном смысле “говорит о себе самом”. То, что можно доказать теорему о неполноте без диагонализации — факт, несомненно, важный как минимум с философской точки зрения. Окажется ли он полезным с математической точки зрения? — пока, кажется, неясно.
P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
Вроде всё верно, и очень красивая идея. Доказательство совершенно семантическое, и использует нестандартную модель PA (арифметики Пеано), но очень простым способом. Нестандартные модели арифметики чаще всего строят с помощью теоремы компактности логики первого порядка (т.к. тогда можно “задать” некоторые удобные свойства полученной модели), но в данном случае, для этого доказательства, можно взять более простое “алгебраическое” (а не “логическое”) построение нестадартной модели с помощью возведения стандартной модели в степень по модулю ультрафильтра.
О неполноте и разных видах теоремы Гёделя и её доказательств у меня была длинная запись почти год назад. В терминах той записи доказательство Крипке (и версия теоремы, которую оно доказывает) более всего походит на второй вариант: относительно “сильное” семантическое условие, и утверждение, которое демонстрирует неполноту, строится конструктивным образом. Более того, доказательство Крипке намного более “семантическое”, чем все три варианта, о которых я писал в старой записи, ещё с одной точки зрения: в нём вообще не рассматриваются формальные доказательства и их арифметизация. Для доказательства Крипке нам нужна арифметизация синтаксиса, но только для работы с формулами, для индуктивного разделения их на составляющие части. Нам не нужно кодировать формальные доказательства или доказывать их свойства.
Конечно, “семантический” характер условия этого варианта теоремы, и самого доказательства, означает, что его невозможно использовать для доказательства второй теоремы о неполноте (в старой записи я объясняю вкратце, почему это так). У доказательства Крипке, однако, есть ещё одна очень интересная особенность. Оно не использует “диагонализацию” во время построения ключевого утверждения (которое оказывается недоказуемым и неопровержимым в заданной формальной системе). Все другие известные варианты доказательства первой теоремы о неполноте используют диагонализацию — процесс построения такого утверждения, которое в известном смысле “говорит о себе самом”. То, что можно доказать теорему о неполноте без диагонализации — факт, несомненно, важный как минимум с философской точки зрения. Окажется ли он полезным с математической точки зрения? — пока, кажется, неясно.
P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2004-04-21 01:10 pm (UTC)no subject
Date: 2004-04-21 01:36 pm (UTC)no subject
Date: 2004-04-21 01:59 pm (UTC)no subject
Date: 2004-04-21 02:05 pm (UTC)no subject
Date: 2004-04-21 04:55 pm (UTC)Свинство со стороны Евклидовых Журналов не поддерживать Athens login:(
no subject
Date: 2004-04-21 05:01 pm (UTC)Если я не ошибаюсь, у теоремы Харрингтона-Париса есть доказательство (или даже таким было первое доказательство), не зависящее ни от теоремы Геделя, ни от диагонализации.
no subject
Date: 2004-04-22 04:14 am (UTC)no subject
Date: 2004-04-23 03:39 am (UTC)no subject
Date: 2004-04-25 12:58 pm (UTC)Если не ошибаюсь, первое доказательство Харрингтона-Париса использовало вторую теорему Гёделя, а после уже они придумали доказательство через нестадартные модели PA. Впрочем, очень может быть, что ошибаюсь.
no subject
Date: 2004-04-25 12:59 pm (UTC)no subject
Date: 2004-04-25 12:59 pm (UTC)no subject
Date: 2004-04-25 01:00 pm (UTC)no subject
Date: 2004-04-25 01:00 pm (UTC)no subject
Date: 2004-04-26 12:06 am (UTC)прошу прощения, погорячился.
утешает, что таки нашлись люди, которым было понятно.
мне вот понравилось упомянутая континуум-гипотеза (яндекс маленько просветил).
не знаете ли, гденть есть подробности про решение?
попроще, для чайников.
вас просить объяснить не буду - обидно, человек старается-старается, а ты ничего не понимаешь.
no subject
Date: 2004-04-26 03:42 am (UTC)