?

Log in

No account? Create an account
Ни о какой безапелляционности в моих высказываниях не может быть и речи! [entries|archive|friends|userinfo]
Anatoly Vorobey

[ website | Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Links
[Links:| English-language weblog ]

новое док-во неполноты [апр. 21, 2004|10:58 pm]
Anatoly Vorobey
Наконец-то нашёл время, и внимательно прочитал и проверил интереснейшее новое доказательство первой теоремы о неполноте Гёделя. Доказательство на самом деле довольно старое, его придумал давно Крипке, но пару лет назад опубликовал наконец Патнэм (потому что Крипке лень было его публиковать, видимо).

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

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

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

P.S. Если кому-то интересно, могу на днях как-нибудь пересказать вкратце, но со всеми нужными подробностями, само доказательство Крипке.
СсылкаОтветить

Comments:
From: i_am_ubique
2004-04-21 01:10 pm
Удивительно, мне стало безумно интересно, хотя я знаю математику на уровне 3-го курса среднего ВУЗа....
(Ответить) (Thread)
[User Picture]From: avva
2004-04-25 01:00 pm
Вот здесь кое-что попробовал объяснить подробнее.
(Ответить) (Parent) (Thread)
[User Picture]From: kobak
2004-04-21 01:36 pm
Очень интересно; но если только мне - то пересказывать не надо, так как понимаю, сколько времени на это может уйти.
(Ответить) (Thread)
[User Picture]From: avva
2004-04-25 12:59 pm
Здесь попробовал описать, но увы, немало знаний пришлось предполагать известными, а то бы это ещё в три раза больше вышло, и я бы не потянул.
(Ответить) (Parent) (Thread)
[User Picture]From: french_man
2004-04-21 01:59 pm
А пришли мне статью, а? Он мне не дает почитать.
(Ответить) (Thread)
[User Picture]From: avva
2004-04-21 02:05 pm
Не могу: мне тоже не показывает. Я дал ссылку, чтобы легко было увидеть библиографические данные и abstract, а самую статью прочитал сегодня на бумаге в библиотеке. Могу отсканировать и переслать тебе картинками, если хочешь, когда в следующий раз там буду.
(Ответить) (Parent) (Thread)
[User Picture]From: sabalin
2004-04-21 04:55 pm
Любопытно. Завтра добирусь до библиотеки почитаю процитированную вами статью.
Свинство со стороны Евклидовых Журналов не поддерживать Athens login:(
(Ответить) (Thread)
[User Picture]From: sowa
2004-04-21 05:01 pm
Линк вообще не открывается. Расскажите.

Если я не ошибаюсь, у теоремы Харрингтона-Париса есть доказательство (или даже таким было первое доказательство), не зависящее ни от теоремы Геделя, ни от диагонализации.
(Ответить) (Thread)
[User Picture]From: avva
2004-04-25 12:58 pm
Вот, написал.

Если не ошибаюсь, первое доказательство Харрингтона-Париса использовало вторую теорему Гёделя, а после уже они придумали доказательство через нестадартные модели PA. Впрочем, очень может быть, что ошибаюсь.
(Ответить) (Parent) (Thread)
[User Picture]From: french_man
2004-04-22 04:14 am
Ну, в библиотеке я тоже могу найти. Я думал, у тебя есть доступ к файлу.
(Ответить) (Thread)
[User Picture]From: avva
2004-04-25 12:59 pm
Увы.
(Ответить) (Parent) (Thread)
[User Picture]From: myjj
2004-04-23 03:39 am
очень здорово было бы
(Ответить) (Thread)
[User Picture]From: avva
2004-04-25 01:00 pm
См. здесь.
(Ответить) (Parent) (Thread)
[User Picture]From: myjj
2004-04-26 12:06 am
н-да,
прошу прощения, погорячился.
утешает, что таки нашлись люди, которым было понятно.
мне вот понравилось упомянутая континуум-гипотеза (яндекс маленько просветил).
не знаете ли, гденть есть подробности про решение?
попроще, для чайников.
вас просить объяснить не буду - обидно, человек старается-старается, а ты ничего не понимаешь.

(Ответить) (Parent) (Thread)
[User Picture]From: avva
2004-04-26 03:42 am
На самом деле много где (в любом достаточно хорошем учебнике аксиоматической теории множеств), но конкретную книгу не могу посоветовать. Если где-то есть про форсинг (forcing) - то это оно и есть.
(Ответить) (Parent) (Thread)