о противоречивости арифметики пеано (математическое)

[avva]

Эдвард Нельсон, профессор Принстонского университета, объявил, что он доказал противоречивость арифметики Пеано (PA) (Update: если страница не открывается, то вот кэш-версия). Он выложил эскиз своего доказательства; полное и строгое доказательство он все еще пишет, и собирается выкладывать его по частям вместе с формальной проверкой с помощью программы, которую он сам написал.

Нельсон - не сумасброд, а настоящий математик. Его доказательство в принципе несложно, и опирается не недавно найденное новое доказательство второй теоремы Геделя о неполноте (той, которая утверждает, что достаточно сложная система аксиом не может доказать свою непротиворечивость, если она непротиворечива).

Я достаточно помню в этой области, чтобы понять его основные идеи, но недостаточно, чтобы строго их проверить. Мне кажется очень вероятным, что где-то у него есть ошибка. Думаю, в ближайшие пару дней это станет ясно.

P.S. Можно помечтать о том, что будет, если ошибки нет. Конечно, это тогда автоматически самый знаменитый и важный результат в логике за последние сто лет, и немедленный кризис в основаниях математики. Если PA противоречива, то и теория множеств, на которую опирается вся современная математика, тоже противоречива. Будет кризис в основаниях математики, похожий на тот, что случился с открытием парадокса Расселла. Нужно будет заменить теорию множеств на такую, которая все еще достаточно мощна, чтобы поддерживать современную математику, но не доказывает полную неограниченную индукцию в арифметике. Не факт, что это будет просто сделать. "Обычные" математики, не связанные с логикой, конечно, особенно волноваться не будут, как не волновались они и 100 лет назад. Но все равно, если это верно, то гигантской важности результат.

P.P.S. Обсуждение в блоге Джона Баэза.

Comments

модель PA

[falcao.livejournal.com]

По поводу индукции я ответил чуть ниже. Это не совсем то, что нужно, то есть при этом нет предъявления какого-то конкретного места в рассуждении, где происходит "нарушение".

Даже вне связи с Генценом, вопрос можно поставить так: если PA считается противоречивой, то схема аксиом индукции проводит к противоречию, но при этом существуют конкретные арифметические свойства, к которым индукцию применять нельзя. Вот их хотелось бы увидеть, и понять, почему такое возможно.

Насчёт "тестирования" PA я согласен, что оно не проводилось на уровне попытки что-то "необычное" вывести из этих аксиом, но тут ситуация не такая, как с ZF. Дело в том, что для ZF мы не имеем "конкретной" модели, с которой можем "работать". Но для PA есть "стандартная" модель, к которой все привыкли и относительно которой принято было считать, что она "существует". Это ведь довольно простая конструкция, и если даже она "не имеет смысла", то сколько всего "монстрообразного" должно будет вместе с этим "упасть"?

Я думаю, вопрос надо ставить как-то примерно так: почему то, что считалось моделью PA, не оказывается таковой? Должна быть какая-то смысловая ошибка, а пока на неё не указано, проще поверить в то, что в формальных рассуждениях чего-то напутали.

Re: модель PA

[markvs.livejournal.com]

Судя по обсуждению, у Нельсона там абсолютная чушь написана. Вообще объявлять такой результат, не имея подробного читабельного текста, очень плохой стиль. Думаю, что сейчас сезон номинаций на всякие призы, а у Нельсона как раз не хватает денег. Вот, например, есть Shaw prize. Скоро срок представления номинаций. Там несколько человек в комитете из Принстона. Цена - $1000000, http://www.shawprize.org/en/ .

предварительные обсуждения

[falcao.livejournal.com]

Я уже выразил степень своей "веры в чудеса", сравнив утверждение Нельсона с заявлением об обнаружении "сверхсветовой черепахи" :)

Вопросы научной этики, а также "делёжки" грантов я не обсуждаю, так как это всё находится несколько в стороне от сути. Независимо от того, полон ли текст, там есть какие-то мысли, которые уже можно обсуждать -- тем более, что автор на возражения как-то реагирует. Вопрос о полном тексте мог бы иметь значение только в порядке присуждения какой-то "премии", то есть в случае, когда "обратный ход" сделать уже невозможно.

В любом случае, если есть рассуждение, которое содержит в себе элементы чего-то "разумного", то я думаю, что это уже повод для обсуждения -- даже при полной кажущейся абсурдности вывода. Чаще всего оказывается, что сам вывод, конечно, неверен, но из рассуждения можно извлечь нечто более "слабое". А это может представлять известную ценность.

Re: предварительные обсуждения

[markvs.livejournal.com]

Ты посмотри http://www.math.princeton.edu/~nelson/papers/outline.pdf
Там есть параграф Que на странице 5. Достаточно прочитать первые 4 строки этого параграфа. Остальное можно уже не читать. Возможно, я не прав насчет денег и там скорее медицинская причина. В Принстоне есть уже один гениальный сумасшедший, Нэш. Возможно, появился еще один.

Re: предварительные обсуждения

[markvs.livejournal.com]

Параграф называется Qea.

Re: предварительные обсуждения

[markvs.livejournal.com]

Интересно, вытекает ли из доказательства Нельсона существование неизвестного науке целого числа между 6 и 7? Раз принцип индукции неверен, вполне может и вытекать.

машинная проверка

[falcao.livejournal.com]

Я видел это место, но не понимаю, чем оно более "сумасшедшее" по сравнению со всем остальным. Ведь ясно же, что сам тезис об обнаружении противоречия не где-нибудь, а в PA звучит "вызывающе". И автор здесь даёт понять, что он и сам пока как бы сомневается, и сам предмет логики -- это не матанализ (normal science), поэтому идея использовать программы типа автоматической проверки (или генерации) доказательств выглядит как раз более чем разумно.

Вообще, я думаю, что при помощи "иронии" такие вещи не анализируются. Это надо воспринимать как "вызов", причём достаточно "изощрённый". Это если и "сумасшествие", то совсем не того уровня, когда в "доказательстве" ВТФ автор чётное число 2k берёт и почему-то записывает в виде 2^k. После чего всё "блестяще" доказывается.

Здесь, кстати, автор вообще мог бы сказать прямо: вот у меня есть рассуждение, ведущее к неправдоподобному выводу, а я не могу в нём найти ошибку. При таком подходе всё вообще находится "в рамках приличий".

[(Anonymous)]

[Я здесь же отвечу на другой Ваш комментарий выше по ветке, чтобы не дробить.]
Как раз назвать свой вывод неправдоподобным Нельсон никак не мог, он же ультрафинитист. Так что у него давно готов ответ на вопрос, почему стандартная модель - не модель PA и в чем тут смысловая ошибка. Не думаю, правда, что нам будет легко понять этот ответ. Но по крайней мере, если быстро не найдется формальная ошибка, будет сильный стимул попытаться прочитать наконец и Нельсона, и Есенина-Вольпина, и разные другие мистические трактаты. С другой стороны, "ангажированность" Нельсона - один из двух "внематематических" аргументов против (второй - возраст и возможная болезнь; деньги тут явно ни при чем).

К чему конкретно нельзя применить индукцию - интересный и очень важный вопрос. Я боюсь, что он трудный. Нельсон существенно использует доказательство Чейтина второй теоремы Геделя. Эта штука обсуждалась давно, и мне кажется, что более-менее общее мнение состоит в том, что формализация в PA этого доказательства гораздо сложнее, чем формализация исходного доказательства Геделя. Собственно, колмогоровская сложность уже является вещью сомнительной для последовательного конструктивиста, и потому ее формализация в PA должна, скорее всего, содержать "неестественные" этапы. Так что я полагаю, что из доказательства Нельсона (если оно верно) мы осмысленного ответа не получим. Обнаружится какая-то арифметическая формула на пять страниц, не имеющая видимого смысла, мы узнаем, что к ней нельзя применять индукцию, и что дальше? Высечь эту формулу на камне и мазать жертвенной кровью?

[(Anonymous)]

Сорри, что встреваю. Мне кажется, что если внимательно проанализировать эту формулу на 5 страниц, даже не вдаваясь слишком глубоко в её смысл, то возможно, что в ней обнаружатся какие-нибудь специфические симметрии. Например, в ней могут быть куски, похожие на формулировки утверждений о неподвижных точках чего-нибудь. Может оказаться (спекуляция), что как раз для формул из определённого класса, для которого характерно наличие таких кусков, индукция в общем виде неприменима. Тогда их придётся запретить, а теоремы о неподвижных точках передоказать какими-нибудь обходными путями.

[(Anonymous)]

Может и вообще повезти, так что формула окажется осмысленная. Но я в такую удачу не верю. Сам факт (это всё в том пока не очень вероятном случае, что ошибок у Нельсона нет) обнаружения противоречия в PA означает, что наши понятия в чем-то ущербны, и только после того, как будут выработаны новые понятия, можно будет надеяться "правильно", то есть с использованием осмысленных промежуточных объектов, доказать противоречивость PA (иными словами, в новой системе понятий всё должно стать более-менее очевидно - и по каким формулам индукция допустима, и как противоречие получать).

хорошие и плохие свойства

[falcao.livejournal.com]

Боюсь, что в терминах "ультрафинитизма" вообще нельзя рассматривать то, что "мы" называем "стандартной моделью" PA.

Я в той или иной мере знаком с идеями Есенина-Вольпина, и думаю, что у него как раз нет ничего "мистического". Более того, он как раз пытался обосновать непротиворечивость даже ZF на базе построения её "как бы модели" на базе "как бы конечного". Многие его соображения уже давно реализованы (хотя бы у Вопенки). Там проблема скорее не в "экзотичности" или "неправдоподобии", а в том, что "неформальные" идеи не доведены до конца.

Что касается "нехорошей" арифметической формулы, то меня здесь вот что интересует. Пусть пока мы вообще не знаем её вид, и рассуждаем "абстрактно". Есть какой-то предикат P(x), и для него известно, что P(0), что P(0)->P(1), и так далее. Пусть оказалось, что нельзя применить индукцию. Это что-то значит относительно P. Однако для "простых" свойств мы вроде как убеждены, что всё хорошо. Значит, где-то должна проявиться специфика конкретного P, которое является "плохим". И вот здесь непонятно, что это в принципе может значить. Потому что стандартное "убедительное" рассуждение насчёт того, почему принцип индукции вообще "верен", никак не опирается на конкретную специфику свойства P.

Я пока не могу представить себе ничего иного кроме как с трудностью и со временем установления "истинности" P(k) при увеличении k.