И всё-таки аксиома выбора должна быть улучшена

Посовещался тут с ЫЫ о своих измышлениях на тему Аксиомы Выбора. Он растолковал мне, в чём я не прав, и помог уточнить, в чём прав.

Суть такова: функция выбора ("такая функция, которая возвращает элемент такой, что...") и операция выбора ("взять элемент такой, что...") - разные, практически независимые вещи. Функция выбора \(f(S)=s\in S\) - это просто функция с некими свойствами. Операция выбора \(\epsilon(S)\) - это именно операция, уничтожающая квантор (позволяя при наличии выражения \((\exists x: P_S(x)) = T\) или \((\forall x: P_S(x)) = T\) ввести независимую константу \(x_0\) такую, что \(P_S(x_0)\)).
Считается, что эта операция не входит в язык, используемый для формулировки ZF(C), и используется как бы на метауровне. AC, очевидно, была попыткой сократить число сущностей и ввести эту операцию в саму теорию. А по свойствам \(\epsilon(S)\) похожа на класс-функцию (отображение из класса множеств в... тоже некий класс). Причём, в ZF понятие класса формально отсутствует, поэтому ввести именно класс-функцию там непосредственно нельзя. Видимо, так и возникла стандартная формулировка про функцию для семейства множеств (свою для каждого семейства).

Но это было крайне неудачное решение.

Операция выбора, так или иначе, в большинстве доказательств всё равно используется (везде, где есть "возьмём такое x, что..." - это она и есть). Как операция уровня теории, или операция мета-уровня - но используется. Без неё нельзя доставать объекты из-под квантора, и корректная формулировка доказательства будет, в лучшем случае, представлять собой разрастающийся по вложенности квантор существования, а в худшем - будет невозможной.

Но самая главная причина, по которой заход через функцию выбора порочен - её существование или несуществование не решает того вопроса, ради которого всё мутилось: не превращает операцию выбора в объект теории.

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

Такой подход, при пристальном рассмотрении, является говном. Если мы таким образом получаем некое доказательство, которое заявляем как "в рамках ZF(C)", то на самом деле это доказательство в рамках "ZF(C) + операция выбора, (неявно) доопределённая конкретно для данного доказательства". А потом кто-нибудь пытается использовать доказательства А и доказательства Б, "полученные в ZF(C)", для получения доказательства C, и получает хрень, потому что А и Б, вообще говоря, построены каждое на своей собственной операции выбора, и никто не гарантрирует их совместимости.
Для ZFC шанс на это ниже, поскольку возможностей придумать несовместимые операции выбора там меньше, а вот в просто ZF получение хрени идёт в полный рост. На днях, вон, получили очередную изобрели очередной вид больших кардиналов, и чего-то там сломали.

Если же мы перестанем морщить репу и включим в состав операций \(\epsilon(S)\), которая напоминает применение некой класс-функции, но, тем не менее, является именно первичной операцией (свойства которой диктуются набором аксиом, которые тоже нужно добавить в аксиоматику (например, \(S_1=S_2\ \Rightarrow\ \epsilon(S_1)=\epsilon(S_2)\) )), то дело поворачивается несколько по-другому.

Вопрос уже не столько в том, существует ли функция выбора, сколько в том, как её свойства соотносятся со свойствами операции выбора. И этот вопрос оказывается, на удивление, слабо связанным с AC или ¬AC.

При соблюдении AC (для любого семейства {S} существует функция выбора f(S)) имеются следующие возможности:
1. Существует не просто f(S), но такая, что для любого S из семейства \(f(S)=\epsilon(S)\) (причём, по очевидным причинам, единственная). Это и есть тот самый вопрос, с которого всё вообще начиналось, но поставленный правильным образом. В этом случае AC в стандартной форме является именно таким ненужным усложнением, каким и выглядит - достаточно аксиомы, что для любого множества S \(\epsilon(S)\) (как операция!) определена и даёт элемент S. Имея такую операцию, можно построить и, собственно, функцию. Только уже зачем?

2. Возможен случай, когда f(S) существует, но такого, который равен результату \(\epsilon(S)\), не существует: \(\epsilon(S)\) даёт результат, не принадлежащий S.
3. Аналогично 2, но по той причине, что \(\epsilon(S)\) не определён для S.
Формально такие аксиоматики возможны и совместимы с AC. Но в практическом смысле они бессмысленны, поскольку выглядят целенаправленным созданием себе трудностей. Таким образом, наиболее естественной заменой стандартной AC, является именно 1 (свойство операции \(\epsilon(S)\)).
Кроме решения проблемы операции выбора, естественная замена AC вскрывает ещё один момент: "выделенная" f(S) единственна только в пределах зафиксированной аксиоматики, однако возможны форки с разными "выделенными" f(S) (соответственно, и разными \(\epsilon(S)\)). И теперь у нас есть инструмент, позволяющий контролировать такие ситуации и предотвратить совмещение доказательств из разных форков. По умолчанию считаем, что в одном доказательстве используется \(\epsilon_1(S)\), а в другом - \(\epsilon_2(S)\). Тогда, если мы строим на их основе третье доказательство (с, вообще говоря, \(\epsilon_3(S)\)), нам следует начать с добавления аксиомы \(\forall S \epsilon_1(S)=\epsilon_2(S)=\epsilon_3(S)\). Если из совмещения доказательств следует нарушение этой аксиомы, значит, доказательства - из несовместимых аксиоматик.

При отрицании AC отсутствие функции выбора не обязано быть тотальным - достаточно существования по крайней мере одного семейства, для которого такая функция отсутствует. В ракурсе свойств \(\epsilon(S)\) это (не вдаваясь в детали) оставляет нам только две возможности, аналогичные пп. 2 и 3 из AC-ветки:
1. Существует множество S, для которого \(\epsilon(S)\) не определена.
2. Существует множество S, для которого \(\epsilon(S)\) даёт элемент, не принадлежащий S.

Вариант 2 здесь тоже можно отбросить, как практически бессмысленный. Остаётся вариант естественной замены ¬AC, который очень кстати оказывается отрицанием "естественной замены AC" (п. 1 из ветки AC): существует множество S, для которого \(\epsilon(S)\) не определена. Что характерно - независимо от того, существует или нет функция выбора для S.

Естественная замена ¬AC уже самим своим видом выпукло демонстрирует искусственную ущербность по сравнению с естественной заменой AC (и, соответственно, ущербность стандартного ¬AC, которое для неё требуется). Теория, по большому счёту, строится именно вокруг операции выбора на множестве - и в чём тогда смысл вводить в неё множества, на которых операция специально запрещается?
И в то же время естественная замена ¬AC демонстрирует ущербность стандартной формы AC, поскольку совместима с ней (п. 3 из AC-ветки).

Вот таким нехитрым образом ситуация ставится с головы на ноги, и в неё возвращается здравый математический смысл.

В заключении е следует отметить, что в своей основе идея не нова, и её задвигал ещё Гильберт - но, как водится у математиков, перемудрил. С высоты современности вижу два недостатка в его подходе:
- "недетерминистичность" операции (т. е., запрещено опираться на предположение, что применение \(\epsilon\) к одному и тому же объекту в разных участках рассуждения даёт один и тот же результат). Это совершенно излишнее и ненужное усложнение. С тем же эффектом можно ввести несколько разных \(\epsilon_1, \epsilon_2, ... \epsilon_n\) и использовать их там, где важно "не гарантировать одинаковость результата". Но проще не выпендриваться и использовать один, не стесняясь полагаться на детерминистичность, а разные вводить при соединении независимо сделанных рассуждений, как показано выше.
- операция вводится слишком рано - для "x, удовлетворяющего предикату", но ещё до введения понятия множеств и связанных аксиом, оставляя висящий в воздухе вопрос - "а из чего выбираем-то?". Применимость \(\epsilon\) следует ограничить именно множествами - это снимает множество вопросов. Хотя, попробовал тут перепостроить логику первого порядка на альтернативном базисе и понял, почему пришлось делать именно так.

А функция выбора действует на каком множестве? Множестве всех множеств?

1 frag / 2 deaths
> А функция выбора действует на каком множестве?
Если она глобальная, то она класс-функция, т. е. действует на классе (всех множеств). ЫЫ сказал, что так можно. Таким же образом легитимизируется мощность множества как функция от множества, и т. п. конструкции.

Sbtrn. Devil
  А switch()  чем не устраивает?

xlat-code
> если аксиома выбора будет улучшена, то тогда что?
Она, для начала, станет проще и натуральнее в формулировке, и её можно будет доносить до людей без подрыва моска. Сейчас-то как? "Для любого семейства непустых множеств существует функция, которая сопоставляет каждому множеству его элемент." Штоблън? Мы разве не можем просто выбрать из любого множества его элемент? Оказывается, можем, и это даже доказывается. Ну так разве этого не достаточно? В чём проблема с привлечением этого самого выбора из каждого отдельного множества задать эту самую функцию на этом самом семействе? А вот, оказывается, проблема. Функция выбора - это, оказывается, одно, а сам выбор - это другое и понимать надо.
А после улучшения всё будет просто: базовым элементом языка является оператор выбора \(\epsilon\), который при применении к любому непустому множеству возвращает элемент этого множества. Как оно и just as planned. Только теперь, поскольку этот оператор - не "мета-операция" мутного статуса, а базовый элемент языка, не определяемый ни через какие второстепенные объекты, для построения "функции из семейства" (если она вдруг нужна) его можно просто брать и применять.
И ещё станет очевидно, что отказ от аксиомы выбора маразматичен, ибо по факту требует, чтобы операция выбора из некоторых множеств прямо запрещалась, причём на каждом шаге рассуждения должны действовать свои правила запрещения. А это уже фигня какая-то, а не математика.

Вот, кстати, ещё одна причина для введения операции \(\epsilon\).
В гильбертовском варианте (не считая недетерминированности) у выбора есть следующие свойства: его можно применять к абсолютно любому предикату, при этом, если возможно выбрать некий x, удовлетворяющий предикату P(x), то \(\epsilon(P)\) удовлетворяет этому предикату (\(P(\epsilon(P))=T\), или, сокращённо, \(P(\epsilon(P))\)), а если невозможно, то выбирается некий левый x, не удовлетворяющий предикату (\(P(\epsilon(P))=F\), или \(\lnot P(\epsilon(P))\)).
Это значит, что кванторы можно выразить через операцию выбора:
\((\exists x: P(x))\ =\ P(\epsilon(P))\) (существует x такой, что для него соблюдается P = можно выбрать элемент, для которого P соблюдается)
\((\forall x: P(x))\ =\ \lnot P(\epsilon(\lnot P))\) (для всех x соблюдается P = нельзя выбрать элемент, для которого P не соблюдается [а можно только такой, для которого соблюдается])
И, как только мы определим кванторы таким образом, автоматически устраняется целый класс парадоксов (парадокс Берри во всех своих вариантах).
Каноническая форма парадокса: должно существовать число, описываемое не менее чем за N слов, но его существование невозможно, поскольку оно описано за менее чем N слов и, соответственно, не является таковым. Стандартная логика по такому поводу мычит пространно и неопределённо, в том смысле, что не только лишь всякий предикат - какой надо предикат, и нужно тщательно изучать конкретную ситуацию.

Но теперь обозначим "парадоксальное" свойство как предикат P(x) и запишем парадокс в терминах операции выбора:
1) Выбираем число x, удовлетворяющее P(x): \(x = \epsilon(P)\)
2) Парадокс в том, что \(\lnot P(x)\), то есть: \(\lnot P(\epsilon(P))\)
И что же мы видим? Видим - прямо по определению - утверждение, эквивалентное \(\lnot\exists x: P(x)\) Т. е., элемента x со свойством P просто не существует. И, что характерно, безотносительно каких-либо подробностей насчёт P. Без разницы, самореференция там, неправильная аксиоматика, или ещё какие причины - если свойство требует парадокса, то элементов с таким свойством не существует по определению существования, и весь сказ. Это намного проще, чем заморачиваться вопросами кошерности предиката.