О непротиворечивости арифметики, теореме Гёделя, etc.

[warlock66613]

george66 в сообщении #1203043 писал(а):

их в огромном количестве производит Харви Фридман и выкладывает на FOM

А можно увидеть конкретный пример? По вашей второй ссылке что-то невнятное: письмо с двумя ссылками, первая ведёт на какое-то видео, а вторая - на какую-то жёлтую статью.

[george66]

Поищите в архивах FOM
http://www.cs.nyu.edu/pipermail/fom/
вот например (не берусь популярно объяснить, что это такое)
http://www.cs.nyu.edu/pipermail/fom/201 ... 20396.html
Суть, как я понял, такая: Фридман придумал способ "обрушивать" утверждения о больших кардиналах, получая равносильные утверждения о натуральных числах. Соответственно, теперь есть множество утверждений о натуральных числах, недоказуемых в ZF ( и неопровержимых, если непротиворечиво существование этих больших кардиналов, во что верят специалисты по теории множеств).
Единственность натурального ряда с точки зрения теории множеств надо понимать так: если есть совокупность множеств (допустим, модель ZF), в ней есть только один натуральный ряд. Но если мы добавляем новые множества (например, обнаруживаем большой кардинал), этот натуральный ряд перестаёт быть натуральным рядом, но появляется новый, более короткий. "Пересечение всех индуктивных множеств" становится меньше, когда множеств становится больше. Старый натуральный ряд оказывается гипернатуральным, в нём есть "лишние" числа, чего мы раньше не знали.

[warlock66613]

george66 в сообщении #1203108 писал(а):

Поищите в архивах FOM

Я, кажется, придумал способ получше: поискать статьи за авторством Harvey M. Friedman.

[george66]

FOM в значительной степени площадка для публикации гениальных идей Фридмана, которых он производит много каждый день. Я туда хожу, чтобы следить, кто умер из великих. Недавно умер Йонсон (в теории моделей известный) в возрасте под сто лет, перед ним Крэйг (теорема Крэйга-Линдона), только что Смальян и т.д. Модератор у них Мартин Дэвис, ему 89 лет. Но когда перед тобой общаются Дана Скотт и Саймон Кочен, это впечатляет, прикасаешься к истории. Молодёжь, группирующаяся вокруг Воеводского, зовёт FOM "хранилищем ядовитых отходов". С другой стороны, любой форум, куда приходит Воеводский, быстро погибает (все уходят за Воеводским в болото), а на FOMе жизнь кипит, старички пишут вовсю.

[warlock66613]

Ну, хотя это весьма любопытно, но исходному вопросу (почему нельзя отбросить условие о непротиворечивости арифметики Пеано в условии теоремы Гёделя) совершенно ортогонально.

-- 24.03.2017, 21:49 --

Вообще, похоже, что ответ до безумия прост: просто утверждение о непротиворечивости арифметики не является частью соответствующей теоремы Гёделя, вот и всё. Это отдельная теорема, а точнее несколько теорем: помимо прочего, можно вспомнить небезизвестную теорему Генцена (которую Вавилов в "Не совсем наивной теории множеств" рекомендует упоминать всегда, когда упоминается теорема Гёделя), и доказательство на основе арифметики второго порядка, упоминаемое тут: http://www.cs.nyu.edu/pipermail/fom/2011-May/015413.html.

[george66]

Теорема Гёделя утверждает: если арифметика непротиворечива, то есть формула, недоказуемая и неопровержимая в ней. Если арифметика вдруг противоречива, то в ней доказуемы вообще все формулы (из противоречия следует что угодно).

[Padawan]

Что там Генцен доказал, я не очень понимаю, но уж точно, не именно то, что арифметика Пеано не противоречива. Это понятно без всяких доказательств, так как она имеет модель. Скорее он доказал, что некое формальное утверждение, имеющее при его (неформальной) интерпретации содержательный смысл непротиворечивости арифметики Пеано можно доказать в некой другой формальной теории. То есть он указал на некоторую связь между двумя формальными теориями.

-- Сб мар 25, 2017 00:59:34 --

george66 в сообщении #1203043 писал(а):

Никакой физический опыт нас не убеждает в существовании числа $10^{10^{100}}$

Убеждает принцип математической индукции, который происходит как обобщение опыта. Если существует число $n$, то и существует число $10^n$. Вы это всерьез пишите или прикалываетесь?

Если так подходить, так я и число 100 не уверен, что существует. Ибо зараз в голове одновременно могу удержать предметов 6-7 в непосредственном восприятии. Но на то математика и существует, чтобы создавать такие абстракции как натуральные числа, исходя из обобщения практического опыта.

[warlock66613]

Padawan в сообщении #1203238 писал(а):

Это понятно без всяких доказательств

То, что что-то понятно, не означает, что это нельзя доказать.

Padawan в сообщении #1203238 писал(а):

некое формальное утверждение, имеющее при его (неформальной) интерпретации содержательный смысл непротиворечивости арифметики Пеано можно доказать в некой другой формальной теории. То есть он указал на некоторую связь между двумя формальными теориями.

Не вижу никакого отличия (но это не значит, что его нет) между этой длинной сентенцией и более короткой "доказал непротиворечивость арифметики Пеано". Любая теорема — это, в конечном счёте, некоторое формальное утверждение, и любое утверждение о непротиворечивости некоторой теории — это утверждение о наличии связи между этой теорией и метатеорией, в которой производится доказательство, так ведь?

-- 24.03.2017, 23:37 --

(Оффтоп)

george66, кстати, спасибо, всё-таки, за ссылку на FOM. Там действительно есть что почитать. Например, интересный вопрос, фатальна ли противоречивость для теории. Оказывается, нет, и с противоречивыми теориями можно содержательно работать! (потому что противоречивость, вообще говоря, не означает, что для любой теоремы доказуемо её отрицание)

[Padawan]

warlock66613 в сообщении #1203245 писал(а):

любое утверждение о непротиворечивости некоторой теории — это утверждение о наличии связи между этой теорией и метатеорией, в которой производится доказательство, так ведь?

Так. Я тоже могу очень просто "доказать непротиворечивость арифметики Пеано". Формально. В некоторой формальной системе, которую сейчас опишу. В этой системе всего одна аксиома "A" и ни одного правила вывода. Интерпретируется эта аксиома так: арифметика Пеано не противоречива. Доказательство того, что арифметика Пеано непротиворечива: А.

Допустим, можно доказать, допустим в теории множеств, в ZFC, формальную теорему, содержательно означающую, что арифметика Пеано непротиворечива. Но это к убежденности в непротиворечивость арифметики Пеано не добавит ни капли, потому что непротиворечивость ZFC сама под вопросом. А непротиворечивость арифметики Пеано более наглядна, потому что у нее есть всем понятная модель.

[warlock66613]

Padawan в сообщении #1203295 писал(а):

А непротиворечивость арифметики Пеано более наглядна, потому что у нее есть всем понятная модель.

Стоп-стоп-стоп. Само понятие модели, и связанные с этим понятием теоремы ("если теория имеет модель, то она непротиворечива") — всё это формулируется в рамках ZFC. Если противоречива ZFC, то всё это рушится (и в частности, рушатся все или почти все теоремы Гёделя).

[george66]

Ребятки, вы не знаете техники. Теорема Гёделя не рушится, если ZF окажется противоречивой. Эта теорема утверждает "Если арифметика непротиворечива, то в ней есть формула, которую нельзя ни доказать, ни опровергнуть". Доказывается она диагональным методом. Формулы нумеруются натуральными числами, затем для каждой формулы $\varphi(n)$ удаётся построить некоторую формулу $\psi$ и доказать $\psi\Leftrightarrow\varphi(\ulcorner\psi\urcorner)$. Например, если формула $\varphi(n)$ утверждает "число n простое", то соответствующая формула $\psi$ как бы утверждает "мой номер - простое число". Затем пишется формула $\varphi(n)$, утверждающая "формула с номером n не доказуема в арифметике". Соответствующая формула $\psi$ утверждает "я не доказуема в арифметике". Если арифметика непротиворечива, то эта формула не доказуема и истинна по смыслу. Если арифметика вдруг противоречива, эта формула доказуема (в противоречивой теории всё доказуемо) и ложна по смыслу. Какое из двух верно, мы не знаем.

[warlock66613]

george66 в сообщении #1203367 писал(а):

Теорема Гёделя не рушится, если ZF окажется противоречивой.

Нет, она "всего лишь", будучи, по крайней мере в "каноническом виде", теоремой ZF (в том смысле, в каком все математические теоремы являются теоремами ZF(C), если явно не указано иного), становится теоремой противоречивой теории, т. е. в значительной мере обессмысливается.

[george66]

Теорему Гёделя можно доказать в гораздо более слабой теории, чем ZF, она не требует кардиналов, ординалов, аксиомы выбора и вообще почти ничего - диагональный метод в чистом виде. Вообще, забудьте про ZF, она сдохла давно, ей 100 лет, математическая логика за это время много чего придумала.
Вообще, по поводу доказательств непротиворечивости. Когда ввели комплексные числа, тогдашние математики возражали, что их нет в природе. Сомнения утихли, когда придумали модель (точки плоскости). Здесь непонятное и ненадёжное свели к более понятному и надёжному. Аналогично, когда добавили бесконечно удалённые точки в геометрии - тоже есть понятная и надёжная модель. Доказывать таким образом непротиворечивость арифметики или ZF не удаётся - ни к чему более простому они не сводятся. "Доказательства непротиворечивости" дают некоторые интересные технические результаты, а не доказывают непротиворечивость. Физический опыт не убеждает даже в бесконечности натурального ряда.

[warlock66613]

george66 в сообщении #1203383 писал(а):

Теорему Гёделя можно доказать в гораздо более слабой теории, чем ZF, она не требует кардиналов, ординалов, аксиомы выбора и вообще почти ничего - диагональный метод в чистом виде.

Это так, но главного это не меняет.

george66 в сообщении #1203383 писал(а):

Вообще, забудьте про ZF, она сдохла давно, ей 100 лет, математическая логика за это время много чего придумала.

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

george66 в сообщении #1203383 писал(а):

"Доказательства непротиворечивости" дают некоторые интересные технические результаты.

А что вам ещё надо? Мы вроде в математическом разделе, а математика — это как раз про "интересные технические результаты", не так ли?

-- 25.03.2017, 15:57 --

george66 в сообщении #1203383 писал(а):

Доказывать таким образом непротиворечивость арифметики или ZF не удаётся - ни к чему более простому они не сводятся.

Для того, чтобы модель была понятной и надёжной, ей вовсе не обязательно быть простой.