?

Log in

о непротиворечивости - Поклонник деепричастий [entries|archive|friends|userinfo]
Anatoly Vorobey

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

Links
[Links:| English-language weblog ]

о непротиворечивости [май. 1, 2004|05:30 pm]
Anatoly Vorobey
Брайан Форд, докторант из MIT, опубликовал интересный препринт, в котором он строит частичные модели ZF (теории множеств Цермело-Франкеля) внутри ZF. Одним из его результатов является доказательство непротиворечивости ZF внутри ZF. Скорее всего, в этом есть ошибка, но как минимум не тривиальная — автор не шарлатан и не сумасшедший, статья написана хорошо и вдумчиво, и использует действительно необычный, и возможно интересный, метод конструирования моделей. Я только бегло просмотрел её; очень хочется распечатать и проштудировать как следует, но совершенно не могу на это сейчас выделить времени, очень жаль. Сейчас её обсуждают в рассылке FOM; пока что Robert Solovay нашёл несколько небольших погрешностей, которые кажутся исправимыми, но всё ещё впереди.

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

Comments:
[User Picture]From: burrru
2004-05-01 07:47 am
Скажите, как подписаться на FOM? А то я кроме своих кривых и многочленов ничем не интересовался в последнее время.
(Ответить) (Thread)
[User Picture]From: avva
2004-05-01 08:14 am
Здесь, но подписка не автоматическая, т.к. рассылкка закрытая. Нужно написать модератору и объяснить, кто ты такой и зачем хочешь подписаться.
(Ответить) (Parent) (Thread)
[User Picture]From: burrru
2004-05-01 02:17 pm
Спасибо. Посмотрел архивы. Интересно, но слишком специально для меня... Возвращаюсь к теории исключения, попробую связать ее с группами кос.
(Ответить) (Parent) (Thread)
[User Picture]From: monomyth
2004-05-01 07:51 am

Отсюда вопрос.

Что можно хорошего почитать про логику и "как она есть" ?
(Ответить) (Thread)
[User Picture]From: myjj
2004-05-01 07:56 am

древнеримская поговорка

Юпитер сер доказал, что прав - значит он неправ. :)
(Ответить) (Thread)
[User Picture]From: kobak
2004-05-01 08:35 am
Это в свою очередь будет ужасным ударом по основаниям математики и логики, последствия которого трудно предсказать (хотя большинство математиков скорее всего не обратят на него особого внимания, т.к. не интересуются логикой или основаниями математики).

Скорее всего, никто просто не поверит этому результату -- и всё тут. То есть, даже если его "признают корректным" и опубликуют в каком-нибудь журнале, большинство математиков будет считать, что где-то там есть какая-то ошибка.
(Ответить) (Thread)
[User Picture]From: avva
2004-05-01 09:01 am
Не думаю; доказательство там не особенно сложное.
(Ответить) (Parent) (Thread)
[User Picture]From: lnvp
2004-05-01 03:47 pm
Является ли автор доказательства профессиональным логиком (сколько лет он проработал в логике, каковы предыдущие результаты?) Имеются ли отзывы / рецензии сильных профессиональных логиков? Внешне история выглядит как типичная деятельность не в своём огороде (типа этой, например); мне самому разбираться статью про ZF, наверно, не по силам. Не думаю, чтобы шансы на великое потрясение были велики. Большую теорему Ферма сколько раз неспециалисты доказывали, а доказал-таки математик, посвятивший практически всю профессиональную деятельность этому.
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2004-05-01 03:55 pm
Нет, автор доказательства не профессиональный логик и тем более не профессионал в теории множеств.

Видите ли, дело тут в том, что именно в аксиоматической теории множеств есть очень хороший пример непрофессионала, никогда раньше не делавшего ничего в этой области, и доказавшего самый важный результат 20-го века (Коэн, независимость аксиомы выбора и континуум-гипотезы). Так что опыт показывает, что всякое бывает.

Не думаю, чтобы шансы на великое потрясение были велики.

Я считаю, что они почти исчезающе малы, и что Форд ошибся почти наверняка, но это не значит, что его статья не заслуживает внимания.
(Ответить) (Parent) (Thread)
[User Picture]From: lnvp
2004-05-01 04:22 pm
Интересный пример. Любопытно, почему вам интересны темы около теоремы Гёделя, а не, скажем, аксиома выбора и её заменители?
(Ответить) (Parent) (Thread)
[User Picture]From: sowa
2004-05-04 12:32 am
Пример Коэна - до некоторой степени красивая легенда. У Коэна был серьезный интерес к логике до того, как он занялся независимостью континуум-гипотезы.
(Ответить) (Parent) (Thread)
[User Picture]From: garvej
2004-05-01 09:35 am
Правильность математического доказательства -- это не вопрос веры. Вряд ли вообще когда-либо было такое, чтобы результат "признали корректным" и при этом большинство математиков считало, что "там есть какая-то ошибка".

Если ведущие специалисты проверят доказательство и всё окажется правильно, то шум поднимется не меньше чем после обнаружения "парадоксов теории множеств".
(Ответить) (Parent) (Thread)
[User Picture]From: kobak
2004-05-01 12:24 pm
Не могу полностью с Вами согласиться. (Дальнейшее следует читать в предположении, что предложенное док-во очень сложное; avva уже сказал, что оно таковым не является.)

Правильность математического док-ва -- действительно не вопрос веры. Однако доверие к нему неспециалиста -- совсем другое дело. То, что я считаю теорему Ферма доказанной, совершенно не значит, что я могу разобраться в существующем док-ве (более того, я заведомо не могу за разумное время это сделать).

Предположим, появляется некое очень сложное док-во непротиворечивости ZF внутри ZF. Его никто не понимает, кроме кучки специалистов, которые через пару лет говорят, что да, мол, похоже, всё правильно. Ничто в таком случае не будет мне мешать *верить* в то, что все они ошибаются и на самом деле в док-ве есть ошибка; потому что моя вера в НЕпротиворечивость ZF гораздо сильнее.
(Ответить) (Parent) (Thread)
[User Picture]From: garvej
2004-05-01 03:53 pm
Насчет доверия к результату, в котором нет возможности разобраться, я бы сказал так: неспециалист полагается на мнение того (а желательно тех), кого он считает большим специалистом.

Для нарисованного сценария, когда кучка специалистов говорит невнятное "да, мол, похоже, всё правильно" -- можно и сомневаться. Только мне кажется, что вряд ли ведущие специалисты будут высказываться (через пару лет) в таком духе: "похоже, всё правильно". Тут вопрос чести :) То есть, либо да, либо нет.

На практике новое доказательство -- это не просто набор силлогизмов. Новое доказательство -- это новые идеи, методы. Эти идеи как правило сразу идут в оборот. Часто сразу появляются упрощения исходного доказательства, доказательства новых результатов в данном направлении и т.д. И тогда ни у кого сомнений не остаётся. Примеры -- доказательство Коэна независимости CH от ZFC, та же теорема Ферма.

Если в доказательстве никто не разберётся, то его статус останется неопределённым, и тогда будет простор для сомнений. Я не знаю случаев, когда доказательство важной теоремы долгое время находилось бы в таком подвешенном состоянии.
Может кто приведёт пример? Перельмана не предлагать :)
(Ответить) (Parent) (Thread)
[User Picture]From: ubaldus
2004-05-01 06:48 pm
де Бранжес и его доказательство гипотезы Бибербаха.
Там было двести страниц какой-то фигни, которыю никто не хотел читать, так как де Бранжес всем надоел неверными доказательствами важных теорем.
Потом он поехал в Ленинград, там долго обьяснял все это умным людям, пока они ему не поверили и не упростили доказательство до 30 страниц внятного текста.

По крайней мере, так говорят люди знакомые с этой историей.
(Ответить) (Parent) (Thread)
[User Picture]From: a_konst
2004-05-02 10:06 pm
любопытно, надо будет узнать поточнее у этих людей :)

Кстати, насколько я знаю, читается все же "де Бранж" без "-ес" - во-первых, я слышал как его так называли те кто с ним лично общался, во-вторых, во французском языке окончание "es" немое.
Думаю, по-русски следует писать так, как читается (пишем же "Айвенго").
(Ответить) (Parent) (Thread)
[User Picture]From: ubaldus
2004-05-03 10:13 am
http://news.uns.purdue.edu/UNS/html4ever/840828.Branges.Mathematics.html

A climate of skepticism had been created by the erroneous proof of the Bieberbach conjecture which had been announced in a Soviet journal. In fact several false proofs of the Bieberbach conjecture litter the historical landscape; and it was the general expectation that some subtle error would be found in the present argument.

To their surprise, the participants of the Leningrad Seminar in Geometric Function Theory became convinced of the validity of the argument during five sessions which took place in April and May. Each session lasted late into the evening and was interrupted only by a break for tea. Two members of the seminar, E. V. Emel'ianov and I. M. Milin, submitted written reports confirming the proof and presenting variants which they considered advantageous. In June, Professor de Branges worked with the seminar leader, Professor G. V. Kuz'mina, to consolidate the findings of the seminar. The resulting argument was accepted for release by Academician L. D. Faddeev, the director of the Leningrad Branch of the V. A. Steklov Mathematical Institute. The 21 page preprint is available both in Russian and in English.

(Ответить) (Parent) (Thread)
From: ignat
2004-05-03 01:13 pm
Может кто приведёт пример?

Есть такая проблема Кеплера о плотной упаковке шаров. Хейлс (Thomas C. Hales) вроде как доказал, но его доказательство в течение шести лет так и не смогли проверить математики под руководством Фейеша Тота. Сейчас Анналы опубликуют его статью "как есть" (беспрецедентный шаг на самом деле!), с припиской, что рецензенты не со всем смогли разобраться.

Хейлс инициировал "Flyspeck Project" по автоматической проверке своего доказательства в системе CAML, но оно настолько огромное и сложное, что для его завершения потребуется ещё 20 лет. Подробности тут:
http://www.math.pitt.edu/~thales/flyspeck/
(Ответить) (Parent) (Thread)
[User Picture]From: kapahel
2004-05-01 03:41 pm
всё равно люди живут не в ZF, а в «идеальном мире множеств»
(Ответить) (Parent) (Thread)
[User Picture]From: ella_p
2004-05-01 08:43 am
Авва, а вы вот можете объяснить совсем чайнику: почему при этом под ударом оказывается теория ZF, а не вторая теорема Геделя? Она "главнее", то есть теория ZF без нее жить не может, а она без этой теории за милую душу?
Сразу предупреждаю, что я про конкретно эти штуки ничего не знаю. Меня заинтересовало само соотношение.
(Ответить) (Thread)
[User Picture]From: mi_b
2004-05-01 08:47 am
Потому что теория ZF - набор аксиом (и правил вывода). Принимать их или нет - вопрос веры в их "осмысленность", в частном случае, в непротиворечивость.

Теорема Геделя - доказанная теоремма, поэтому, если мы принимаем набор аксиом, из которых она выведена, мы должны принять и ее.
(Ответить) (Parent) (Thread)
[User Picture]From: ella_p
2004-05-01 09:06 am
Спасибо!
(Ответить) (Parent) (Thread)
From: (Anonymous)
2004-05-01 08:50 am

Whoah.

Wish Acrobat worked on this computer. That would be something to see.

--PF (http://www.m14m.net/pf)
(Ответить) (Thread)
[User Picture]From: sinistrorsum
2004-05-01 01:06 pm
Верно ли, что Брайан Форд - не математик и это его первая работа по математике?
(Ответить) (Thread)
[User Picture]From: avva
2004-05-01 03:57 pm
Да, вроде бы он computer scientist, и предыдущие его работы были связаны больше с CS, чем с математикой, или на стыке. Но в этом ничего зазорного нет, конечно. Его статья написана грамотно и, вполне возможно, представляет независимый интерес даже если результат о противоречивости ZF окажется ошибочным (в чём практически никто пока что не сомневается).
(Ответить) (Parent) (Thread)
[User Picture]From: flaass
2004-05-02 11:52 pm
Мечта каждого математика - доказать, что 0=1. Но боюсь, тут этого не случится.
(Ответить) (Thread)
From: ignat
2004-05-03 12:43 pm
Чур! Чур!

Взорвать Вселенную -- разве стоит к этому стремиться? То ли дело -- выращивать цветы.
(Ответить) (Parent) (Thread)
From: oblomov_jerusal
2004-05-04 11:57 pm
Дочитал вчера доказательство. По-моему, используя метод автора в обычной ZF, (т.е. со схемой замены, и единственный вид терма - переменная) можно определить понятие истинности, и тем самым показать противоречивость теории несколько проще, чем в статье. (Автор доказывает более сильное утверждение - противоречивость системы Цермело (без замены)).
(Ответить) (Thread)