Конечность по Дедекинду

[Z1X]

Someone в сообщении #1218461 писал(а):

Если в качестве теории множеств взять ZF (без аксиомы выбора), то возможны странные множества, в которых можно найти сколь угодно длинную конечную последовательность попарно различных элементов, но нельзя указать бесконечную последовательность. Они конечны по Дедекинду, но бесконечны в смысле обычного определения.

Необходим пример такого множества.

Вообще неясно, при чем тут аксиома выбора: все теоремы, доказанные в ZF, автоматически выполняются в ZFC. Предположим, существует странное множество $H$, и для него справедливо $\forall x \subsetneq H \ x \not\cong H$ и $\forall n \in \mathbb{N} \ H \not\cong n$. Тогда такая странность (если она вообще возможна) будет выполнена и в ZFC и доказана тем же путем, что и в ZF.

[Someone]

Z1X в сообщении #1237568 писал(а):

Необходим пример такого множества.

У Вас противоречивые желания. Здесь Вы требуете конструктивного предъявления некоего множества, а в параллельной теме не желаете использовать конструктивное определение суммы натуральных чисел. Должен Вас разочаровать. Для того, чтобы делать вычисления (а арифметика нужна нам именно для этого), всё равно придётся сформулировать и доказать конструктивный вариант определения суммы (и произведения) натуральных чисел. Что касается дедекиндова множества, то его невозможно построить, пользуясь аксиомами ZF, так как это означало бы противоречивость не только ZFC, но и ZF, поэтому такое множество должно быть заложено в модель ZF изначально.

Z1X в сообщении #1237568 писал(а):

Вообще неясно, при чем тут аксиома выбора: все теоремы, доказанные в ZF, автоматически выполняются в ZFC. Предположим, существует странное множество $H$, и для него справедливо $\forall x \subsetneq H \ x \not\cong H$ и $\forall n \in \mathbb{N} \ H \not\cong n$. Тогда такая странность (если она вообще возможна) будет выполнена и в ZFC и доказана тем же путем, что и в ZF.

Следовательно, эта "странность" не является теоремой ZF. Ещё раз повторю: такое множество $H$ нельзя построить средствами ZF, поэтому в ZFC такого множества нет. Ибо в ZFC отсутствие дедекиндова множества доказуемо.

[Z1X]

То есть в ZFC можно доказать, что $\forall x \subsetneq H \ x \not\cong H \leftrightarrow \exists n \in \mathbb{N} \ H \cong n$ ?

[Anton_Peplov]

Z1X в сообщении #1237598 писал(а):

То есть в ZFC можно доказать, что $\forall x \subsetneq H \ x \not\cong H \leftrightarrow \forall n \in \mathbb{N} \ H \cong n$ ?

Я дико извиняюсь, Вы справа квантор не перепутали?

[Z1X]

Anton_Peplov, спасибо, исправил.

[Anton_Peplov]

Тогда - да, можно доказать. Неформальное доказательство встречается в учебниках по анализу (в Колмогорове-Фомине я его, кажется, видел) и обычно озаглавлено как "бесконечное множество равномощно своему собственному подмножеству". Как и практически любое неформальное доказательство, его можно формализовать в ZFC.

[Someone]

Anton_Peplov в сообщении #1237602 писал(а):

Я дико извиняюсь, Вы справа квантор не перепутали?

Кстати, и в первом сообщении так же, а я и не вник…

Z1X в сообщении #1237598 писал(а):

То есть в ZFC можно доказать, что $\forall x \subsetneq H \ x \not\cong H \leftrightarrow \exists n \in \mathbb{N} \ H \cong n$ ?

Да, конечно.

-- Ср авг 02, 2017 10:58:58 --

Нет, в первом сообщении так и должно быть.

[Z1X]

Но в этом доказательстве используется аксиома выбора? Поэтому у ZF существуют такие модели, где данная теорема уже не является истинной?

Вообще, сам факт использования аксиомы выбора в доказательстве еще не гарантирует независимость самого утверждения от ZF. Доказательств может быть много. Есть шанс, что какое-то одно из них строится в ZF.

[Anton_Peplov]

Z1X в сообщении #1237623 писал(а):

Но в этом доказательстве используется аксиома выбора?

Да.

Z1X в сообщении #1237623 писал(а):

Вообще, сам факт использования аксиомы выбора в доказательстве еще не гарантирует независимость самого утверждения от ZF. Доказательств может быть много. Есть шанс, что какое-то одно из них строится в ZF.

Стандартный путь - посмотреть, нельзя ли из этого утверждения вывести аксиому выбора средствами ZF.

[Someone]

Z1X в сообщении #1237623 писал(а):

Вообще, сам факт использования аксиомы выбора в доказательстве еще не гарантирует независимость самого утверждения от ZF. Доказательств может быть много. Есть шанс, что какое-то одно из них строится в ZF.

В данном случае шанса нет. Известно, что если ZF непротиворечива, то ZFC тоже непротиворечива, так как в ZF можно определить так называемый конструктивный универсум, в котором выполняется аксиома выбора (а заодно аксиома регулярности и обобщённая континуум-гипотеза). Если бы дедекиндово множество можно было построить средствами ZF, то оно существовало бы и в ZFC (введение дополнительной аксиомы не может запретить доказательства, не использующие её). Но в ZFC доказуемо, что дедекиндовых множеств нет. Это дало бы противоречие.

Или я Вас неправильно понял?

[Z1X]

Someone в сообщении #1237823 писал(а):

Или я Вас неправильно понял?

Видимо, неправильно.

Someone в сообщении #1237823 писал(а):

Но в ZFC доказуемо, что дедекиндовых множеств нет.

Чем гарантировано, что в ZF не доказуемо то же самое?

[Someone]

Z1X в сообщении #1237891 писал(а):

Чем гарантировано, что в ZF не доказуемо то же самое?

Построением модели ZF, в которой дедекиндовы множества существуют.

[Z1X]

Есть какая-то подтверждающая информация, что такая модель может существовать? Нужны ссылки. Построение такой модели может оказаться сложнейшей метатеоремой: для нее нужно доказать истинность бесконечного числа аксиом ZF + что дедекиндовы множества существуют. Коэну для доказательства независимости континуум-гипотезы и аксиомы выбора от ZF пришлось написать целую книгу. То же ожидается и здесь: большой объем текста и высокая сложность. Нужны ссылки на литературу.

[Someone]

Z1X в сообщении #1237898 писал(а):

Есть какая-то подтверждающая информация, что такая модель может существовать? Нужны ссылки.

Это где-то в работах Коэна по методу форсинга надо искать. Модель упоминается, например, в работе Херрлиха "Аксиома выбора", сразу после Proposition 4.10.
Horst Herrlich. Axiom of Choice. Вы хотите лично проверить, не врут ли математики? Как у Вас с математической логикой? А с методом форсинга (вынуждения) Вы уже разобрались?

Z1X в сообщении #1237898 писал(а):

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

Ну, можете начать разбираться с этой книги.

[Z1X]

Someone в сообщении #1237918 писал(а):

Как у Вас с математической логикой?

Я в последнее время систематически попадаюсь на парадокс Сколема в самых разных вариациях. Самый ранний случай произошел примерно здесь. А последний (на настоящий момент) — непосредственно в этой теме.

Someone в сообщении #1237892 писал(а):

Построением модели ZF, в которой дедекиндовы множества существуют.

Если я правильно понял, дедекиндовость будет внутренним свойством модели. А метатеория, используемая для построения модели, с этим может быть никак не связана. Более того, если в роли метатеории тоже используется ZF, и в ней удалось доказать про некоторые множества, что они конечны по Дедекинду и бесконечны одновременно, то ZFC будет противоречива.