чудесатее и чудесатее

[avva]

Вдогонку к записи о предложенном доказательстве непротиворечивости теории множеств ZF. Robert Solovay (очень известный специалист в теории множеств) из Беркли нашёл нетривиальную ошибку в доказательстве, которую автор пока не может исправить. Подробности здесь.

Тем временем Рэндалл Холмс, профессор математики из Айдахо, объявил, что придумал доказательство противоречивости PA (арифметики Пеано), причём второго порядка; это значит по сути дела, что натуральных чисел в том виде, в каком мы их обычно понимаем, нет модели; или, иными словами, он нашёл противоречие внутри стандартной модели натуральных чисел N.
Это ещё несравнимо менее вероятно, чем противоречие в теории множеств. Доказательство Холмса можно сгрузить в формате PDF с его домашней страницы, в самом начале её.

Это меня совсем уж возмутило, так что я распечатал доказательство Холмса (небольшое, 6 страниц), прочитал его и нашёл ошибку. В рассылку отправлять не стал, написал прямо ему. Копию помещаю внизу под lj-cut'ом (но её бесполезно читать, если вы не прочитали док-во Холмса, так как я использую введённую им терминологию; само же доказательство я рекомендую читать только особо любопытным или желающим самим найти ошибку. Математической пользы в нём нет).

Dear Prof. Holmes,

Let I be an interpretation for (U,n) and I' an interpretation for
(U',n). I' is said to extend I if U(i) and I(i) are subsets of
U'(i) and I'(i) for all i<=n. What does it mean for a subset of I(i) to
be a subset of I'(i)? I(i) is a pre-interpretation for (U(i),n): a
mapping which sends every assignment of variables <=n to members of the
set U(i), plus a formula <=n, to {0,1}. Members of I(i) are pairs
< <assignment,formula>, truth-value >. So technically speaking, I(i)
being a subset of I'(i) means that truth values of formulas stay the
same as long as assignments remain within original U(i)'s. That
won't preserve correctness. For example, consider a true (in the
standard model) existential sentence (Ex)phi(x), which is mapped to
"false" under some I(i) because U(i-1) is not large enough to contain
the witness for phi(x). Since it's a sentence, it'll have the same truth
value under any assignment (provided I is correct, of course). You want
this sentence to be mapped to "true" when you extend U(i-1) to include
the witness for phi(x); but under your definition the truth value of
(Ex)phi(x) can't change when I is extended to I'. Perhaps what you mean
by I' extending I is that each U'(i) extends U(i), and the set of those
pairs <assignment, formula> which are mapped to "true" by I to remain so
mapped by I'. That won't help you though, because correctness demands
not only conversion of some "false" formulas to "true" formulas under
same assignments as I is extended to I', but also conversion of some
"true" formulas to "false" formulas - for instance, negations of
existential formulas (negation being suitably defined with the help of
your neither/nor operator).
                                                                                
Basically, as you extend U(i) to U'(i), some formulas on which I(i+1)
acts change from "false" to "true", and others from "true" to "false",
under their original assignments within U(i+1). There is no relation
between I' and I that you can formalise and that will allow you to
preserve truth of formulas under extension (assuming correctness of
interpretations). You can still formalise "correct", and you can still
define a veridical interpretation to be such that it can be gradually
extended, preserving correctness, to encompass any given sets, but since
the interpretations aren't conservative extensions of each other, it
doesn't follow that a formula true in such a veridical interpretation
is true in the standard model (and in fact, "veridical" simply collapses
to "correct").
                                                                                
The only thing that can be salvaged from the proof is definability of
truth for purely existential formulas (meaning those that only have
existential quantifiers in the prenex form), which is trivial.

Comments

[ex-ex-ex-gr.livejournal.com]

Он с Холмсом пил коньяк, и жил на Бейкер-стрит...

[oblomov-jerusal.livejournal.com]

А где Holmes утверждает, что расширение должно сохранять корректность?

[avva.livejournal.com]

В определении того, что такое веридическая интрепретация: должна существовать цепочка корректных расширений.

Вообще говоря, некорректные интерпретации Холмсу вообще ничего не дают и ни для чего не могут использоваться.

[oblomov-jerusal.livejournal.com]

Я послал ему письмо:

Considering your preprint on the subject, would it be sufficient in the
definition of veridical interpretation at p.4 instead of requiring
existence of the chain of interpretations simply require existence of an
interpetation I'' correct for (U'', n) such that for each i<=n U'(i) is
subset of U''(i)?
If it isn't, what is purpose of the intermediate members of the chain?

Он мне ответил, что у него там ошибка в доказательстве. Непонятно, можно ли доказать в PA существование veridical interpretations. Если нет, то получается, что в существует арифметическая формула истинности для арифметики, но чтобы доказать это, нужна ZF. По-моему, это все же доказывает несуществование стандартной модели PA (и тем самым, противоречивость ZF).

[avva.livejournal.com]

Considering your preprint on the subject, would it be sufficient in the
definition of veridical interpretation at p.4 instead of requiring
existence of the chain of interpretations simply require existence of an
interpetation I'' correct for (U'', n) such that for each i<=n U'(i) is
subset of U''(i)?
If it isn't, what is purpose of the intermediate members of the chain?

Холмс думал, что расширяя постепенно, по одному члену, он может сохранять истинность формул. Но это не так. Нет сохранения истинности, поэтому понятие veridical interpretation теряет смысл, и означает не более чем correct interpretation. Потому что для любой интерпретации I над множествами U можно построить корректную интерпретацию I'' над множествами U'', так что каждое U'' расширяет некое заданное U', большее U. Для этого достаточно просто использовать истинную интерпретацию, назначающую каждой формуле её значение в стандартной модели, и брать U'' достаточно большими, чтобы на каждом шагу они включали в себя U' плюс всех свидетелей истинных формул предыдущих ступеней, начинающихся с квантора существования. При этом значение первоначальной интерпретации I вообще никак не используется.

Поэтому veridical interpretation=correct interpretation и не более того; и это можно формализовать, но это не влечёт истинность формулы. Истинная формула получает значение истины в корректной интерпретации, но не наоборот.

Если нет, то получается, что в существует арифметическая формула истинности для арифметики,

Нет, не получается. По замыслу Холмса такая формула говорила бы: φ истинна, если существует веридическая интерпретация, дающая φ значение true. Такая формула действительно есть, но она не определяет истинность, т.к. из того факта, что веридическая интерпретация даёт φ значение true не следует истинность &phi.

По-моему, это все же доказывает несуществование стандартной модели PA (и тем самым, противоречивость ZF).

Нет, не доказывает.

[oblomov-jerusal.livejournal.com]

Я понял, проблема с моим определением в том, что расширенная интерпретация не обязательно веридическая

[avva.livejournal.com]

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

[oblomov-jerusal.livejournal.com]

Я забыл добавить, что I'' - расширеине I (т.е. сохраняет определения I) Тогда можно было бы доказывать по индукции по длине формулы, что veridical interpretations присваивают формулам правильные значения истинности. Проблема в том, что Exφ может содержаться в veridical interpretation в которой нет соотв. свидетеля, а расширенная интерпретация, в которой есть такой свидетель, может не быть veridical.

[avva.livejournal.com]

Да, потому что "расширение с сохранением определений" и "корректность" (часть веридикальности) несовместимы, как я ему и написал. Можно сравнить расширения U(i) до U'(i) с ситуацией в теории моделей, когда у нас есть подструктура M и её расширение M'. Тогда, как известно, purely existential formulas остаются истинными при переходе от M к M', но насчёт любых формул это, конечно, неверно. Здесь то же самое происходит со значениями формул в I(i+1), если предположить корректность I и I'.

[oblomov-jerusal.livejournal.com]

Если последовательность множеств U(i) имеет специальный вид: каждый U(i) содержит всех нужных свидетелей для U(i+1), то корректная интерпретация будет присваивать "верные" значения для всех формул, и будет расширяема. В ZF, имея определение для арифметической истинности, легко доказать, что для любого наследственно конечного множества S и любого n есть такая последовательность длины n, что U(n) = S. (Как объясняет Холмс, последовательность строится по индукции с последнего члена). Проблема в том, чтобы доказать, что все "veridical interpretations" имеют такой вид.

[avva.livejournal.com]

Не совсем. Целью Холмса было не доказать, что все "veridical interpretations" имеют такой вид, а доказать, что "veridical interpretation" можно расширить до интерпретации, имеющей такой вид, и при этом сохраняя старые значения формул. Он думал, что у него получилось так определить "correct interpretation" и процесс расширения (через chains), вместе дающие "veridical interpretation", что это определение оказывается definable в стандартной модели. Назовём такую корректную интерпретацию, у которой в U(i) есть все нужные свидетели для U(i+1), для всех формул соответствующей длины, "faithful interpretation". Тогда очевидно, что истина формулы эквивалентна истине в faithful interpretation. Но очевидно и то, что "в лоб" опредлеить faithful interpretation надежды нет именно ввиду теоремы Тарского on the non-definability of truth. Вам кажется, видимо, что Холмс хотел определить veridical interpretation так, чтобы оказалось, что veridical interpretation является faithful interpretation, но это неверно. Его намерение было другим: определить veridical interpretation так, чтобы она была всегда расширима до faithful interpretation, сохраняя при этом существующие значение старых формул с параметрами в старых U(i). Конечно, это невозможно.

[oblomov-jerusal.livejournal.com]

Вам кажется, видимо, что Холмс хотел определить veridical interpretation так, чтобы оказалось, что veridical interpretation является faithful interpretation, но это неверно. Почему неверно? (Впрочем, это только догадки о том, что Холмс имел в виду). Все faithful interpretations корректны и расширяемы, вопрос в том, верно ли обратное.

[avva.livejournal.com]

Потому что faithfulness можно получить, только расширяя что-то неограниченно "вверх", именно потому, что свидетель для любого отдельно взятого квантора существования может найтись только где-то очень далеко вверху. Поэтому если мы хотим иметь всех свидетелей, мы должны быть готовы расшириться вверх неограниченно. Если при этом нам дают определение чего-то, включающее начальные условия, не накладывающие условий на размер (correctness возможна при любых U(i)) плюс условия, позволяющие расширяться вверх неограниченно, логично считать, что нам хотят доказать не faithfulness начального объекта, а то, что этим процессом можно прийти к faithful-объекту. Конечно ,теоретически может оказаться, что условие расширяемости вверх на самом деле каким-то образом влечёт за собой обязательную нужную огромную величину начального объекта, но не очень понятно, с какой это стати и как такое можно было бы доказывать.

[oblomov-jerusal.livejournal.com]

Конечно ,теоретически может оказаться, что условие расширяемости вверх на самом деле каким-то образом влечёт за собой обязательную нужную огромную величину начального объекта, но не очень понятно, с какой это стати и как такое можно было бы доказывать. В принципе так: Если объект не содержит нужного свидетеля, то его нельзя (сохраняя корректность) расширить до объекта, содержащего свидетеля.

[oblomov-jerusal.livejournal.com]

Хм, я уже не вижу ошибки. То, что корректное расширение расширяемой интерпретации расширяемо, это же следует из определений.

[avva.livejournal.com]

Хм, я уже не вижу ошибки. То, что корректное расширение расширяемой интерпретации расширяемо, это же следует из определений.

Ничего не понял ;) но ошибка есть, конечно.

[oblomov-jerusal.livejournal.com]

Да, есть ошибка, то что я написал не следует из определений.

[oblomov-jerusal.livejournal.com]

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

[avva.livejournal.com]

Этого знать не могу, статью Форда ещё не читал внимательно.

[muchandr.livejournal.com]

На самом деле мне всегда была подозрительна следующая Пеановская аксиома:

zero is not the successor of a number

Что если отрицательные числа тоже натуральны? Ну в смысле у натуральных чисел есть какой-то meaningful wraparound, может быть и множество? Как косвенный evidence у меня вызывает подозрение, что существует и так ловко работает two's compliment, причем аналогичный хаки существуют и в других базах. Может, в этом и есть множество Канторовских бесконечностей?

(off-topic) lj-cut

[bougakov.livejournal.com]

"помещаю внизу под lj-cut'ом"

Avva, можно к вам, как к автору rss и atom-экспорта из ЖЖ небольшую просьбу?

Дело в том, что в ЖЖ'шных rss-feeds lj-cut игнорируется и читать дневники через rss-reader неудобно - особенно тогда, когда под кат кладут большие картинки или большие тексты (как в этой вашей записи). Можно ли сделать так, чтобы и в rss на месте lj-cut была стандартная ссылка "read more" на продолжение записи?

Спасибо (и ещё раз извинения за off-topic).

[ignat.livejournal.com]

Странно. Только сейчас пришло его, Холмса, сообщение в рассылке FOM. Он что, проигнорировал Вас, или просто рассылка запаздывает?

[avva.livejournal.com]

Если то, в котором он рассказывает о своём доказательстве и даёт ссылку, то оно до Вас долго шло почему-то, ко мне оно вчера пришло, или сегодня утром, не помню.

[ex-ilyavinar899.livejournal.com]

У меня почему-то foundations ассоциируются с небезызвестным Александром Абианом.

Это, видимо, солнечная активность

[justpasha.livejournal.com]

А вот еще для коллекции: http://front.math.ucdavis.edu/math.GM/0405053 .Там, впрочем, опровергать нечего.