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

[маткиб]

2 Котофеич:

Текст крайне непонятный, но в некоторых местах еще можно читать, а в некоторых вообще непонятно. Что такое ZFC-множество?
У Вас написано что-то вроде

Цитата:

A есть ZFC-множество, если существует формула \Phi(X) с единственной свободной переменной X такая, что выполнено следующее условие:
\overline{ZFC}\vdash\exists A\Phi(A)

Причем здесь вообще A? У Вас A в формуле не является свободной переменной, поэтому эта формула не может быть определением того, что A "чем-то там является"! И что Вы вообще под множеством подразумеваете? Ваше определение скорее говорит о том, когда \Phi является ZFC-формулой.

Непонятно, что такое метатеория ZFC. У Вас написано, что это

Цитата:

формальная теория, которая получается в результате расширения теории ZFC путем добавления одного унарного отношения
\vdash_{ZFC} A.

Из этого я ни одного слова не понял. Что это значит? Что такое A? получается, что для разных A получаются разные метатеории что ли?

[маткиб]

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

[Котофеич]

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

2 Котофеич:

Текст крайне непонятный, но в некоторых местах еще можно читать, а в некоторых вообще непонятно. Что такое ZFC-множество?
У Вас написано что-то вроде

Цитата:

A есть ZFC-множество, если существует формула \Phi(X) с единственной свободной переменной X такая, что выполнено следующее условие:
\overline{ZFC}\vdash\exists A\Phi(A)

Причем здесь вообще A? У Вас A в формуле не является свободной переменной, поэтому эта формула не может быть определением того, что A "чем-то там является"! И что Вы вообще под множеством подразумеваете? Ваше определение скорее говорит о том, когда \Phi является ZFC-формулой.

Непонятно, что такое метатеория ZFC. У Вас написано, что это

Цитата:

формальная теория, которая получается в результате расширения теории ZFC путем добавления одного унарного отношения
\vdash_{ZFC} A.

Из этого я ни одного слова не понял. Что это значит? Что такое A? получается, что для разных A получаются разные метатеории что ли?

1.Там просто лишнее переобозначение X и А это одно и тоже. Нужно читать так
\overline{ZFC}\vdash\exists X\Phi(X)
Под ZFC-множеством обычно подразумевают множество существование которого
доказуемо в ZFC в предположении ее непротиворечивости.
2. Там сокращение в определении метатеории. Полностью нужно читать так:
\overline{ZFC}\ это формальная теория, которая получается в результате расширения алфавита теории ZFC путем добавления одного символа унарного отношения \vdash_{ZFC} X.

[маткиб]

Не понятно, как формула
\overline{ZFC}\vdash\exists X\Phi(X)
может выражать свойство X или A. Она выражает свойство \Phi, потому что у нее нет свободных переменных.

Цитата:

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

Это нужно определить более формально. Что значит доказать что-то для множества? Доказать можно что-либо для _определения_множества_ (формулы). Снова повторяю вопрос: что Вы подразумеваете под множеством? Элемент стандартной модели ZFC?
P.S. Я не придираюсь, мне реально абсолютно ничего не понятно (книжки по логике я читал).

[маткиб]

Про метатеорию кажись понял. Просто появилась новая логическая связка \vdash_{ZFC}.
Только что можно делать с этой связкой? Какие-то аксиомы должны быть или правила вывода...

[Котофеич]

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

Не понятно, как формула
\overline{ZFC}\vdash\exists X\Phi(X)
может выражать свойство X или A. Она выражает свойство \Phi, потому что у нее нет свободных переменных.

Цитата:

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

Это нужно определить более формально. Что значит доказать что-то для множества? Доказать можно что-либо для _определения_множества_ (формулы). Сново повторяю вопрос: что Вы подразумеваете под множеством? Элемент стандартной модели ZFC?
P.S. Я не придираюсь, мне реально абсолютно ничего не понятно (книжки по логике я читал).

Формула \overline{ZFC}\vdash\exists X\Phi(X)
говорит о том что в \overline{ZFC}\ доказуемо утверждение \exists X\Phi(X)

[маткиб]

А какое это имеет отношение к фразе
"X является ZFC-множеством"?
Ваша формула говорит о некотором свойстве формулы \Phi, но никак не о свойстве X (X является связанной переменной, ее название не имеет никакого значения, можно хоть "Ъ" ее назвать, она никак не связана с тем X, который в фразе "X является ZFC-множеством").

[Котофеич]

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

А какое это имеет отношение к фразе
"X является ZFC-множеством"?
Ваша формула говорит о некотором свойстве формулы \Phi, но никак не о свойстве X (X является связанной переменной, ее название не имеет никакого значения, можно хоть "Ъ" ее назвать, она никак не связана с тем X, который в фразе "X является ZFC-множеством").

Не понял. Например формула $n \in \mathbb{X}$
выражает то свойство множества X, что n есть его элемент.
Множество $\mathbb{N}$ дает Вам канонический пример ZFC-множества.

[маткиб]

формула
\exists X(n\in X)
выражает то, что существует множество X, в котором есть n. Это свойство n, но никак не X.

Про множество \mathds{N}. Ну докажите что-нибудь для этого множества в ZFC, например, что оно не пустое. Выглядеть это будет так: будет взято некоторое определение \mathds{N}, выражаемое некоторой формулой \Phi(X) и для него будет доказано, что если \Phi(X), то X не пустое. Если же взять другую формулу \Psi, тоже "определяющую" множество \mathds{N}, то будет уже другое доказательство (или вообще не будет). Но какое отношение имеет например формула \Phi к множеству \mathds{N}? Да никакого, это просто его определение. Поэтому свойство будет доказано все-таки для формулы-определения \Phi, а не для \mathds{N}.

P.S. Мне кажется, что у Вас все-таки есть ошибка в доказательстве, но из-за мелких неточностей, неформальных рассуждений и т.п. найти её будет очень трудно. Нужно более формально рассуждать (и пользоваться общепринятыми обозначениями).

[Котофеич]

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

Про метатеорию кажись понял. Просто появилась новая логическая связка \vdash_{ZFC}.
Только что можно делать с этой связкой? Какие-то аксиомы должны быть или правила вывода...

Да совершенно верно. Вы правильно поняли-должны быть аксиомы. Они еще просто
не дописаны там. Суть их проста. В ZFC-формулах допустимы только элементарные
логические связки. Аксиомы метатеории множеств те же что и у ZFC, но теперь
класс формул более широкий. Так например аксиома выделения будет за счет этого,
более общей чем у ZFC.
Свойства этой новой связки \vdash_{ZFC} разумеется хорошо известны,
это обычное отношение выводимости классического исчисления предикатов.

[Котофеич]

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

формула
\exists X(n\in X)
выражает то, что существует множество X, в котором есть n. Это свойство n, но никак не X.

Про множество \mathds{N}. Ну докажите что-нибудь для этого множества в ZFC, например, что оно не пустое. Выглядеть это будет так: будет взято некоторое определение \mathds{N}, выражаемое некоторой формулой \Phi(X) и для него будет доказано, что если \Phi(X), то X не пустое. Если же взять другую формулу \Psi, тоже "определяющую" множество \mathds{N}, то будет уже другое доказательство (или вообще не будет). Но какое отношение имеет например формула \Phi к множеству \mathds{N}? Да никакого, это просто его определение. Поэтому свойство будет доказано все-таки для формулы-определения \Phi, а не для \mathds{N}.

P.S. Мне кажется, что у Вас все-таки есть ошибка в доказательстве, но из-за мелких неточностей, неформальных рассуждений и т.п. найти её будет очень трудно. Нужно более формально рассуждать (и пользоваться общепринятыми обозначениями).

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

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

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

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

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

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

[zkutch]

Феликс Шмидель писал(а):

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

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

И что делать с поиском ошибки в формализации? Это все равно человеческая работа, так что человеческий фактор снять не получается.

Сводить же все к проверке человеком это и есть ссылка на авторитеты. Гарантий нет и здесь - это правда.

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

Как только кто-нибудь ошибку найдет, так может полететь даже теорема Пифагора.

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

Уважаемый zkutch, если в формализации будет допущена ошибка, то проверяющая программа забракует доказательство.
Ответственность за исправление ошибки лежит на том, кто её сделал. Если же проверяющая программа не обнаружила ошибки, то тогда пусть доказательство проверяют люди. Это имеет смысл, поскольку вероятность ошибки близка к нулю.
Я не понимаю, что мешает уважаемому автору доказательства
противоречивости ZF предъявить найденное им противоречие
для компьютерной проверки, например, на языке "Мицар"?

[zkutch]

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

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

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

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

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