Глава 6. Синтез Части X: что доказуемо без выбора, и карта границ

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

Часть X прошла путь от оснований к их границе. Глава 10.1 переставила онтологию: множество — роль-Система, принадлежность — роль, парадоксы — ошибки овеществления. Глава 10.2 прочла счётность и несчётность как правила о процессах. Глава 10.3 свела сравнение мощностей к предпорядку вложений (Шрёдер–Бернштейн, Кантор) — без выбора. Глава 10.4 разложила аксиому выбора надвое: правило L5 переинтерпретируется, завершённый граф запрещается P4. Глава 10.5 распространила тот же двухуровневый диагноз на ординалы-процессы и башню сильных аксиом (Бесконечность, импредикативность, ATR${}_0$, ${\Pi }_1^1$).

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

Заключительная глава Части X: синтез доказуемого без выбора, карта аксиомных цен и честная стена. Единый итог — смена категории, а не доказательство ZFC без аксиомы выбора.

Ещё доказуемое без выбора: wqo и конечная детерминированность

Помимо ядра (счётность, диагональ, Шрёдер–Бернштейн, Кантор) кластер settheory/ проводит без выбора и более «высокие» результаты. Лемма Хигмана: списки над конечным алфавитом образуют хорошо-квазиупорядочение (wqo) — доказано для конкретных алфавитов (единичного, булева, $N$) с леммой Диксона в основе.¹ Теорема Крускала: конечные деревья wqo под гомеоморфным вложением — доказано для конкретных семейств (цепи, вилки, растущие последовательности, деревья глубины $\le 1$).² Кантор–Бендиксон: производная замкнутого множества как процесс, $\omega$-предел — совершенное ядро.³ И конечная детерминированность игр (Цермело, 1913): всякая конечная игра определена.⁴

Честная мера повсюду одна. Эти результаты классически считаются «высокими» (полная теорема Крускала имеет большую ординальную силу); ToS проводит их конструктивные ядра для конкретных семейств без выбора — но не в полной общности. Это и подводит к карте границ.

Без выбора доказуемы и wqo-результаты (Хигман, Крускал — для конкретных семейств) и конечная (цермеловская) детерминированность. Это конструктивные ядра «высоких» теорем, не их полная общность.

Карта аксиомных цен

Все результаты Части X выстраиваются по цене аксиом. Это оформлено как разрешимая таблица: каждому результату сопоставлен ярус, и доказан итог — ни один доказанный результат не требует полной аксиомы выбора (ZFC).⁵

Ярус (цена)	Результаты
0 аксиом	счётность ℚ (Калкин–Уилф); диагональ (diagonal_differs); общий Кантор $X\to (X\to \mathtt{bool})$; Кантор–Бендиксон; ординалы, ${\epsilon }_0$, wf_ord_lt, transfinite_ind (сверено Print Assumptions: Closed); уровневая индукция; P4_Eliminates/Prohibits-кластер — ATR, Бесконечность, импредикативность
classic (L3)	несчётность $[0,1]$ (трисекция); Хигман; Крускал (конкретные семейства); конечная детерминированность
classic $+$ L4	Шрёдер–Бернштейн; антисимметрия мощностей (cardinal_antisym)
вычислительный примитив	${\Pi }_1^1$-переинтерпретация — 0 логич. аксиом, но при eval_program (Parameter)
Граница (PBoundary)	завершённый актуально-бесконечный объект — единственный P4-запрет (вкл. завершённый граф-выбора и $\mathcal{P}(\mathbb{N})$ как Element; правило-ядро выбора у нас — L5); процессные формы высоких теорем (полный wqo Крускала, борелевская детерминированность) — не привлечены, не построены

Главное наблюдение: содержательное ядро теории множеств — от счётности до Кантора–Бендиксона и wqo — живёт на ярусах 0/ L3/ L3$+$L4, и ни один доказанный результат не требует полной аксиомы выбора.

Важно: граница названа в наших терминах. <<Полная AC>> как аксиома и её метатеоретическая независимость — утверждения о ZFC (другой системе), не точки нашего пространства; внести их в <<нашу границу>> значило бы повторить ту самую категориальную ошибку смешения уровней, которой открывается Часть X. Наша граница — один P4-запрещённый объект (завершённая актуальная бесконечность); а мнимая <<завершённая бесконечность>> высоких теорем при откате оказывается ZFC-упаковкой (ниже).

Карта цен — роль-аудит: каждый результат несёт ярус (0 / L3 / L3$+$L4), и доказано, что доказанное не требует полной AC. Цена меряется явно, а не замалчивается.

Честная стена: куда ToS не заходит

Граница Части X двоякая, и эти два рода рубежа нельзя смешивать.

Первый род — не привлечено / не построено (открыто, но не противоречиво): процессные формы высоких теорем — полная теорема Крускала во всей общности и борелевская (Мартина) детерминированность (их откат — ниже); обратный мост сюръекция$\to$инъекция (это сам выбор); линейность кардинальной шкалы (трихотомия мощностей, тоже выбор); трансфинитная рекурсия за пределами конструктивных нотаций. Сюда ToS не заходит — но и не отрицает: это направления, а не противоречия. (Завершённый степенной объект $\mathcal{P}(X)$ в этот список не входит: его bool-предикатный слой $X/\twoheadrightarrow (X\to \mathtt{bool})$ доказан в 10.3, а сам завершённый объект — не открытое направление, а артефакт упаковки: см.\ откат ниже и второй род.)

Второй род — запрещено P4 (object-форма несовместима): завершённый граф выбора (completed_inf_contradicts_P4); завершённая бесконечность как объект; степенное множество $\mathcal{P}(X)$ как завершённый Элемент (P1); импредикативная тотальность-в-себе (P1$+$P4). Это не «пока не доказано», а несовместимо с конечной актуальностью.

Различение существенно: не привлечено слабее, чем запрещено. Большая часть стены — первого рода (честные открытые направления); меньшая, но принципиальная — второго (завершённые объекты, противоречащие P4).

И один аудит на все аксиомы сразу. Из девяти аксиом ZFC три — Расширяемость, Пары, Объединение — структурно тривиальны; Бесконечность, Выделение, Подстановка заменены P4; Фундирование — P1; Выбор — L5; и ровно одна, Powerset, ложится на role-limit-сторону границы: конечный степенной объект $2^n$ перечислим явно (Element, доказано), а полный $2^{\mathbb{N}}$ — несчётность. Powerset — единственная <<цена>>.⁶

И тот же откат — для <<высоких>> теорем; здесь сила системы видна прямо. То, что классически требует завершённой бесконечности — полный $\mathcal{P}(\mathbb{N})$, минимально-плохая последовательность Крускала, башня итерированных степеней Бореля, — при разборе оказывается ZFC-упаковкой, а не стеной: содержание достигается без завершённого объекта. Степень есть роль-тип $\mathbb{N}\to \mathtt{bool}$: на каждой конечной стадии ровно $2^n$ подмножеств, а её ядро <<несчётность>> — отсутствие перечислителя ролей (диагональ), 0-аксиомно; конечная детерминированность — обратная индукция на дереве игры, тоже без башни. Остаётся ровно один подлинный запрет — завершённая актуальная бесконечность как объект; полный wqo и борелевская детерминированность — не стены, а не привлечённые процессные конструкции.⁷

Стена двоякая: не привлечено (процессные формы полного Крускала и Мартина, мост выбора, линейность шкалы — открыто) и запрещено P4 (завершённый граф, завершённая бесконечность, степень-объект, тотальность-в-себе — несовместимо). А <<полная AC>> и её метатеоретическая независимость — о самой ZFC, не наша граница. Не смешивать.

Единая E/R/R-структура Части X

Вся часть — одна система: теория множеств как процесс ролей над конечно-актуальными носителями.

Слой	Содержание
Rules (L5)	порядок уровней P1; критерий$+$P2; разрешение L5 (выбор); диагональ/трисекция; конечная глубина цепи (SB); структурная рекурсия по Ord; функция$=$код
Roles (L4)	множество$=$Система; $\in =$роль позиции; мощность$=$роль-сравнение; выбор$=$роль-правило; ординал$=$роль-процесс
Elements (L1$+$P4)	на каждой стадии конечные данные (список, ℚ, путь, нотация, код); завершённые тотальности (граф выбора, $2^{{\aleph }_0}$-объект, $\mathcal{P}(X)$, несчётное пространство функций) Элементами не являются

Двухуровневый диагноз — единообразно. Каждая сильная аксиома склеивает законное правило (которое ToS сохраняет и переинтерпретирует как теорему) с незаконной завершённо-объектной формой (которую ToS не привлекает или запрещает P4). Парадоксы (Рассел, Кантор, Бурали-Форти) — предельный случай: овеществление правила-тотальности как Элемента, снятое P1$+$P4.

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

Часть X — одна система: теория множеств как процесс ролей. Каждый сильный принцип разложен надвое (правило$+$завершённый объект); правило сохранено, объект отведён или запрещён. Смена категории, а не ослабление ZFC.

Закрытие Части X

Теория множеств перестроена без аксиомы выбора и без завершённой бесконечности — с P4 как центральным фильтром в уровневом E/R/R-каркасе (P1, P2, L3–L5). Содержательные теоремы выжили: Шрёдер–Бернштейн и общая теорема Кантора без выбора, конструктивная счётность ℚ, несчётность через диагональ и трисекцию, дихотомия Кантора–Бендиксона, wqo-результаты Хигмана и Крускала для конкретных семейств, конечная детерминированность. Сильные аксиомы — выбор, бесконечность, импредикативность, ATR${}_0$, ${\Pi }_1^1$ — получили единый двухуровневый разбор: законное ядро переинтерпретировано, завершённо-объектная форма отведена или запрещена. И граница очерчена честно, в двух родах: не привлечено и запрещено.

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

Теория множеств без аксиомы выбора — не ZFC с вычетом, а другая категория: множество есть роль-Система, мощность и выбор — правила, бесконечность — процесс. Доказуемое без выбора простирается до Шрёдера–Бернштейна, bool-варианта теоремы Кантора ($X/\twoheadrightarrow (X\to \mathtt{bool})$), Кантора–Бендиксона и wqo; за честной стеной — открытые направления и завершённые объекты, несовместимые с P4. Таков итог Части X.

---

---

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

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

Навигация: ← Глава 5. Ординалы как процессы; башня сильных аксиом (ATR_0, ^1_1) и её снятие · Глава 1. Поле как роль-расширение; степень как ярус — Часть XI →

Footnotes

1. HigmanLemma.v: is_wqo, wqo_nat_le, dickson_pair, higman_unit, итог — higman_synthesis. 15 Qed, использует classic (L3). ↩

2. KruskalFull.v/KruskalTree.v: chain_wqo, fork_wqo, growing_wqo, depth1_wqo, итог — L5_from_kruskal. 15 Qed, 0 новых аксиом. ↩

3. CantorBendixsonFull.v: CB_deriv (удаление изолированных точек), CB_omega ($\omega$-предел); совершенное-или-пустое ядро, конечные множества рассеяны. 20 Qed, 0 аксиом. ↩

4. BorelDeterminacy.v: weak_determinacy, zero_game_determined. 15 Qed, 1 аксиома (classic). NB: вопреки имени файла, доказана именно конечная (цермеловская) детерминированность, а не борелевская (Мартина). ↩

5. settheory/ChoicePriceMap.v (эта работа): AxiomPrice (PZero/PL3/PL3_L4/PBoundary), функция price, и proven_results_below_boundary — каждый доказанный результат строго ниже границы. Это аудит-слой, фиксирующий сверенные Print Assumptions статусы, а не новая математика. ↩

6. foundation/ZFCAxiomLedger.v (9 Qed, 0 аксиом): машинный реестр-вердикт девяти аксиом ZFC — tos_verdict, eight_axioms_eliminated, only_powerset_is_role_limit; bitvectors_length ($|2^{[0,n)}|=2^n$, конечный powerset — Element). Реестр — синтез/классификация (вердикты цитируют существующие 0-аксиомные файлы), не новая теорема. Машинно проверено. ↩

7. Откат закреплён машинно (0 аксиом каждый): foundation/PowersetRoleType.v (powerset_card: $|\mathcal{P}(l)|=2^{|l|}$; cantor_bool_seq: нет сюръекции $\mathbb{N}\to (\mathbb{N}\to \mathtt{bool})$), foundation/FiniteGameDeterminacy.v (finite_game_determined, обратная индукция), foundation/FiniteWqoPigeonhole.v (конечное голубятное ядро wqo). Свод-вердикт — foundation/FormerWallsLedger.v (former_walls_are_artifacts, only_completed_infinity_is_a_wall): ровно завершённая бесконечность запрещена, три <<стены>> откатываются (ReachedFreely/NotYetBuilt). Конкретные свидетели — genuine; свод — синтез/классификация, не доказательство полных Крускала/Бореля. Машинно проверено. ↩