Глава 4. Аксиома выбора: запрет и переинтерпретация

Где стоит глава

Глава 10.3 локализовала выбор: он не нужен ни для предпорядка вложений, ни для Шрёдера–Бернштейна, ни для Кантора — но появляется в переходе сюръекция$\to$инъекция и в требовании линейности кардинальной шкалы. Теперь рассмотрим аксиому выбора прямо. Ответ ToS двойствен, и эта двойственность — центральный E/R/R-диагноз сильной аксиомы:

• Переинтерпретация. Допустимая работа выбора — взять по одному элементу из каждого множества конечного семейства (или из приближения процесса) — выполняется правилом: позиционным разрешением L5 («голова списка»). Тогда выбор — не аксиома, а теорема конечной комбинаторики.
• Запрет. Завершённо-объектная форма выбора — функция выбора $f:N\to N$, граф которой $\{(n,f(n))\}$ есть готовая бесконечная совокупность, — противоречит P4. Уже нат-индексированная completed-object форма AC не «не принимается», а несовместима с конечной актуальностью; полная ZFC-AC тем более содержит такую object-форму.

И — синтез: запрет строго сильнее переинтерпретации. Если завершённая форма невозможна, то и аксиомой она быть не должна. Точный диагноз таков: аксиома выбора смешивает законное Правило (разрешение L5 по запросу) с незаконной Элемент-овеществлённостью (завершённый граф выбора). ToS сохраняет первое и отвергает второе. Сразу оговорка, проходящая сквозь главу: принцип L4 (L4_witness) — это не аксиома выбора.

Аксиома выбора — роль-смешение: законное правило разрешения L5 склеено с незаконным завершённым графом. ToS переинтерпретирует первое как теорему и запрещает второе как несовместимое с P4; запрет сильнее переинтерпретации.

Допустимое ядро: выбор как правило L5{L5}

Что в ToS есть «множество» на стадии $N$? Конечный список. А что значит «выбрать из него элемент»? Взять первый в конститутивном порядке — голову списка. Это и есть L5: позиционное разрешение. Для непустого списка голова в нём лежит; для семейства непустых списков функция «голова» даёт выбор сразу для всех.¹

Поэтому допустимое ядро выбора — теорема конечной комбинаторики, а не постулат: L5 (порядок, уже несущий статус позиции) сам производит функцию выбора. Из той же конечности следует и «конечная лемма Цорна»: в непустом конечном списке есть максимальный элемент — просто максимум списка, без всякого выбора.²

Важная честная оговорка о границе этого ядра. Версия с квантором по всем натуральным индексам ($\forall i$) читается двояко. Как правило процесса — «выбор по запросу для любого предъявленного индекса» — она P4-совместима. Как завершённый граф $\{(i,f(i))\}$ — попадает под запрет следующего параграфа. Поэтому однозначно P4-совместима именно постадийная версия с конечным фронтом $N$; неограниченную следует читать как правило-на-запрос, а не как готовый объект.³

Выбор на конечном/постадийном семействе — роль-правило L5 (голова в конститутивном порядке); функция выбора и конечная лемма Цорна суть теоремы (0 аксиом), а не постулаты. Неограниченную версию читаем как правило-на-запрос, не как объект.

Запрет: завершённый граф выбора несовместим с P4{P4}

Возьмём полную форму выбора над $N$: для любого семейства непустых списков $F:N\to$ list $N$ существует функция $f:N\to N$ с $f(n)\in F(n)$ для всех $n$. Ключевой момент: такая $f$, взятая разом по всем $n$ как готовый объект (в коде эту завершённую тотальность кодирует choice_graph — завершённую поддержку области, а не множество пар с их значениями), есть завершённая бесконечность. А P4 (конечная актуальность) требует, чтобы на каждой стадии было актуально лишь конечное. Завершённая бесконечная совокупность нарушает эту ограниченность — противоречие.⁴

Значит, уже нат-индексированная completed-choice форма AC несовместима с P4 — это сильнее, чем «мы её не принимаем»; полная ZFC-AC тем более содержит такую object-форму, но формальный файл фиксирует именно нат-индексированный диагноз. Здесь надо точно развести потенциальную и завершённую бесконечность. ToS не запрещает бесконечные процессы: потенциальная бесконечность с P4 вполне совместима.⁵ Запрещён ровно завершённый выбор-как-объект: график, взятый разом, целиком, как готовая вещь. Это и есть отказ Элемент-слоя овеществлять то, что законно лишь как правило-на-запрос.

Полная аксиома выбора — роль-овеществление: завершённый граф $\{(n,f(n))\}$ как готовый бесконечный объект. P4 его запрещает (completed_inf_contradicts_P4); потенциальная бесконечность процесса при этом совместима. Запрет, а не просто отказ от постулата.

Синтез: запрет сильнее переинтерпретации

Два уровня — не одно и то же, и их связь сама есть теорема. Переинтерпретация говорит: P4 делает выбор ненужным как аксиому, ибо его работу выполняет L5. Запрет говорит: P4 несовместима с завершённой формой выбора. В формальном синтезе запрет даёт переинтерпретацию (если завершённый объект невозможен, он тем более не нужен как постулат), тогда как одна переинтерпретация сама по себе противоречия object-формы не даёт — в этом смысле запрет сильнее.⁶

Это и есть точный E/R/R-диагноз сильной аксиомы. Аксиома выбора склеивает две разные вещи: законное правило (разрешение L5 по запросу, на конечном фронте) и незаконную Элемент-овеществлённость (завершённый график как готовый объект). ToS расклеивает их: правило сохраняет (теорема, 0 аксиом), объект отвергает (несовместим с P4). Тот же диагноз применим и к другим сильным аксиомам — это увидим в 10.5 на бесконечности, импредикативности, ATR${}_0$ и ${\Pi }_1^1$.

Запрет$\Rightarrow$переинтерпретация (строго): невозможность завершённого объекта сильнее его ненужности. E/R/R-диагноз AC: расклеить законное правило L5 и незаконный завершённый граф; сохранить правило, отвергнуть объект.

L4{L4} не есть выбор; и почему нет Банаха–Тарского

Критическое различение, на котором держится вся Часть X. Принцип L4 (L4_witness) извлекает свидетеля из одного существования: из $\exists x,P(x)$ — объект $\{x\mid P(x)\}$. Аксиома выбора берёт функцию по произвольному семейству существований сразу. Это объекты разной онтологической категории: определённость единичного существования против одновременного отбора по неограниченной завершённой совокупности.⁷ Поэтому результаты 10.3 (Шрёдер–Бернштейн, антисимметрия) используют L4, но не выбор: L4 обращает единственное, а выбор отбирал бы по слоям. При этом L4 — не 0-аксиомная конструкция, а отдельный свидетельский принцип уровня L4 (в 10.3 он применялся через L4_definite); его цена учитывается отдельно от выбора.

Отсюда и судьба патологий выбора. Парадокс Банаха–Тарского и неизмеримые множества Витали требуют изготовить неизмеримое множество выбором по несчётному семейству классов. В текущем finite/list-слое P4 такого основания нет: всякое разрешимое подмножество конечного списка само есть конечный список (фильтр), а длина сохраняется при конечном разбиении — парадоксальному удвоению не на чём держаться.⁸

L4 (свидетель из одного $\exists$) — не выбор (отбор по семейству); это разные категории. Патологии выбора (Витали, Банах–Тарский) лишаются опоры: при P4 разрешимые подмножества конечного остаются конечными, длина аддитивна.

E/R/R-разбор

Слой	Содержание
Rules (L5)	разрешение L5 (голова списка) — выбор на конечном/постадийном семействе; P4-ограниченность стадии (источник запрета завершённого графа)
Roles (L4)	«выбор»$=$роль-правило разрешения; завершённый граф $\{(n,f(n))\}=$незаконная роль-овеществлённость; L4$=$свидетель из одного $\exists$ (не выбор)
Elements (L1$+$P4)	конечные списки на каждой стадии; функция выбора как завершённый бесконечный граф Элементом не является

{ Что даёт. Допустимое ядро — теорема (AC_is_L5, P4_eliminates_AC_finite, finite_zorn; 0 аксиом). Полная форма — запрещена (P4_prohibits_AC, completed_inf_contradicts_P4). Связь — prohibition_implies_reinterpretation (запрет сильнее).}

Диагностика. В P4-онтологии ToS аксиома выбора — склейка правила L5 и завершённого графа-Элемента. L4 с ней путать нельзя: разные категории.

Честные границы. P4_eliminates_AC доказана для семейств конечных списков (конечных множеств) / как правило-на-запрос — это не полная ZFC-AC, которую P4 как раз запрещает. Анти-Банах–Тарский — отсутствие опоры (разрешимые конечные подмножества$+$аддитивность длины), а не метатеорема о ложности парадокса. Потенциальная бесконечность совместима; запрещён лишь завершённый объект.

Выбор расщепляется надвое: правило L5 (теорема, 0 аксиом) и завершённый граф (запрещён P4). Запрет сильнее переинтерпретации; L4 — иная категория, не выбор; патологии выбора лишены опоры.

Итог и переход

Аксиома выбора получила в ToS двойственную судьбу. Её допустимое ядро — выбор по конечному (или постадийному) семейству — есть теорема: позиционное разрешение L5 производит функцию выбора без всякой аксиомы (AC_is_L5, P4_eliminates_AC_finite). Её завершённо-объектная форма — график выбора как готовая бесконечность — запрещена, ибо несовместима с P4 (completed_inf_contradicts_P4); и запрет строго сильнее переинтерпретации (prohibition_implies_reinterpretation). Принцип L4 — не выбор, а определённость единичного существования; патологии выбора при P4 лишаются опоры.

Глава 10.5 распространит тот же двухуровневый диагноз на остальную башню сильных аксиом: ординалы как процессы, а Бесконечность, импредикативное свёртывание, арифметическую трансфинитную рекурсию (ATR${}_0$) и ${\Pi }_1^1$-свёртывание — как сильные принципы, чьё допустимое ядро переинтерпретируется, а завершённо-объектная форма запрещается.

Аксиома выбора в ToS — не принимается и не отвергается целиком: её правило-ядро становится теоремой L5, а её завершённый граф запрещается P4. Это образец E/R/R-разбора сильной аксиомы — расклеить законное правило и незаконный завершённый объект, — и Часть X применит его дальше ко всей башне оснований.

---

---

Часть: Часть X. Теория множеств без аксиомы выбора · Том: «Математика»

Понятия: Парадокс

Навигация: ← Глава 3. Сравнение мощностей без выбора: Шрёдер–Бернштейн и теорема Кантора · Глава 5. Ординалы как процессы; башня сильных аксиом (ATR_0, ^1_1) и её снятие →

Footnotes

1. P4_Eliminates_AC.v: L5_choose (голова списка), finite_choice (голова непустого списка в нём лежит), AC_is_L5 (для семейства непустых списков функция выбора — голова), P4_eliminates_AC_finite (явная версия для конечного фронта $\{0,\dots ,N-1\}$). Всё 0 аксиом. ↩

2. finite_zorn (P4_Eliminates_AC.v): $\forall l\ne \varnothing ,\exists m\in l,\forall n\in l,n\le m$. 0 аксиом. ↩

3. Это различение явно зафиксировано в комментарии P4_Eliminates_AC.v к P4_eliminates_AC: читать как процессное правило — P4-совместимо; читать как завершённый граф — под P4ProhibitsAC.v. ↩

4. P4ProhibitsAC.v: AC_on_nat (полная форма), ac_implies_completed (AC даёт завершённый граф), P4_prohibits_AC. И P4CompletedInfinity.v: CompletedInfSet против P4_stage_bounded, итог — completed_inf_contradicts_P4. Всё 0 аксиом. ↩

5. P4CompletedInfinity.v: potential_compatible_with_P4 — потенциальная бесконечность не противоречит P4. Запрещён именно завершённый объект, не процесс. ↩

6. P4ProhibitionSynthesis.v: prohibition_implies_reinterpretation (запрет влечёт переинтерпретацию), reinterpretation_weaker (обратное неверно), P4_is_prohibition. 0 аксиом. ↩

7. ToS_Axioms.v, шапка прямо это проговаривает: «This is NOT the Axiom of Choice»; L4_witness — (exists x, P x) -> {x | P x}, не ZFC-AC и не зависимый выбор. Сравнивать их на одной «шкале силы» — категориальная ошибка. ↩

8. P4_Eliminates_AC.v: decidable_subset_finite (разрешимое подмножество конечного списка конечно), finite_decomposition_preserves_length (длина аддитивна при конкатенации). Это не метатеорема «Банах–Тарский ложен», а отсутствие опоры для построения: нет неизмеримых кусков — нет и парадоксального разбиения. ↩