![[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 10:56 am (UTC)no subject
Date: 2011-09-28 11:02 am (UTC)no subject
Date: 2011-09-28 12:36 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 04:10 pm (UTC)Генцен
Date: 2011-09-28 03:49 pm (UTC)Но ведь одно дело противоречивость системы как таковой, и совсем другое -- ошибка в конкретном доказательстве. Конечно, если я сначала выведу противоречие, то потом из него выведу что угодно, то Генцен ведь так не поступает!
Вообще, я бы не очень удивился нахождению противоречия в формальной теории ZF (её как следует на этот предмет не тестировали, мне кажется), но PA -- это уже слишком. Если первое можно было бы сравнить с обнаружением сверхсветовых "материальных" частиц, то второе -- это что-то вроде утверждения, что зенонова черепаха движется быстрее света! :)
no subject
Date: 2011-09-28 04:02 pm (UTC)PA на самом деле тоже не очень тестировали - "больших индукций" в математической практике мало. Реальная математика живет в маленьком кусочке. Так что "положительная программа" Нельсона важнее. Если удастся всю "повседневную математику" погрузить в более слабую теорию, то, во-первых, непротиворечивость PA станет не важна, а во-вторых, в противоречивость будет гораздо легче поверить.
модель PA
Date: 2011-09-29 02:57 am (UTC)Даже вне связи с Генценом, вопрос можно поставить так: если PA считается противоречивой, то схема аксиом индукции проводит к противоречию, но при этом существуют конкретные арифметические свойства, к которым индукцию применять нельзя. Вот их хотелось бы увидеть, и понять, почему такое возможно.
Насчёт "тестирования" PA я согласен, что оно не проводилось на уровне попытки что-то "необычное" вывести из этих аксиом, но тут ситуация не такая, как с ZF. Дело в том, что для ZF мы не имеем "конкретной" модели, с которой можем "работать". Но для PA есть "стандартная" модель, к которой все привыкли и относительно которой принято было считать, что она "существует". Это ведь довольно простая конструкция, и если даже она "не имеет смысла", то сколько всего "монстрообразного" должно будет вместе с этим "упасть"?
Я думаю, вопрос надо ставить как-то примерно так: почему то, что считалось моделью PA, не оказывается таковой? Должна быть какая-то смысловая ошибка, а пока на неё не указано, проще поверить в то, что в формальных рассуждениях чего-то напутали.
Re: модель PA
Date: 2011-09-29 05:46 am (UTC)предварительные обсуждения
Date: 2011-09-29 06:15 am (UTC)Вопросы научной этики, а также "делёжки" грантов я не обсуждаю, так как это всё находится несколько в стороне от сути. Независимо от того, полон ли текст, там есть какие-то мысли, которые уже можно обсуждать -- тем более, что автор на возражения как-то реагирует. Вопрос о полном тексте мог бы иметь значение только в порядке присуждения какой-то "премии", то есть в случае, когда "обратный ход" сделать уже невозможно.
В любом случае, если есть рассуждение, которое содержит в себе элементы чего-то "разумного", то я думаю, что это уже повод для обсуждения -- даже при полной кажущейся абсурдности вывода. Чаще всего оказывается, что сам вывод, конечно, неверен, но из рассуждения можно извлечь нечто более "слабое". А это может представлять известную ценность.
Re: предварительные обсуждения
Date: 2011-09-29 11:53 am (UTC)Там есть параграф Que на странице 5. Достаточно прочитать первые 4 строки этого параграфа. Остальное можно уже не читать. Возможно, я не прав насчет денег и там скорее медицинская причина. В Принстоне есть уже один гениальный сумасшедший, Нэш. Возможно, появился еще один.
Re: предварительные обсуждения
Date: 2011-09-29 12:01 pm (UTC)Re: предварительные обсуждения
Date: 2011-09-29 12:05 pm (UTC)машинная проверка
Date: 2011-09-29 12:55 pm (UTC)Вообще, я думаю, что при помощи "иронии" такие вещи не анализируются. Это надо воспринимать как "вызов", причём достаточно "изощрённый". Это если и "сумасшествие", то совсем не того уровня, когда в "доказательстве" ВТФ автор чётное число 2k берёт и почему-то записывает в виде 2k. После чего всё "блестяще" доказывается.
Здесь, кстати, автор вообще мог бы сказать прямо: вот у меня есть рассуждение, ведущее к неправдоподобному выводу, а я не могу в нём найти ошибку. При таком подходе всё вообще находится "в рамках приличий".
no subject
Date: 2011-09-29 02:04 pm (UTC)Как раз назвать свой вывод неправдоподобным Нельсон никак не мог, он же ультрафинитист. Так что у него давно готов ответ на вопрос, почему стандартная модель - не модель PA и в чем тут смысловая ошибка. Не думаю, правда, что нам будет легко понять этот ответ. Но по крайней мере, если быстро не найдется формальная ошибка, будет сильный стимул попытаться прочитать наконец и Нельсона, и Есенина-Вольпина, и разные другие мистические трактаты. С другой стороны, "ангажированность" Нельсона - один из двух "внематематических" аргументов против (второй - возраст и возможная болезнь; деньги тут явно ни при чем).
К чему конкретно нельзя применить индукцию - интересный и очень важный вопрос. Я боюсь, что он трудный. Нельсон существенно использует доказательство Чейтина второй теоремы Геделя. Эта штука обсуждалась давно, и мне кажется, что более-менее общее мнение состоит в том, что формализация в PA этого доказательства гораздо сложнее, чем формализация исходного доказательства Геделя. Собственно, колмогоровская сложность уже является вещью сомнительной для последовательного конструктивиста, и потому ее формализация в PA должна, скорее всего, содержать "неестественные" этапы. Так что я полагаю, что из доказательства Нельсона (если оно верно) мы осмысленного ответа не получим. Обнаружится какая-то арифметическая формула на пять страниц, не имеющая видимого смысла, мы узнаем, что к ней нельзя применять индукцию, и что дальше? Высечь эту формулу на камне и мазать жертвенной кровью?
no subject
Date: 2011-09-29 04:59 pm (UTC)(no subject)
From: (Anonymous) - Date: 2011-09-29 07:49 pm (UTC) - Expandхорошие и плохие свойства
Date: 2011-09-30 06:59 pm (UTC)Я в той или иной мере знаком с идеями Есенина-Вольпина, и думаю, что у него как раз нет ничего "мистического". Более того, он как раз пытался обосновать непротиворечивость даже ZF на базе построения её "как бы модели" на базе "как бы конечного". Многие его соображения уже давно реализованы (хотя бы у Вопенки). Там проблема скорее не в "экзотичности" или "неправдоподобии", а в том, что "неформальные" идеи не доведены до конца.
Что касается "нехорошей" арифметической формулы, то меня здесь вот что интересует. Пусть пока мы вообще не знаем её вид, и рассуждаем "абстрактно". Есть какой-то предикат P(x), и для него известно, что P(0), что P(0)->P(1), и так далее. Пусть оказалось, что нельзя применить индукцию. Это что-то значит относительно P. Однако для "простых" свойств мы вроде как убеждены, что всё хорошо. Значит, где-то должна проявиться специфика конкретного P, которое является "плохим". И вот здесь непонятно, что это в принципе может значить. Потому что стандартное "убедительное" рассуждение насчёт того, почему принцип индукции вообще "верен", никак не опирается на конкретную специфику свойства P.
Я пока не могу представить себе ничего иного кроме как с трудностью и со временем установления "истинности" P(k) при увеличении k.
Re: Генцен
Date: 2011-09-28 04:06 pm (UTC)поимка
Date: 2011-09-29 02:48 am (UTC)Вот с примитивно-рекурсивными функциями уже гораздо интереснее, но здесь-то и нужно попытаться представить себе, "как такое может быть?" Хотелось бы проследить более конкретно, где и как происходит "нарушение". Я так понимаю, что если такая функция конкретно предъявляется, то её мы можем "поймать" некий момент, когда через очередной оператор подстановки или рекурсии что-то не проходит. А такое довольно трудно себе представить.
Re: поимка
Date: 2011-09-29 05:38 am (UTC)Действительно, там нужно несколько изменить определение истинности.
> Хотелось бы проследить более конкретно, где и как происходит "нарушение". Я так понимаю, что если такая функция конкретно предъявляется, то её мы можем "поймать" некий момент, когда через очередной оператор подстановки или рекурсии что-то не проходит.
Насколько я понял, нет. Но тут лучше подождать обещанного примера.
обозримое и необозримое
Date: 2011-09-29 06:25 am (UTC)Возможен другой вариант, когда "обозримо" доказывается само наличие противоречия "где-то", но при этом оно само не предъявляется. Но в этом случае можно подумать на какую-то ошибку, связанную со "смешиванием" классического типа доказательства с чем-то "ограниченным в средствах". Ясно, скажем, что если натуральный ряд ограничить "обозримыми" по величине числами, и при этом считать, что "необозримые" числа тоже заведомо есть, то здесь противоречие, конечно, получается, но "необозримой" длины.
Мне кажется, в самое ближайшее время всё должно так или иначе проясниться.
Re: обозримое и необозримое
Date: 2011-09-29 08:15 pm (UTC)no subject
Date: 2011-09-28 05:50 pm (UTC)(Из ответа я понял, что я понимал доказательство слишком упрощенно, пропустив несколько шагов; кажется, Тао ошибся похожим образом, то есть возражал не авторскому доказательству.)
no subject
Date: 2011-09-28 06:17 pm (UTC)