Еще раз об аксиоме выбора

[Mikhail_K]

EminentVictorians в сообщении #1614013 писал(а):

Вот есть универсум, в котором есть недостижимый кардинал. "Он там есть" = "он существует". А как мы поняли, что он существует в этом универсуме?

А мы и не поняли, что он существует. Но и опровергнуть тоже не смогли. Может, есть, может, нет.

Аксиомы теории множеств позволяют получать новые множества из старых. Но теория множеств не утверждает, что существуют только те множества, которые можно получить с помощью аксиом. Может, существуют какие-то ещё, просто мы о них не знаем.

И если Вы стоите на позициях платонизма, это должно быть Вам очень понятно. Давайте вместо множеств рассмотрим числа. "Построить", задать формулами и конечными описаниями можно лишь счётное множество вещественных чисел, но всего их континуум. Значит, есть много чисел, которые мы никак не можем построить. Точно так же, наверняка, есть много множеств, которые мы никак не можем построить исходя из аксиом. Может быть, среди них есть недостижимые кардиналы, а может, нет.

[epros]

mihaild в сообщении #1613978 писал(а):

Но тогда возникает вопрос - что вообще такое конструктивное множество двоичных последовательностей?

Очевидно, выход только один: Определить некий алгоритм, который принимает на вход код другого алгоритма и, проанализировав его, отвечает "да", если анализируемый алгоритм генерирует двоичную последовательность из заданного множества. Разумеется, невозможно гарантировать, что он ответит "да" для всех принадлежащих данному множеству двоичных последовательностей. Т.е. отсутствие ответа не означает "нет". И очевидно, что существуют разные алгоритмы для заданного множества двоичных последовательностей, некоторые из которых могут ответить "да" тогда, когда некоторые другие не дают ответа.

mihaild в сообщении #1613978 писал(а):

Конструктивисты не признают promise проблемы?

Не готов ответить.

mihaild в сообщении #1613978 писал(а):

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

Да, из двух тотальных алгоритмов можно собрать тотальный алгоритм, вычисляющий двоичную последовательность. Но вопрос тотальности непростой. Иногда бывает трудно доказать или опровергнуть наличие значения для некоторых аргументов. Поэтому мы вправе предложить некий алгоритм и сказать, что если он на данном аргументе останавливается, то выход - единица, иначе - выход нуль. С точки зрения классической логики это однозначно определённая функция (стратегия). Но чтобы стратегия второго игрока могла использовать её выход в качестве аргумента, она должна решить проблему останова в общем случае.

[EminentVictorians]

Mikhail_K в сообщении #1614020 писал(а):

"Построить", задать формулами и конечными описаниями можно лишь счётное множество вещественных чисел, но всего их континуум.

Но ведь "можно дотянуться формулой" $\ne$ "можно получить из аксиом". В моем универсуме есть все действительные числа. Я это знаю и могу доказать. Но "дотянуться формулами" я могу только до счетного их количества. Но ведь нету противоречия.

С множествами то же самое. В моем универсуме есть множество наследственно конечных множеств. А значит, все его элементы (пока все еще за рамки счетности не вышли). Но так же и все его подмножества. А это уже несчетное число множеств. Точно так же "дотянуться формулами" я до всех множеств не смогу, но я "построил" $=$ "получил из аксиом" несчетное число множеств.

[epros]

Mikhail_K в сообщении #1614020 писал(а):

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

Поскольку все множества - продукт нашего воображения, в связи с вопросом о существовании недостижимых кардиналов возникает вопрос: Можем ли мы вообразить то, чего не можем вообразить?

-- Пт окт 20, 2023 12:09:04 --

EminentVictorians в сообщении #1614042 писал(а):

Но ведь "можно дотянуться формулой" $\ne$ "можно получить из аксиом".

EminentVictorians в сообщении #1614042 писал(а):

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

Вот есть теорема Лёвенхейма-Сколема, из которой следует, что теория действительных чисел первого порядка имеет счётную модель. При этом в самой этой теории есть доказательство несчётности действительных чисел (отсутствия биекции с множеством натуральных чисел). А моделирующая теория говорит, что биекция есть. Как же так? Оказывается, биекция, которая есть, не может быть построена средствами моделируемой теории.

Так может быть всё дело не в том, что действительных чисел "больше счётного количества", а в том, что в наш ограниченный универсум не попала биекция между ними и натуральными числами?

[mihaild]

EminentVictorians в сообщении #1614042 писал(а):

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

А может быть их счетно, а дотянуться Вы не можете до биекции?
Учтите, что есть модель ZFC, в которой каждое множество задается какой-то формулой.

-- 20.10.2023, 11:01 --

epros в сообщении #1614039 писал(а):

Определить некий алгоритм, который принимает на вход код другого алгоритма и, проанализировав его, отвечает "да", если анализируемый алгоритм генерирует двоичную последовательность из заданного множества

Это же просто алгоритм, который выдает алгоритмы, выдающие последовательности из нашего множества, такой что для каждой последовательности он выдаст хотя бы один алгоритм для этой последовательности?

[epros]

mihaild в сообщении #1614048 писал(а):

Это же просто алгоритм, который выдает алгоритмы, выдающие последовательности из нашего множества, такой что для каждой последовательности он выдаст хотя бы один алгоритм для этой последовательности?

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

[EminentVictorians]

epros в сообщении #1614044 писал(а):

EminentVictorians в сообщении #1614042 писал(а):

Но ведь "можно дотянуться формулой" $\ne$ "можно получить из аксиом".

Хорошо, объясню другими словами. Есть носитель множества действительных чисел (для краткости, если это не вызывает недопонимания, можно называть его "множеством действительных чисел"). Это вполне конкретное множество, которое есть в моем универсуме (как его строить, я рассказывал в той теме на 20 страниц про комплексные числа). Оно несчетное. Теперь я хочу повыделять из него вполне конкретные действительные числа. Например, $\sqrt{2}$ я могу выделить такой формулой: $(\exists ! x) ((x^2 = 2) \wedge (x > 0)) $. Кстати говоря, Вам может показаться, что я выделяю действительные числа формулами формальной теории действительных чисел. Но это не так. Как я уже неоднократно говорил, я разделяю "действительные числа" и "формальную теорию действительных чисел" (как минимум потому что "действительные числа" - это конкретное множество из моего универсума, а "формальная теория действительных чисел" - это большая вещь, в которой в нагрузку идут формальный язык, формальная грамматика, исчисление предикатов первого порядка и все в таком духе).

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

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

Но на самом деле, это все не так уж и важно. То, что непосредственным образом, в виде формул, мы можем выделить не более чем счетное количество действительных чисел - и так очевидно.

А вот получить из аксиом (моего универсума) мы можем несчетное количество множеств. Как получить сам носитель множества действительных чисел - я уже говорил (это не очень сложно). Далее, берем произвольное действительное число $x \in \mathbb R$. Имеем: $x \in \mathbb R$ и $\mathbb R \in U$ $\Rightarrow$ $x \in U$ (вторая аксиома). Таким образом, в моем универсуме есть каждое действительное число. Это иллюстрация, как "получить из аксиом" несчетное количество множеств.

epros в сообщении #1614044 писал(а):

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

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

[mihaild]

epros в сообщении #1614062 писал(а):

Как он их будет выдавать, по очереди? Тогда получится, что все выдаваемые им алгоритмы пронумерованы

Ну и что? Перечеслимое множество же можно пронумеровать.

epros в сообщении #1614039 писал(а):

Определить некий алгоритм, который принимает на вход код другого алгоритма и, проанализировав его, отвечает "да", если анализируемый алгоритм генерирует двоичную последовательность из заданного множества

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

EminentVictorians в сообщении #1614066 писал(а):

А то что у нее есть какие-то счетные модели, мне вообще без разницы. Я работаю внутри своей модели, другие не интересуют

А вдруг вообще весь ваш юниверсум счетный?

Но я перестал понимать, о чем разговор.
Вот Вы написали список аксиом ZFC, и попросили отвести Вас в юниверсум, где они выполнены. Без проблем, отвели. Есть ли в этом юниверсуме недостижимые кардиналы или нестандартные натуральные числа - ну как повезет, Вы же ничего про них не требовали.
А потребовать, чтобы Вас отвели в юниверсум, где нестандартных натуральных чисел нет, у Вас не получится.

[EminentVictorians]

mihaild в сообщении #1614069 писал(а):

А вдруг вообще весь ваш юниверсум счетный?

А давайте проверим.

1)Обозначим множество наследственно конечных множеств буквой $\Sigma$. Тогда $\Sigma \in U$ (по аксиоме множества наследственно конечных множеств).
2) $\Sigma \in U \Rightarrow 2^\Sigma \in U$ (аксиома булеана)
3) Положим $\mathbb N_0$ - носитель множества натуральных чисел. $\mathbb N_0 \subset \Sigma \Rightarrow \mathbb N_0 \in 2^\Sigma \in U \Rightarrow \mathbb N_0 \in U$ (использовалась вторая аксиома).
4) Легко доказать, что операции сложения и умножения (имеющие вид $\mathbb N_0 \times \mathbb N_0 \to \mathbb N_0$), так же принадлежат универсуму. Если хочется считать ноль и единицу операциями (нульарными), тоже легко показать, что они (как функции вида $\circ \to \mathbb N_0$ (где кружочек - это какое-нибудь одноточечное множество универсума) тоже принадлежат универсуму.
5) Таким образом, вся структура $\mathbb N = (\mathbb N_0, + , \cdot, 0, 1)$ принадлежит универсуму.
6) Множество $\{0 , 1\}$ принадлежит универсуму.
7) Множество всех битовых последовательностей (т.е. функций вида $\mathbb N \to \{0 , 1\}$) тоже принадлежит универсуму.
8) Докажем, что множество из пункта 7 несчетно. (стандартный диагональный процесс).

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

Как он может быть счетным?

[epros]

EminentVictorians в сообщении #1614066 писал(а):

А вот получить из аксиом (моего универсума) мы можем несчетное количество множеств.

Собственно, я поставил вопрос именно потому, что по моим понятиям "из аксиом" можно получить ровно то же самое, что "из формул". Ибо аксиомы - и есть формулы. Это верно даже в том случае, если аксиом бесконечно много (схемы аксиом). Так что никакого несчётного количества чего бы то ни было из аксиом Вы не "получите". А вот вывод о том, что что-то там существует в несчётном количестве, вполне получить можете, хоть из аксиом, хоть из формул.

EminentVictorians в сообщении #1614066 писал(а):

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

Интересно, в каком смысле Вы можете "построить" множество действительных чисел? Я знаю два смысла этого слова: практический (в котором строители строят дом) и теоретический, когда нечто строится в воображении. Множество действительных чисел, очевидно, в практическом смысле построить никак невозможно. А построение в теоретическом смысле это и есть построение теории. Кстати, теоремы, о которых Вы говорите, это и есть элементы теории. Даже если речь о неформальной теории, это всё равно теория. Кантор в рамках своего "учения о множествах", когда рассуждал о различных кардинальностях, на самом деле строил неформальную теорию.

Так что то, что Ваша неформальная теория не допускает существования биекции между действительными и натуральными числами - это проблема Вашей неформальной теории.

-- Пт окт 20, 2023 15:48:42 --

mihaild в сообщении #1614069 писал(а):

epros в сообщении #1614062 писал(а):

Как он их будет выдавать, по очереди? Тогда получится, что все выдаваемые им алгоритмы пронумерованы

Ну и что? Перечеслимое множество же можно пронумеровать.

Так получается, что мы на уровне определения требуем, чтобы любое конструктивное множество двоичных последовательностей было перечислимым. А это идеологически неправильно.

mihaild в сообщении #1614069 писал(а):

epros в сообщении #1614039 писал(а):

Определить некий алгоритм, который принимает на вход код другого алгоритма и, проанализировав его, отвечает "да", если анализируемый алгоритм генерирует двоичную последовательность из заданного множества

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

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

[mihaild]

EminentVictorians в сообщении #1614071 писал(а):

Таким образом, наш универсум уже содержит несчетное число элементов

Нет, наш юниверсум не содержит биекции между какими-то двумя своими объектами. Это дотационный юниверсум, туда не все биекции подвезли. А вот у меня такая биекция есть (но я Вам её не покажу, Вы же вещественные числа не показываете).

epros в сообщении #1614073 писал(а):

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

ЯННП. Если у нас есть алгоритм, то множество входов, на которых он говорит "да", перечеслимо. Это практически определение перечислимости.

[EminentVictorians]

mihaild в сообщении #1614078 писал(а):

Нет, наш юниверсум не содержит биекции между какими-то двумя своими объектами.

Я не понимаю, какую биекцию и какие объекты Вы имеете в виду.

Вы сказали: "а вдруг универсум счетный?"
Я доказал, что любая двоичная последовательность является элементом моего универсума.
Все двоичные последовательности уже образуют несчетное множество. А кроме них в моем универсуме есть еще элементы.

Как универсум может быть счетным?

[mihaild]

EminentVictorians в сообщении #1614080 писал(а):

Я доказал, что любая двоичная последовательность является элементом моего универсума

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

[EminentVictorians]

mihaild в сообщении #1614082 писал(а):

Нет, Вы доказали, что Вашему юниверсуму принадлежат те двоичные последовательности, которые ему принадлежат.

Я взял произвольную двоичную последовательность. Оказалось, что она является элементом моего универсума. Далее я делаю вывод, что все двоичные последовательности принадлежат моему универсуму. Неужели я не имею право так делать?

[mihaild]

EminentVictorians в сообщении #1614093 писал(а):

Я взял произвольную двоичную последовательность. Оказалось, что она является элементом моего универсума

Где Вы её взяли?