ZFC и категорная теория множеств противоречивы.

[Котофеич]

маткиб писал(а):

В Вашем тексте очень тяжело разбираться и искать определения. Среди большого количества демагогии и доказательства стандартных вещей (типа теорем Геделя) трудно найти то, что нужно.
Что означают обозначения T[PA], Def[\overline{ZFC}],
\in_{\vdash}?
Аккуратнее писать надо.

Да написано без особой заботы о читателях, но я предупредил, что это только часть.
T[PA]-множество всех предложений арифметики Пеано истинных в стандартной
модели.
Def[\overline{ZFC}]-тоже самое, что и D[\overline{ZFC}]-
множество всех множеств, определимых в метатеории множеств
\overline{ZFC}.
X\in_{\vdash}Y- сокращение для следующего высказывания
в ZFC выводимо, что $X \in Y\
Доказательства теорем Геделя приводятся по той причине, что они будут нужны в дальнейшем изложении и именно в той форме которая приведена. Существуют и другие
доказательства. Что там является демагогией я не понял . Существование т.н. противоречивых множеств это общепризнанный факт, а теория противоречивых множеств
и противоречивая логика это точные науки по которым имеются даже учебники.

[Котофеич]

zkutch писал(а):

Уважаемый Феликс Шмидель
в моменте о формализации у мне кажется у нас с вами некоторое недопонимание, которое, наверное, моя вина. Я подразумеваю возможную ошибку при подготовке материала для обработки, а не синтаксическую ошибку, которую должна замечать машина. Исключать такую возможность это удел человека.

Теперь представим, что машина нашла ошибку - что мы не проверив, так и отбросим доказательство? Или поручимся эксперту? Это опять человеческая работа.

А если машина не нашла ошибку? Верить машине или опять приглашать эксперта и верить человеку?

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

Касательно же последнего вашего вопроса, то думаю тут надо дождаться ответа от Котофеич-а.

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

[Феликс Шмидель]

Уважаемый zkutch,
если машина нашла ошибку, то скорее всего доказательство ошибочно, и никому, кроме автора доказательства и компании, ответственной за проверяющую программу, не стоит им заниматься. Если автор доказательства уверен, что проблема в проверяющей программе, он может разбить своё доказательство на части и проверить на компьютере каждую часть в отдельности. Таким образом можно выяснить, где именно проверяющая программа неправильно работает.

Уважаемый Котофеич,
Я не понимаю, почему противоречивое предложение строится только на уровне метатеории? Почему нельзя привести противоречивое предложение а самой ZF? Ведь если ZF противоречива, то такое предложение существует.

[Феликс Шмидель]

На сайте http://www.cs.ru.nl/~freek/mizar/ есть пример доказательства на языке "Мицар".

[er]

Сомнения и вопросы маткиба мне понятны..
Может для мат.логика, который знает все определения, обозначения и вообще в курсе,
все и очевидно, для меня нет.

Что такое ZFC-множество, я не понял. В INCZFC.PDF что то невразумительное написано, на что маткиб и указал. С формальной точки зрения.
Если пытатся как то разумно трактовать, что там написано, то тоже ничего хорошего не получается.
Если в качестве $\Phi$ взять всегда истинное высказывание например, "$A$ либо пусто либо не пусто", то получается, что любое множество ZFC-множество.

Котофеич писал(а):

Под ZFC-множеством обычно подразумевают множество существование которого доказуемо в ZFC в предположении ее непротиворечивости.

Что это означает эта фраза? Пример, что ли, какой то..
Пример ZFC-множества и пример не ZFC-множества.

Не знаю, в тему или нет.. У нас говорят, ZFC-пример для высказывания $\Phi$. Если понятно о каком $\Phi$ идет речь, то "для высказывания $\Phi$" опускают. Но $\Phi$ подразумевается.
Есть работы, в которых строят объекты(=множества), которые в разных расширениях ZFC (к ZFC добавляется некоторая аксиома) имеет разные свойства.
Есть высказывания $\Phi$, для которых $\exists X\Phi(X)$ верно в ZFC, но доказывается порой странно. Для некоторой добавочной аксиомы $A$ доказывается $\exists X\Phi(X)$ в $ZFC+A$ и доказывается $\exists X\Phi(X)$ в $ZFC+\rceil A$. То есть, как бы, явного ZFC сконстрированного примера и нету..

Котофеич писал(а):

Доказательство. (а) Включение $R^{\#} \in Def[\overline{ZFC}]$, есть очевидное следствие
соответствующих определений.

Гм, для логиков это может и очевидно.. Мне кажется, тут в явном виде ошибка, типа "парадокса лжеца", семантическая, то есть.

Насколько понимаю, должна существовать формула $\Phi(X)$ (не содержащая в своем определении $Def[\overline{ZFC}]$), которая определяет $R^{\#}$. И что эта за формула?

[Котофеич]

Ну я кажется понял Ваш вопрос. Он сводится к тому что Вы хотите иметь точное определение
доказуемости в ZFC :?: Потом если подставить "$A$ либо пусто либо не пусто", то не получается, что любое множество ZFC-множество. А получается только
что, что любое ZFC-множество "$A$ либо пусто либо не пусто"
Что такое доказуемость в строгом смысле, так это описывается в курсе мат логики. Но
можно упростить, чтобы Вам не нужно было тратить время на изучение лишнего.
Под ZFC-множеством Вы можете понимать любой элемент стандартной модели или любой
другой удобной для Вас модели теории ZFC.
Потом я не понял про лжеца. Тут нету никакой аналогии с лжецом. Явная аналогия
с парадоксом Рассела. Потом почему Вы думаете что в парадоксе лжеца есть ошибка
Это самое настоящее противоречие, но это не в тему. Формула
$\Phi(X)$ не содержащая в своем определении $Def[\overline{ZFC}]$), действительно существует, она не приведена потому что текст пока не полный.
Но чтобы понять как эта формула строится Вам необходимо сначала разобраться с ее
метаверсией, которая намного проще.

[er]

Котофеич писал(а):

Ну я кажется понял Ваш вопрос. Он сводится к тому что Вы хотите иметь точное определение
доказуемости в ZFC :?:

Нет, это ни при чем.

Котофеич писал(а):

Потом если подставить "$A$ либо пусто либо не пусто", то не получается, что любое множество ZFC-множество. А получается только
что, что любое ZFC-множество "$A$ либо пусто либо не пусто"

Вопрос в том, что такое ZFC-множество. Я действительно этого не понимаю. В тексте у Вас чепуха вместо определений. Есть учебники, где это понятие определяется?

Котофеич писал(а):

Что такое доказуемость в строгом смысле, так это описывается в курсе мат логики. Но
можно упростить, чтобы Вам не нужно было тратить время на изучение лишнего.
Под ZFC-множеством Вы можете понимать любой элемент стандартной модели или любой
другой удобной для Вас модели теории ZFC.
Потом я не понял про лжеца. Тут нету никакой аналогии с лжецом. Явная аналогия
с парадоксом Рассела.

Для меня это парадоксы одного типа.. В двух словах не объясню.

Парадокс с лжецом не в определении $R^{\#}$, а в Вашем "очевидно".

Котофеич писал(а):

Потом почему Вы думаете что в парадоксе лжеца есть ошибка

Не я один.

Котофеич писал(а):

Это самое настоящее противоречие, но это не в тему.

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

Котофеич писал(а):

Формула $\Phi(X)$ не содержащая в своем определении $Def[\overline{ZFC}]$), действительно существует, она не приведена потому что текст пока не полный.

Насколько понял, текст противоречивости $\overline{ZFC}$ достаточно полный. А это относится именно к доказательству противоречивости $\overline{ZFC}$, а не ${ZFC}$.

Котофеич писал(а):

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

А я с метаверсией и разбираюсь. Насчет противоречивости ZFC у Вас ничего не написано. Эта формула нужна для доказательства противоречивости $\overline{ZFC}$, а не ${ZFC}$.

У меня впечетление, что Вы между делом путаете $\overline{ZFC}$ и ${ZFC}$, отсюда извлекая произвольные противоречия.

Да ну ладно.. Если не разберусь, буду ждать результатов голосования логиков-авторитетов.

[Руст]

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

[er]

Руст писал(а):

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

И тут

Котофеич писал(а):

Доказательство. (а) Включение $R^{\#} \in Def[\overline{ZFC}]$, есть очевидное следствие соответствующих определений.

это "очевидно" из той же области.

Ну, не понимаю, почему очевидно..

Впечетление, из тех же соображений можно сказать, что "очевидно" $Def[\overline{ZFC}] \in Def[\overline{ZFC}]$. И моментально получить противоречие с аксиомой фундирования. Вот, укоротил доказательство Котофеича до одной строчки.

[Котофеич]

er писал(а):

Руст писал(а):

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

И тут

Котофеич писал(а):

Доказательство. (а) Включение $R^{\#} \in Def[\overline{ZFC}]$, есть очевидное следствие соответствующих определений.

это "очевидно" из той же области.

Ну, не понимаю, почему очевидно..

Впечетление, из тех же соображений можно сказать, что "очевидно" $Def[\overline{ZFC}] \in Def[\overline{ZFC}]$. И моментально получить противоречие с аксиомой фундирования. Вот, укоротил доказательство Котофеича до одной строчки.

Включение $R^{\#} \in Def[\overline{ZFC}]$, действительно есть очевидное следствие соответствующих определений. Объясняю почему.
Множество $R^{\#} определено с помощью формулы, соответствующего
языка и очевино есть элемент множества $ Def[\overline{ZFC}]$,
которое по своему же определению включает усе множества определимые с помощью
этого же самого языка т.е. языка метатеории множеств $ \overline{ZFC}
Что касается Вашего доказательства, то в нем элементарная ошибка. Множество
Def[\overline{ZFC}]$ требует для своего формального определения специального языка-языка второго порядка. Вы доказали только то что давно и хорошо известно-в теориях с языком второго порядка аксиома фундирования ложна.

[Котофеич]

Руст писал(а):

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

То о чем Вы говорите не в эту тему. Такие противоречивые числа действительно
теперь рассматриваются логиками как реальные объекты, но они не имеют отношения
к ZFC. Их нельзя формально определить в ZFC, для этого нужен более сильный формальный
язык. Так что такие конструкции ничего не доказывают для ZFC.

[Котофеич]

er писал(а):

Котофеич писал(а):

Ну я кажется понял Ваш вопрос. Он сводится к тому что Вы хотите иметь точное определение
доказуемости в ZFC :?:

Нет, это ни при чем.

Котофеич писал(а):

Потом если подставить "$A$ либо пусто либо не пусто", то не получается, что любое множество ZFC-множество. А получается только
что, что любое ZFC-множество "$A$ либо пусто либо не пусто"

Вопрос в том, что такое ZFC-множество. Я действительно этого не понимаю. В тексте у Вас чепуха вместо определений. Есть учебники, где это понятие определяется?

Котофеич писал(а):

Что такое доказуемость в строгом смысле, так это описывается в курсе мат логики. Но
можно упростить, чтобы Вам не нужно было тратить время на изучение лишнего.
Под ZFC-множеством Вы можете понимать любой элемент стандартной модели или любой
другой удобной для Вас модели теории ZFC.
Потом я не понял про лжеца. Тут нету никакой аналогии с лжецом. Явная аналогия
с парадоксом Рассела.

Для меня это парадоксы одного типа.. В двух словах не объясню.

Парадокс с лжецом не в определении $R^{\#}$, а в Вашем "очевидно".

Котофеич писал(а):

Потом почему Вы думаете что в парадоксе лжеца есть ошибка

Не я один.

Котофеич писал(а):

Это самое настоящее противоречие, но это не в тему.

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

Котофеич писал(а):

Формула $\Phi(X)$ не содержащая в своем определении $Def[\overline{ZFC}]$), действительно существует, она не приведена потому что текст пока не полный.

Насколько понял, текст противоречивости $\overline{ZFC}$ достаточно полный. А это относится именно к доказательству противоречивости $\overline{ZFC}$, а не ${ZFC}$.

Котофеич писал(а):

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

А я с метаверсией и разбираюсь. Насчет противоречивости ZFC у Вас ничего не написано. Эта формула нужна для доказательства противоречивости $\overline{ZFC}$, а не ${ZFC}$.

У меня впечетление, что Вы между делом путаете $\overline{ZFC}$ и ${ZFC}$, отсюда извлекая произвольные противоречия.

Да ну ладно.. Если не разберусь, буду ждать результатов голосования логиков-авторитетов.

Ну во первых рано или поздно разберетесь. Ваши замечания помогают "скорректировать" доказательство таким образом чтобы оно было доступно
нелогику или хотябы очень плохому логику.
Во вторых я ничего не путаю. Так многие думали, которые не знают чем они отличаются.
Я уже говорил, что противоречивость только одной $\overline{ZFC}$ разрушает всю теорию моделей и соответственно все что на ней Теорема Геделя о полноте это метатеорема и ее доказательство использует именно $\overline{ZFC}$ Многие математики не зная деталей доказательства, наивно думают, что это ZFC-теорема. Но конструкция модели использует аксиомы существования множеств,
которые можно определить только через отношение ZFC-выводимости. Но в ZFC такие
множества просто не обязаны существовать.
Погружаемость противоречия в ZFC я доказывал для получения более важных результатов и доказательство будет приведено также. Синтаксического доказательства теоремы о полноте за 50 лет не нашли хотя ищут его и сегодня.

[er]

Котофеич писал(а):

Включение $R^{\#} \in Def[\overline{ZFC}]$, действительно есть очевидное следствие соответствующих определений. Объясняю почему.
Множество $R^{\#} определено с помощью формулы, соответствующего
языка и очевино есть элемент множества $ Def[\overline{ZFC}]$,
которое по своему же определению включает усе множества определимые с помощью
этого же самого языка т.е. языка метатеории множеств $ \overline{ZFC}

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

Да и вообще, кажется, подправить слегка определение Вашего $\mathfrak{R}^{\#}$, получится все $Def[\ovrline{ZFC}]$.

Котофеич писал(а):

Что касается Вашего доказательства, то в нем элементарная ошибка. Множество
Def[\overline{ZFC}]$ требует для своего формального определения специального языка-языка второго порядка. Вы доказали только то что давно и хорошо известно-в теориях с языком второго порядка аксиома фундирования ложна.

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

Не только, конечно. Между определениями Def[\overline{ZFC}]$ и $\mathfrak{R}^{\#}$ особой разницы не понимаю.

[Руст]

Извините, что опять вмешиваюсь. То, что я привёл, это тоже парадокс лжеца, но в болеее завуалированной форме, определение того, что отвергается. Если язык достаточно богат, он позволяет определить то, что не определимо этим формальным языком, что приводит к противоречию. По сути, теорема Гёделя примерно тоже находит истинное не доказуемое предложение.

[Котофеич]

er писал(а):

Котофеич писал(а):

Включение $R^{\#} \in Def[\overline{ZFC}]$, действительно есть очевидное следствие соответствующих определений. Объясняю почему.
Множество $R^{\#} определено с помощью формулы, соответствующего
языка и очевино есть элемент множества $ Def[\overline{ZFC}]$,
которое по своему же определению включает усе множества определимые с помощью
этого же самого языка т.е. языка метатеории множеств $ \overline{ZFC}

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

Да и вообще, кажется, подправить слегка определение Вашего $\mathfrak{R}^{\#}$, получится все $Def[\ovrline{ZFC}]$.

Котофеич писал(а):

Что касается Вашего доказательства, то в нем элементарная ошибка. Множество
Def[\overline{ZFC}]$ требует для своего формального определения специального языка-языка второго порядка. Вы доказали только то что давно и хорошо известно-в теориях с языком второго порядка аксиома фундирования ложна.

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

Не только, конечно. Между определениями Def[\overline{ZFC}]$ и $\mathfrak{R}^{\#}$ особой разницы не понимаю.

Я разъясню эту разницу детально в более полной версии, которая скоро будет готова.
Здесь отмечу только кратко из учебника. В обычной математике используется только т.н. язык первого порядка. В языке первого порядка квантор существования и квантор общности категорически запрещено навешивать на переменные которые являются
формулами самого этого языка В языке второго порядка это разрешается. Если Вы
запишите определение множества Def[\overline{ZFC}]$ полностью, то
оно такое -произвольное x есть элемент множества Def[\overline{ZFC}]$
тогда и только тогда когда существует формула Ф(z) языка теории
\overline{ZFC}$ определяющая это x Здесь квантор существования
навешивается на переменную Ф(z) которая является формулой
Множество $\mathfrak{R}^{\#}$ определяется явным образом с указанием конкретной формулы исходного языка теории \overline{ZFC}$. Здесь
очевидно кванторы навешиваются только на обычные переменные, которые обозначают
множества. Для математика нелогика эта разница конечно трудноуловима.
Но как Вы сами показали использование языка второго порядка несовместимо с аксиомой
фундирования, т.е. различия носят на самом деле очень существенный характер.
А форсинги Вас смущали именно по той причине что это теоретикомодельные
конструкции, а эти конструкции как я уже говорил лежат именно в \overline{ZFC}$
Кстати что касается форсингов, то о них можете забыть навсегда. Все это разрушается
вместе с теоремой о полноте и без погружения метапротиворечия внутрь ZFC Для Вас это наверное уже почти очевидно