Глава 5. Ординалы как процессы; башня сильных аксиом (ATR_0, ^1_1) и её снятие

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

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

Предупреждение о масштабе утверждений

Эта глава — самая тонкая в Части X, и её надо читать с точной мерой. Когда мы говорим, что P4 «снимает» ATR${}_0$ или ${\Pi }_1^1$, речь идёт о P4-переинтерпретации: о прочтении, делающем сильный принцип ненужным внутри P4-развития. Это не метатеорема обратной математики (reverse mathematics): ToS не доказывает разделения RM-иерархии, не доказывает недоказуемость ATR${}_0$/${\Pi }_1^1$ в более слабых системах и не переопределяет эти принципы как формальные теоремы. Утверждается строго следующее: допустимая работа каждого принципа выполняется конкретным P4-приёмом (структурной рекурсией по ординальным нотациям; отождествлением функции с программным кодом), а его завершённо-объектная форма (рекурсия по произвольному завершённому вполне-порядку; квантификация по завершённому несчётному пространству всех функций) к P4-развитию не привлекается. Этот масштаб удерживается до конца главы.

Ординал — роль-процесс; башня сильных аксиом получает тот же двухуровневый диагноз, что и выбор. «Снятие» ATR${}_0$/${\Pi }_1^1$ — это P4-переинтерпретация (приём, делающий принцип ненужным), а не метатеорема обратной математики.

Ординалы как процессы

В ToS ординал задан индуктивно: ноль, успешник и предел процесса — $\mathrm{OLim}f$ для $f:N\to \mathrm{Ord}$. Именно последний конструктор делает ординал процессным: $\mathrm{OLim}f$ несёт роль «взять предел процесса $f$, ступающего по натуральным стадиям». Так $\omega =\mathrm{OLim}$ от вложения $N\hookrightarrow \mathrm{Ord}$, а ${\epsilon }_0=\mathrm{OLim}$ от башни $\omega ,{\omega }^{\omega },{\omega }^{{\omega }^{\omega }},\dots$ — предел процесса возведения в степень.¹ На каждой стадии $n$ актуально лишь конечное (${\mathrm{OSucc}}^n(\mathrm{OZero})$); сам ординал — не завершённый трансфинитный объект, а позиция в фундированном процессе.

Это даёт трансфинитную индукцию и рекурсию по нотациям — без аксиом. Отношение $\mathrm{or}{\mathrm{d}}_{\mathrm{l}}\mathrm{t}$ фундировано, и из этого следуют принципы индукции вплоть до $\omega$, башни и ${\epsilon }_0$.² Подчеркнём область: это индукция/рекурсия по конструктивным ординальным нотациям Ord, а не по произвольному завершённому вполне-порядку.

Ординал — роль-процесс ($\mathrm{OLim}$ — предел процесса; ${\epsilon }_0$ — предел башни); трансфинитная индукция по конструктивным нотациям структурна и 0-аксиомна. Завершённый трансфинитный объект — вне Элементов.

ATR${}_0$: трансфинитная рекурсия как структурная

Арифметическая трансфинитная рекурсия (ATR${}_0$) — одна из «большой пятёрки» аксиом обратной математики: она постулирует возможность итерировать арифметическую операцию вдоль вполне-порядка. В ToS соответствующая работа — итерация операции вдоль конструктивной ординальной нотации — есть просто Fixpoint по индуктивному типу Ord: проверяющий завершаемость Rocq принимает рекурсию по структуре $\alpha$, и никакой аксиомы не нужно.³

Точная мера (см. §10.5.1). Сказанное относится к рекурсии вдоль нотаций Ord: для них ATR${}_0$-как-аксиома не требуется, её заменяет структурная рекурсия. Это не утверждение о полной ATR${}_0$ над всеми завершёнными вполне-порядками и не RM-разделение. В терминах главы: допустимое ядро (рекурсия вдоль конструктивных нотаций) — структурная рекурсия (Правило); завершённо-объектная форма (рекурсия по произвольному завершённому вполне-порядку как готовому объекту) к P4-развитию не привлекается.

ATR${}_0$ — роль-смешение: законная итерация вдоль нотаций (структурный Fixpoint, 0 аксиом) склеена с завершённой рекурсией по произвольному вполне-порядку. ToS переинтерпретирует первое, второе не привлекает — не доказывая RM-метатеорем.

${\Pi }_1^1$: второй порядок как первый порядок по кодам

${\Pi }_1^1$-свёртывание — вершина «большой пятёрки»: оно утверждает, что $\{n\mid \forall f,\phi (n,f)\}$ есть множество, когда $\phi$ арифметична. Загвоздка — квантор $\forall f$ по всем функциям $N\to N$, что классически означает пробег по несчётному завершённому пространству. В ToS ход иной: при P4 всякая функция есть процесс, заданный программным кодом; тогда «$\forall f$» сводится к «$\forall c:N$» по кодам — второй порядок прочитывается как первый.⁴

Здесь нужна особая осторожность — это самый тонкий пункт. «Снятие» ${\Pi }_1^1$ идёт через отождествление функции с программным кодом ($\forall f\mapsto \forall c:N$). Это конкретный P4-выбор онтологии (функция$=$процесс$=$код), переинтерпретирующий второпорядковую квантификацию как первопорядковую по кодам. Это не метатеорема о ${\Pi }_1^1$-CA${}_0$ и не RM-разделение. Допустимое прочтение (квантор по функциям, заданным кодами) — первопорядковое; завершённо-объектная форма (квантор по завершённой несчётной тотальности всех функций) к P4-развитию не привлекается — это ровно тот завершённый объект, который P4 не актуализирует.

${\Pi }_1^1$ — роль-смешение: квантор по кодам-функциям (первый порядок) склеен с квантором по завершённому несчётному пространству всех функций. P4-переинтерпретация берёт первое (функция$=$код), второе не привлекает; это онтологический выбор, не RM-метатеорема.

Бесконечность, импредикативность; башня как одна структура

Те же два уровня видны в двух нижних этажах башни. Бесконечность: ToS не берёт завершённое бесконечное множество как Элемент, но удерживает бесконечность как схему процесса — потенциальную, в духе сходящихся приближений.⁵ Импредикативность: определение $R=\{x\mid x\notin x\}$ квантует по тотальности, включающей само себя; P1 (иерархия) и P4 (конечность) его растворяют — это расселов случай Главы 10.1, теперь как импредикативное свёртывание.⁶

Так вся башня — выбор, бесконечность, импредикативность, ATR${}_0$, ${\Pi }_1^1$ — получает один диагноз. Каждый сильный принцип склеивает законное прочтение (правило L5; процесс; структурная рекурсия; квантор по кодам) с незаконной завершённо-объектной формой (граф выбора; завершённая бесконечность; тотальность-в-себе; рекурсия по готовому вполне-порядку; несчётное пространство всех функций). P4 сохраняет первое и не привлекает второе. Это и есть единая структура Части X.

Бесконечность — процесс, не завершённый объект; импредикативность растворяется P1$+$P4. Вся башня — одно роль-смешение законного прочтения и завершённого объекта; P4 держит первое, отводит второе.

E/R/R-разбор и честная карта

Слой	Содержание
Rules (L5)	структурная рекурсия по Ord; отождествление функция$=$код ($\forall f\mapsto \forall c$); схема процесса для бесконечности; уровневый порядок P1
Roles (L4)	ординал$=$роль-процесс; ${\epsilon }_0=$предел башни; «снятие принципа»$=$роль P4-переинтерпретации (не RM-метатеорема)
Elements (L1$+$P4)	конечная нотация/код/стадия на каждом шаге; завершённый трансфинит, завершённый вполне-порядок и несчётное пространство всех функций Элементами не являются

{ Что даёт. Трансфинитная индукция/рекурсия по нотациям — wf_ord_lt, transfinite_ind (0 аксиом). ATR${}_0$/${\Pi }_1^1$/Бесконечность/импредикативность — переинтерпретированы (P4_eliminates_ATR0, P4_eliminates_Pi11, P4_eliminates_Infinity, P4ProhibitsImpredicative; ATR/Бесконечность/импредикативность 0 аксиом, ${\Pi }_1^1$ — 0 логических аксиом при примитиве eval_program).}

Диагностика. В P4-онтологии ToS сильный принцип — склейка законного прочтения и завершённо-объектной формы; P4 расклеивает их.

Честные границы (главное). «Снятие» ATR${}_0$/${\Pi }_1^1$ — это P4-переинтерпретация, не метатеорема обратной математики: нет ни RM-разделений, ни доказательства недоказуемости в слабых системах. Рекурсия — по конструктивным нотациям Ord, не по всем вполне-порядкам. ${\Pi }_1^1$ снят отождествлением функции с кодом — онтологический выбор, а не теорема о ${\Pi }_1^1$-CA${}_0$. Для ATR${}_0$ и ${\Pi }_1^1$ завершённые формы (произвольный вполне-порядок, несчётное пространство функций) не опровергаются как RM-принципы, а не привлекаются в P4-развитии; для завершённой бесконечности и импредикативной тотальности действует более сильный P4/P1-запрет object-формы (Главы 10.4, 10.1).

Ординалы — процессы; башня сильных аксиом получает единый двухуровневый диагноз. Каждое «снятие» — P4-переинтерпретация законного ядра (структурная рекурсия, функция$=$код, процесс), а не метатеорема обратной математики; завершённые формы не привлекаются, а не опровергаются.

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

Ординалы оказались процессами: $\mathrm{OLim}$ — предел процесса, ${\epsilon }_0$ — предел башни, а трансфинитная индукция по конструктивным нотациям структурна и 0-аксиомна (wf_ord_lt, transfinite_ind). Башня сильных аксиом над выбором получила тот же двухуровневый разбор, что и сам выбор в 10.4: ATR${}_0$ — структурная рекурсия по нотациям (P4_eliminates_ATR0); ${\Pi }_1^1$ — второй порядок как первый по кодам (P4_eliminates_Pi11); Бесконечность — схема процесса (P4_eliminates_Infinity); импредикативность — растворена P1$+$P4. И всё это — честно — P4-переинтерпретации, а не метатеоремы обратной математики.

Глава 10.6 соберёт Часть X: что доказуемо без выбора (включая WQO-результаты Хигмана и Крускала для конкретных семейств и конечную детерминированность игр), полную карту аксиомных цен и честную «стену» — полную теорему Крускала, борелевскую детерминированность, метатеоретическую независимость, — куда ToS не заходит.

Ординал есть роль-процесс, а не завершённый трансфинит; вся башня оснований над выбором читается единым двухуровневым диагнозом — законное ядро переинтерпретируется, завершённый объект не привлекается. С точной мерой: это P4-прочтение, а не теоремы обратной математики.

---

---

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

Навигация: ← Глава 4. Аксиома выбора: запрет и переинтерпретация · Глава 6. Синтез Части X: что доказуемо без выбора, и карта границ →

Footnotes

1. Ordinal.v: Ord (с OZero/OSucc/OLim), omega $=\mathrm{OLim}‘na{t}_t{o}_{o}rd‘$, epsilon_0 $=\mathrm{OLim}‘omeg{a}_{t}ower‘$ — сверено Print Assumptions: Closed, 0 аксиом. Арифметика ($+,\cdot ,{}^{\wedge }$) — структурной рекурсией, но часть её лемм опирается на функциональную экстенсиональность. ↩

2. TransfiniteInduction.v: wf_ord_lt (well_founded ord_lt), transfinite_ind, transfinite_rec; omega_tower_induction. 0 аксиом (сверено Print Assumptions: wf_ord_lt и transfinite_ind закрыты — вопреки устаревшему комментарию в шапке файла, который ошибочно называет classic; источника этих аксиом файл даже не импортирует). Дополнительно индукция по уровневой иерархии — level_strong_induction в TransfiniteInductionLevel.v (эта работа). ↩

3. P4_Eliminates_ATR.v: CB_transfinite — трансфинитная итерация (производная Кантора–Бендиксона) как Fixpoint на Ord; P4_eliminates_ATR0 фиксирует zero/successor-уравнения рекурсии (limit-стадия задана самим Fixpoint). 15 Qed, 0 аксиом (сверено Print Assumptions: Closed). ↩

4. P4_Eliminates_Pi11.v: Program := nat, P4_forall_functions (квантор по функциям через коды), итог — P4_eliminates_Pi11. По Print Assumptions — 0 логических аксиом, но зависит от eval_program (Parameter — вычислительный примитив универсальной машины); это и есть P4-кодовая переинтерпретация, а не построение пространства программ изнутри. ↩

5. P4_Eliminates_Infinity.v: converges (сходимость приближений), итог — P4_eliminates_Infinity. 12 Qed, 0 аксиом. Ср. 10.4: потенциальная бесконечность с P4 совместима, завершённая — нет. ↩

6. P4ProhibitsImpredicative.v: P1$+$P4 исключают завершённую тотальность, по которой идёт импредикативное определение. 10 Qed, 0 аксиом. ↩