Глава 3. Сравнение мощностей без выбора: Шрёдер–Бернштейн и теорема Кантора

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

Глава 10.2 показала, что счётность и несчётность — не размеры готовых множеств, а правила о процессах. Естественный следующий вопрос: как сравнивать мощности — и нужна ли для этого аксиома выбора? В ZFC с выбором классика отвечает так: кардиналы образуют линейно упорядоченную шкалу (вполне упорядоченную благодаря выбору), и на завершённых $\aleph$-объектах определена кардинальная арифметика.

ToS читает сравнение иначе. Если «быть счётным» и «быть несчётным» — роли, то их упорядочение есть правило: один носитель вкладывается в другой. Мощность — не число, приклеенное к завершённому множеству, а роль, которую носитель (тип) играет в предпорядке вложений. Два носителя равномощны, когда играют одну роль (есть биекция).

Глава держится на двух столпах, оба — без аксиомы выбора:

• Шрёдер–Бернштейн: если $A$ вкладывается в $B$ и $B$ в $A$, то $A$ и $B$ равномощны. Это делает предпорядок вложений антисимметричным с точностью до биекции — и доказывается без выбора, ценою L3 и L4 (не 0 аксиом), на конечной глубине цепи.
• Общая теорема Кантора: ни один носитель не накрывает (сюръективно) своё пространство bool-предикатов. Максимальной мощности нет — и это конструктивно, без единой аксиомы.

И сразу честная оговорка, которую глава доведёт до конца: обратный мост — от сюръекции $A\twoheadrightarrow B$ к вложению $B\hookrightarrow A$ — это в точности аксиома выбора. В ToS он не доказывается; именно там, и только там, в теории мощностей живёт выбор.

Мощность — роль-режим сравнения, а не кардинал-число; её упорядочение — правило вложения. Антисимметрия (Шрёдер–Бернштейн) и отсутствие максимума (Кантор) держатся без выбора; выбор локализуется в одном переходе — сюръекция в инъекцию.

Сравнение как роль; инъекция как правило-предпорядок

Зафиксируем три роли сравнения для носителей (типов) $A,B$:

$$A\le B:=\exists \text{инъекция }A\to B;A\twoheadrightarrow B:=\exists \text{сюръекция};A\simeq B:=\exists \text{биекция.}$$

Отношение $\le$ (вложение) — предпорядок: рефлексивно (тождественная инъекция) и транзитивно (композиция инъекций инъективна). Оба свойства конструктивны, без аксиом. Так же ведут себя сюръекция и биекция: композиция сохраняет каждую из ролей.¹

Смысл, как и прежде, в категории. «Мощность $A$» — не число, приписанное завершённому множеству, а роль, которую $A$ играет в этом предпорядке: ниже одних носителей, выше других. Равномощность $A\simeq B$ — совпадение ролей. Никаких $\aleph$-объектов для этого не нужно: сравнение есть правило о носителях, а не арифметика готовых кардиналов.

$\le$ — роль-правило (предпорядок вложений), конструктивно рефлексивное и транзитивное; мощность — позиция носителя в этом предпорядке, равномощность — совпадение ролей.

Шрёдер–Бернштейн без выбора

Антисимметрия предпорядка — содержательное ядро теории мощностей: если $A\le B$ и $B\le A$, то $A\simeq B$. Это теорема Шрёдера–Бернштейна.

Классическое доказательство прослеживает для каждой точки бесконечную «челночную» цепь $\dots \to a\to f(a)\to \dots$ под двумя инъекциями. ToS заменяет завершённую бесконечную цепь конечной глубиной — натуральным числом: каждая точка либо укоренена на конечной глубине (доходит до точки без прообраза за конечное число шагов), либо принадлежит двусторонне-бесконечной цепи. Биекция $h$ собирается по этому признаку: на укоренённых в $B$ точках берём частичный обратный $g^{-1}$, иначе — $f$. Бесконечный объект заменён конечным процессом — ход в духе P4.²

Какова аксиомная цена? Ровно classic (L3) и L4_witness (L4) — и не аксиома выбора.³ L3 входит как разрешимость признака укоренённости; L4_witness выбирает свидетеля из одного существования, а не функцию по произвольному семейству — оба строго слабее выбора. Поэтому фундаментальная теорема о мощностях держится без выбора.

Шрёдер–Бернштейн — роль-правило антисимметрии $\le$: два встречных вложения дают биекцию. Завершённая цепь заменена конечной глубиной (P4); цена — L3$+$L4, не выбор.

Теорема Кантора: нет максимальной мощности

Второй столп — общая теорема Кантора: для любого типа $X$ нет сюръекции $X\to (X\to \mathtt{bool})$. Доказательство — та же диагональ, что в 10.2, но для произвольного носителя: предикат $g(x):=\neg f(x)(x)$ не совпадает ни с одной «строкой» $f(a)$, ибо в точке $a$ они различаются. Замечательно, что никакого жителя типа $X$ не требуется: сама сюръективность поставляет свидетеля — тот $a$, для которого $f(a)=g$, — и приводит к противоречию $f(a)(a)=\neg f(a)(a)$.⁴

Отсюда: ни один носитель не накрывает своё пространство bool-предикатов — максимальной мощности нет. Над любым $X$ есть роль, которую он не накрывает сюръективно — пространство предикатов $X\to \mathtt{bool}$.⁵ Именно в этом канторовском (сюръективном) смысле максимума нет: это не строгость в инъекционном порядке (инъекция $X\hookrightarrow (X\to \mathtt{bool})$ для произвольного $X$ потребовала бы разрешимого равенства) и не построение полной линейной шкалы кардиналов.

Честная оговорка о категории. Речь о типе bool-предикатов $X\to \mathtt{bool}$, а не о завершённом степенном множестве $\mathcal{P}(X)$ как объекте. Степень-как-множество в ToS структурно не строится (P1, Глава 10.1): «множество всех подмножеств» потребовало бы критерия по своему же уровню. Поэтому «нет максимальной мощности» — утверждение о роли-сравнении (нет накрывающей сюръекции), а не о построении $\mathcal{P}(X)$.

Теорема Кантора — роль-правило отсутствия максимума: каждый носитель не накрывает сюръективно свою bool-степень. Конструктивно (0 аксиом) и о ролях-типах, а не о завершённом степенном объекте.

Где живёт выбор: честная граница

Теперь точно укажем, где в теории мощностей появляется аксиома выбора. Антисимметрия дала $A\simeq B$ из двух инъекций. А что, если есть две сюръекции — или сюръекция $A\twoheadrightarrow B$, из которой хочется получить вложение $B\hookrightarrow A$?

Именно этот обратный мост — выбрать по одному прообразу для каждого $b\in B$ — и есть аксиома выбора (выбор по слоям сюръекции). В ToS он не доказывается и честно помечен как граница.⁶ С одним лишь L4_witness можно обратить биекцию (прообразы единственны), но не произвольную сюръекцию (прообразов в слое может быть много, и нужен выбор по всем слоям сразу).

Вот почему антисимметрия $\le$ опирается на Шрёдер–Бернштейна (L3$+$L4), а не на выбор: она работает с инъекциями, где обратный частичный однозначен. Содержательные результаты главы — предпорядок, антисимметрия, отсутствие максимума — выбора не требуют; выбор локализован ровно в одном непроведённом переходе.

Сюръекция-в-инъекцию — это ровно место, где требуется выбор, и ToS его не проводит. Антисимметрия живёт на инъекциях (L4 обращает единственное), а не на слоях сюръекции (где нужен выбор).

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

Слой	Содержание
Rules (L5)	предпорядок вложений $\le$ (рефл.$+$транз.); Шрёдер–Бернштейн (конечная глубина цепи) для антисимметрии; диагональ Кантора для отсутствия максимума
Roles (L4)	мощность$=$роль-позиция в предпорядке; $\simeq =$совпадение ролей; bool-степень$=$роль, не накрываемая сюръективно
Elements (L1$+$P4)	носители (типы) и их точки; конечная глубина цепи (nat); кардинал-число завершённым Элементом не является

Корректность. $\le$ — корректный предпорядок (инъекции компонуются); $h$ Шрёдера–Бернштейна корректна как биекция (инъективна$+$сюръективна).

Что даёт. Антисимметрия $\le$ — cardinal_antisym (L3$+$L4); отсутствие максимума — no_maximal_cardinality (0 аксиом); предпорядок — 0 аксиом.

Диагностика. В P4-онтологии ToS кардинал как число и «шкала всех кардиналов» — овеществление роли сравнения. Вполне-упорядочение всех мощностей в одну линейную шкалу — это теорема выбора (Цермело), здесь не предполагаемая.

Честные границы. Обратный мост сюръекция$\to$инъекция — сам выбор, не проведён. Степень-как-объект $\mathcal{P}(X)$ не строится (P1). Линейность кардинальной шкалы (трихотомия мощностей) требует выбора и здесь не утверждается.

Сравнение мощностей — предпорядок ролей; антисимметрия (Шрёдер–Бернштейн) и отсутствие максимума (Кантор) держатся без выбора (L3$+$L4 и 0 аксиом соответственно); выбор локализован в единственном непроведённом переходе и в линейности шкалы.

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

Сравнение мощностей оказалось предпорядком ролей-носителей, а не арифметикой завершённых кардиналов. Вложение — конструктивное правило $\le$; Шрёдер–Бернштейн делает его антисимметричным с точностью до биекции (cardinal_antisym, L3$+$L4, конечная глубина вместо бесконечной цепи); общая теорема Кантора лишает шкалу максимума (no_maximal_cardinality, 0 аксиом). Аксиома выбора понадобилась бы лишь для обратного моста сюръекция$\to$инъекция и для линейности шкалы — и именно их ToS не проводит.

Это подводит к Главе 10.4, где аксиома выбора рассматривается прямо — в её двойственной судьбе: запрет завершённо-объектной формы (граф выбора как готовая бесконечность, несовместимая с P4) и переинтерпретация допустимого ядра как правила позиционного разрешения L5.

Мощность есть роль в предпорядке вложений, а не кардинал-число; антисимметрия и отсутствие максимума доказуемы без выбора. Выбор не исчезает — он точно локализуется: в переходе от сюръекции к инъекции и в линейности кардинальной шкалы, которые ToS оставляет непроведёнными.

---

---

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

Навигация: ← Глава 2. Счётность конструктивна; несчётность — правило о процессах · Глава 4. Аксиома выбора: запрет и переинтерпретация →

Footnotes

1. В settheory/CardinalityWithoutChoice.v (эта работа): injects, surjects, bijects; injects_refl, injects_trans (предпорядок $\le$), surjects_refl/_trans, bijects_refl/_trans/_injects/_both — все 0 аксиом. ↩

2. Schroeder_Bernstein (SchroederBernstein_ERR.v): из двух инъекций строится биекция $h$ (инъективная и сюръективная). Глубина цепи — nat; признак B_rooted решается через L3_informative (информативное исключённое третье) — это и есть цена L3. ↩

3. Аксиомный статус сверен Print Assumptions: Schroeder_Bernstein и обёртка cardinal_antisym (CardinalityWithoutChoice.v, эта работа) дают ровно classic $+$ L4_witness. В самом доказательстве L4_witness применяется через производную лемму определённого описания L4_definite (CDD), извлекающую единственный частичный прообраз из $\exists !$ — именно так помечает технику шапка файла. См. различение L4 и выбора в Главе 10.4. ↩

4. cantor_no_surjection (settheory/CantorTheoremGeneral.v, эта работа): $\forall X(f:X\to (X\to \mathtt{bool})),\neg ‘surjective‘f$. Чисто конструктивно, 0 аксиом; работает для любого $X$ без предположения о его населённости. ↩

5. no_maximal_cardinality (CardinalityWithoutChoice.v): $\forall X,\neg (X\twoheadrightarrow (X\to \mathtt{bool}))$. Следствие cantor_no_surjection; 0 аксиом. ↩

6. Документировано в шапке CardinalityWithoutChoice.v: переход surjects $\to$ injects обратного направления есть выбор и здесь не выводится. ↩