Кардинальный анализ
Статус
[Т] — кардинальный анализ через 23.T1-T2 + 90.T (Con = ZFC + 2 inacc) полностью установлен.
Вопрос
Каковы размерные характеристики ⟪⟫?
Значение вопроса
Размерные характеристики определяют:
- Консистентность относительно ZFC + дополнений.
- Возможность Verum-формализации.
- Связь с large cardinal hierarchy.
- Ограничения на работу с пределами и классифицирующими пространствами.
Ответ
Ob(⟪⟫) — проперный класс
Trace(𝖠) для полного развертывания — собственный класс в ZFC. Не множество.
Почему проперный класс
- Trace(𝖠) содержит артикуляции 𝖬^κ(α_0) для всех ординалов κ.
- Ординалы образуют проперный класс Ord.
- Следовательно, Trace — проперный класс.
Следствия
- Работа с Trace требует NBG или class-theoretic расширения ZFC.
- Ob(⟪⟫) ⊇ Trace, значит Ob(⟪⟫) — тоже проперный класс.
- Классифицирующее пространство 𝓜_Fnd — проперный класс (но факторизация по gauge может уменьшить).
Локально-малая
Для α, β: Hom(α, β) — множество. Это требование Axi-1.
Почему важна локальная малость
- Применимость стандартной теории: позволяет использовать стандартные результаты о малых категориях.
- Избежание парадоксов: при глобально-больших Hom возникают проблемы размера.
- Практическая работа: можно «вычислять» в Hom-множествах.
Компромисс
- Ob большой + Hom маленькие: стандартное решение.
- Альтернативы: полностью большие категории — возникают технические сложности.
Требования к основаниям
Для стандартной работы Diakrisis требуется:
- ZFC + 1 инаксессибальный кардинал — базовая теория.
- ZFC + 2 инаксессибальных — для α_Apeiron и рефлексивной замкнутости.
31.C1: |Diakrisis_базовая| = |ZFC + 1 inacc|, |Diakrisis_полная| = |ZFC + 2 inacc|.
Зачем инаксессибальные
- Первый инаксессибальный κ_1: ограничивает «малые» артикуляции. Гротендик universe V_{κ_1}.
- Второй инаксессибальный κ_2: ограничивает «большие» артикуляции + включает Trace(𝖠).
- α_Apeiron (самоприменение 𝖠): требует сильных кардиналов для консистентной формализации.
Сравнение с другими основаниями
| Основание | Кардинальные требования |
|---|---|
| ZFC | — (без дополнений) |
| ZFC + Universes | 1 inaccessible |
| Morse-Kelley (NBG-like) | 1 inaccessible (неявно) |
| ∞-topoi (Люри) | 2 inaccessibles |
| Diakrisis (полная) | 2 inaccessibles |
| Higher topos theory | Много inaccessibles |
Diakrisis — сравнимо с ∞-topos theory по сила консистентности.
Стратификация глубины
23.T1: артикуляции стратифицированы по ν (глубина от α_0):
- Малые (элементы 𝒰): ν < κ_1 инаксессибальный.
- Большие (элементы 𝒰_1 \ 𝒰_0): κ_1 ≤ ν < κ_2.
- Проперные классы: ν ≥ κ_2.
Роль стратификации
- Блокировка парадоксов: T-2f* использует стратификацию.
- Управление размером: ограничения на применение 𝖬.
- Практическая работа: большинство работы — с малыми артикуляциями.
Пример стратификации
- α_0 := малая категория. ν(α_0) = 0.
- 𝖬(α_0) = эндо-функтор на α_0. ν = 1.
- 𝖬²(α_0) = эндо-функтор на 𝖬(α_0). ν = 2.
- ...
- 𝖬^ω(α_0) — счётный предел. ν = ω.
- 𝖬^{ω_1}(α_0) — требует κ_1. ν = ω_1.
Уточнение стратификации
| Ранг ν | Размер | Пример |
|---|---|---|
| 0..ω | конечные | малые категории |
| ω..ω_1 | счётные пределы | счётный колимит |
| ω_1..κ_1 | меньше инаксессибального | стандартные LP-категории |
| κ_1..κ_2 | между двумя инаксессибалами | 𝓜_Fnd |
| ≥ κ_2 | проперный класс | полный Trace(𝖠) |
LP-статус
По 14.T2: если ⟪⟫ не locally presentable, 𝖬 не представим; α_𝖬 активна.
В Cat-модели: ⟪⟫ = Cat — LP → α_𝖬 пассивна.
В не-LP моделях — возможна активность. Но не-LP модели требуют специфических условий.
Определение LP
Locally presentable (LP) category (Адамек-Росицкий, 1994):
- Существует регулярный кардинал λ такой, что:
- Каждый объект представим как λ-filtered colimit λ-presentable objects.
- Имеется достаточно λ-presentable objects.
Следствия LP
- Стандартная теория accessible functors (Адамек-Росицкий).
- Существование инициальных/финальных алгебр.
- Ёнеда-представимость большинства endofunctors.
Не-LP модели
- Large categories: без LP-структуры.
- Paradoxical структуры (например, full subcategory of Set).
- Non-standard constructions: используют специфические условия.
Работа в не-LP — открытая программа в Diakrisis.
Verum-формализация
Для формализации в Verum требуется:
- Proof-assistant с поддержкой trans-finite induction.
- Гротендик-universes (или эквивалент).
Verum в стадии активной разработки.
Технические требования
- Universe hierarchy: Verum должен поддерживать иерархию universes (V_0 ∈ V_1 ∈ V_2 ∈ ...).
- Trans-finite induction: для итераций 𝖬^κ.
- 2-categorical rewriting: для работы с 2-морфизмами.
- Accessibility proofs: для Адамек-Росицкий теорем.
Альтернативы
- Lean 4: поддерживает большинство требований; может использоваться как запасной.
- Coq: поддерживает universes, но 2-категорная работа сложна.
- Agda: хорош для HoTT, менее удобен для 2-категорий.
Предпочтение: Verum (специализация под УГМ); Lean 4 — запасной.
Статус Verum
- Активно разрабатывается командой УГМ.
- Базовая функциональность: доступна.
- Поддержка 2-категорной работы: в разработке.
- Полная поддержка Diakrisis: программа Пути Б.
Признанные редукции
- Кардинальный анализ — стандартный ZFC + инаксессибалы.
- Стратификация — известна из NBG.
Детализация
| Наш элемент | Редукция | Источник |
|---|---|---|
| Ob как proper class | Standard NBG | Bernays-Гёдель |
| Inaccessible cardinals | Classical large cardinals | Kanamori |
| Гротендик universes | SGA 4 | Гротендик |
| Stratification | Рассел-style types | Рассел 1908 |
| LP theory | Адамек-Росицкий 1994 | — |
| Accessibility | Standard | Folklore |
Всё — стандартный арсенал современной мат-логики.
Следствия кардинального анализа
Для консистентности
- Diakrisis консистентен относительно ZFC + 2 inaccessibles.
- Без inaccessibles — некоторые теоремы (например, 29.T) могут не работать.
Для применимости
- Большинство теорем работают в ZFC + 1 inaccessible.
- Только самые «глобальные» (Trace(𝖠), 𝓜_Fnd) требуют 2 inaccessibles.
Для Verum
- Проверка в Verum требует соответствующих универсов.
- Современные прувер-системы поддерживают это.
Альтернативные формализмы
Class-based set theory
- Morse-Kelley, NBG.
- Проперные классы — first-class objects.
- Удобно для работы с Ob(⟪⟫).
Type theory with universes
- MLTT, CIC, HoTT.
- Иерархия типов U_0 : U_1 : U_2 : ...
- Аналог иерархии universes в ZFC.
(∞,1)-categories
- Люри HTT.
- Работа «в пределе» без эксплицитных кардиналов.
- Концептуально чище, технически сложнее.
Вопросы открытой работы
- Q: существует ли «минимальная» модель Diakrisis (в смысле сила консистентности)?
- Q: можно ли обойтись одним inaccessible для полной теории (при определённых упрощениях)?
- Q: что даёт переход к (∞,1)-категорной формулировке?
- Q: связь с large cardinal hierarchy выше inaccessibles?
Это — программа формализации, относящаяся к Пути Б.