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

[avva]

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

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

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

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

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

Comments

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.