![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaЭдвард Нельсон, профессор Принстонского университета, объявил, что он доказал противоречивость арифметики Пеано (PA) (Update: если страница не открывается, то вот кэш-версия). Он выложил эскиз своего доказательства; полное и строгое доказательство он все еще пишет, и собирается выкладывать его по частям вместе с формальной проверкой с помощью программы, которую он сам написал.
Нельсон - не сумасброд, а настоящий математик. Его доказательство в принципе несложно, и опирается не недавно найденное новое доказательство второй теоремы Геделя о неполноте (той, которая утверждает, что достаточно сложная система аксиом не может доказать свою непротиворечивость, если она непротиворечива).
Я достаточно помню в этой области, чтобы понять его основные идеи, но недостаточно, чтобы строго их проверить. Мне кажется очень вероятным, что где-то у него есть ошибка. Думаю, в ближайшие пару дней это станет ясно.
P.S. Можно помечтать о том, что будет, если ошибки нет. Конечно, это тогда автоматически самый знаменитый и важный результат в логике за последние сто лет, и немедленный кризис в основаниях математики. Если PA противоречива, то и теория множеств, на которую опирается вся современная математика, тоже противоречива. Будет кризис в основаниях математики, похожий на тот, что случился с открытием парадокса Расселла. Нужно будет заменить теорию множеств на такую, которая все еще достаточно мощна, чтобы поддерживать современную математику, но не доказывает полную неограниченную индукцию в арифметике. Не факт, что это будет просто сделать. "Обычные" математики, не связанные с логикой, конечно, особенно волноваться не будут, как не волновались они и 100 лет назад. Но все равно, если это верно, то гигантской важности результат.
P.P.S. Обсуждение в блоге Джона Баэза.
Нельсон - не сумасброд, а настоящий математик. Его доказательство в принципе несложно, и опирается не недавно найденное новое доказательство второй теоремы Геделя о неполноте (той, которая утверждает, что достаточно сложная система аксиом не может доказать свою непротиворечивость, если она непротиворечива).
Я достаточно помню в этой области, чтобы понять его основные идеи, но недостаточно, чтобы строго их проверить. Мне кажется очень вероятным, что где-то у него есть ошибка. Думаю, в ближайшие пару дней это станет ясно.
P.S. Можно помечтать о том, что будет, если ошибки нет. Конечно, это тогда автоматически самый знаменитый и важный результат в логике за последние сто лет, и немедленный кризис в основаниях математики. Если PA противоречива, то и теория множеств, на которую опирается вся современная математика, тоже противоречива. Будет кризис в основаниях математики, похожий на тот, что случился с открытием парадокса Расселла. Нужно будет заменить теорию множеств на такую, которая все еще достаточно мощна, чтобы поддерживать современную математику, но не доказывает полную неограниченную индукцию в арифметике. Не факт, что это будет просто сделать. "Обычные" математики, не связанные с логикой, конечно, особенно волноваться не будут, как не волновались они и 100 лет назад. Но все равно, если это верно, то гигантской важности результат.
P.P.S. Обсуждение в блоге Джона Баэза.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2011-09-28 09:22 am (UTC)Во что же теперь верить...
no subject
Date: 2011-09-28 09:56 am (UTC)no subject
Date: 2011-09-28 09:58 am (UTC)no subject
Date: 2011-09-28 09:59 am (UTC)simply by inspection"). Кажется, в математике тоже встаёт проблема спама :-)
no subject
Date: 2011-09-28 10:14 am (UTC)no subject
Date: 2011-09-28 10:18 am (UTC)А вы уже разобрались в последствиях этого доказательства? Все доказательства по индукции становятся невалидными в результате (если Эдвард Нельсон нигде не напутал, конечно) или только какие-то более тонкие эффекты вылезают?
no subject
Date: 2011-09-28 10:22 am (UTC)Не могли бы вы дать ссылку на это доказательство?
no subject
Date: 2011-09-28 10:28 am (UTC)Думаю, что если результат Нельсона верен, хоть и не верится в это, то будет кризис в основаниях математики, похожий на тот, что случился с открытием парадокса Расселла. Нужно будет заменить теорию множеств (т.к. она тоже получается противоречива) на такую, которая все еще достаточно мощна, чтобы поддерживать современную математику, но не доказывает полную неограниченную индукцию в арифметике. Не факт, что это будет просто сделать. "Обычные" математики, не связанные с логикой, конечно, особенно волноваться не будут, как не волновались они и 100 лет назад. Но все равно это тогда автоматически самый важный результат в логике и основаниях математики за последние сто лет.
no subject
Date: 2011-09-28 10:32 am (UTC)no subject
Date: 2011-09-28 10:56 am (UTC)no subject
Date: 2011-09-28 11:02 am (UTC)no subject
Date: 2011-09-28 11:32 am (UTC)no subject
Date: 2011-09-28 12:36 pm (UTC)no subject
Date: 2011-09-28 12:45 pm (UTC)no subject
Date: 2011-09-28 01:23 pm (UTC)no subject
Date: 2011-09-28 01:25 pm (UTC)http://en.wikipedia.org/wiki/Internal_Set_Theory
no subject
Date: 2011-09-28 02:25 pm (UTC)no subject
Date: 2011-09-28 03:10 pm (UTC)Вообще, сочетание двух таких утверждений считается не очень-то хорошим тоном. Но можно считать, что матанщик, который неожиданно решил заняться логикой, заслуживает снисхождения.
Генцен
Date: 2011-09-28 03:49 pm (UTC)Но ведь одно дело противоречивость системы как таковой, и совсем другое -- ошибка в конкретном доказательстве. Конечно, если я сначала выведу противоречие, то потом из него выведу что угодно, то Генцен ведь так не поступает!
Вообще, я бы не очень удивился нахождению противоречия в формальной теории ZF (её как следует на этот предмет не тестировали, мне кажется), но PA -- это уже слишком. Если первое можно было бы сравнить с обнаружением сверхсветовых "материальных" частиц, то второе -- это что-то вроде утверждения, что зенонова черепаха движется быстрее света! :)
no subject
Date: 2011-09-28 03:53 pm (UTC)no subject
Date: 2011-09-28 04:02 pm (UTC)PA на самом деле тоже не очень тестировали - "больших индукций" в математической практике мало. Реальная математика живет в маленьком кусочке. Так что "положительная программа" Нельсона важнее. Если удастся всю "повседневную математику" погрузить в более слабую теорию, то, во-первых, непротиворечивость PA станет не важна, а во-вторых, в противоречивость будет гораздо легче поверить.
Re: Генцен
Date: 2011-09-28 04:06 pm (UTC)no subject
Date: 2011-09-28 04:10 pm (UTC)no subject
Date: 2011-09-28 04:40 pm (UTC)no subject
Date: 2011-09-28 04:41 pm (UTC)Но ни разу не слышал, чтобы кто-то ругался на исчисление предикатов.
А с виду, это самая кривая конструкция в основаниях.
Но я, конечно, не настоящий сварщик.