Каталог аксиом Diakrisis

Обзор

Полный нормативный каталог 13 аксиом Diakrisis. При расхождении с другими документами — каталог имеет приоритет.

Организация

• Формулировки: formal statement.
• Свойства: независимость, консистентность.
• Связи: с теоремами, сборками.
• Verum-статус: progress на формализацию.

Полный список (13 аксиом)

Axi-0 — непустотность

$\mathrm{Ob}(\llbracket\cdot\rrbracket) \neq \emptyset.$

Статус: [П]. Verum: базовая. Следствия: гарантирует нетривиальность теории.

Axi-1 — структура ⟪⟫

⟪⟫ — локально-малая 2-категория с внутренней замкнутостью (2-полностью-верное ι: End(⟪⟫) ↪ ⟪⟫).

Статус: [П]. Verum: в разработке (2-cat machinery). Следствия: основа всей структуры.

Axi-2 — 𝖬 как 2-функтор

𝖬: ⟪⟫ → ⟪⟫ — 2-функтор.

Статус: [П]. Verum: в разработке. Следствия: гарантирует functorial behavior 𝖬.

Axi-3 — α_math

α_math ∈ Ob(⟪⟫).

Статус: [П]. Verum: требует инстанциация. Следствия: основа для ρ.

Axi-4 — ρ через хом

ρ(α) := [α_math, α] ∈ End(⟪⟫).

Статус: [П]. Verum: в разработке (internal hom). Включает: accessibility 𝖬.

Axi-5 — ρ-нетривиальность

∃ α, β: ρ(α) ≇ ρ(β).

Статус: [П]. Verum: легко формализуется. Следствия: гарантирует различимость артикуляций.

Axi-6 — ρ и 𝖬 не перестановочны

ρ ∘ 𝖬 ≇ ρ в общем.

Статус: [П]. Verum: требует конкретного примера. Следствия: 𝖬 — содержательная операция.

Axi-7 (M-5w) — самоартикулируемость

∃ α_𝖬: ρ(α_𝖬)[ρ(β)] ≃ ρ(𝖬(β)).

Статус: [П]. Verum: в разработке. Связь: эквивалент T-96 в α_uhm (04.T2).

Axi-8 (M-5w*) — нетривиальность

α_𝖬 не Ёнеда-представим (критерий; в Cat-модели нарушается, но в не-LP возможна выполнимость).

Статус: [П] (в сильной форме часто нарушается). Verum: сложная формализация. Замечание: часть AFN-T — о ограничениях этой аксиомы.

Axi-9 — достаточность

∀ осмысленная конфигурация C: ∃ α_C, реализующая C.

Статус: [П]. Verum: требует формализации «осмысленности». Следствия: богатство ⟪⟫.

T-α — непривилегированность α_math

Канонический (позитивный) вариант: ∃ γ ∈ Ob(⟪⟫): γ ⊄_0 α_math.

Классический эквивалент (через двойное отрицание, работает при LEM): ¬(∀γ ∈ Ob(⟪⟫), γ ⊏_0 α_math).

Конструктивный вариант T-α_c: то же самое, но с конструктивным доказательством существования γ — необходим для интуиционистских gauge-классов (α_hott, α_cic, α_int).

Статус: [П]. Verum: легко формализуется в обоих вариантах. Следствия: gauge-свобода; совместимость с классическими и конструктивными gauge-классами.

Детальная спецификация мета-логики: /02-canonical-primitive/02-axiomatics#t-alpha-spec.

T-2f* — локально-стратифицированная комплетация

Выделение α_P по предикату P допустимо ⇔ все вхождения 𝖬, ⊏_• в P имеют меньшую глубину, чем α_P.

Статус: [П]. Verum: требует глубинной машинерии. Следствия: Рассел-иммунитет.

Свойства аксиоматики

Независимость

21.T2: каждая аксиома независима.

Детализация

Для каждой пары (Axi-i, Axi-j), i ≠ j:

• Существует модель, удовлетворяющая Axi-i, но не Axi-j.
• Следовательно, Axi-i не выводится из остальных.

Подробности — .

Консистентность

10.T1: есть модель в Cat. Относительно ZFC + 2 инаксессибальных.

Модель

• ⟪⟫ = Cat (2-категория малых категорий).
• 𝖬 = specific accessible endofunctor.
• α_math = specific малая категория.
• Все аксиомы (кроме Axi-8 в сильной форме) удовлетворяются.

Рассел-иммунитет

10.T2, 18.T: пять именных семейств парадоксов заблокированы T-2f*.

105.T (/06-limits/10-maximality-theorems): универсальная иммунность — T-2f* блокирует любой Яновский-сводимый самореферентный парадокс (Яновский 2003), а не только именные 5 семейств. Ключ: $\mathrm{dp}(T^Y) = \mathrm{dp}(Y)+1$ — экспоненциал на один depth выше; слабая точечная сюръективность требует depth-сохранения; T-2f* строгое неравенство → w.p.s. невозможно → все диагональные парадоксы заблокированы.

Именные семьи парадоксов (частные случаи Яновский)

1. Рассел: {x : x ∉ x}.
2. Curry: (X → ⊥) ∈ X.
3. Grelling: heterologicality.
4. Burali-Forti: класс всех ординалов.
5. Жирар Type:Type: Type ∈ Type.
6. Через 105.T: также Кантор, Тарский, Ловер, Гёдель-type, Löb, и любой другой Яновский-сводимый парадокс.

Все — заблокированы.

Связь с ZFC

31.C1: |Diakrisis_полная| = |ZFC + 2 inacc|.

Детализация

• Diakrisis_базовая (без полного Trace): ZFC + 1 inaccessible.
• Diakrisis_полная (с 𝓜_Fnd): ZFC + 2 inaccessibles.
• Diakrisis в (∞,1)-обобщении: больше inaccessibles.

Минимальность

13 аксиом — минимальный набор: каждая независима (21.T2), ни одна не выводится из остальных.

Что не является аксиомой (а теоремой): рефлексивность 𝖠 (теорема из Axi-0..Axi-2), самоартикуляция (10.T3), неполнота α_math (10.T4), существование Fix(𝖬) (10.T5) — все выводятся из 13.

Группировка аксиом

Базовые (Axi-0..Axi-3)

Обеспечивают существование и базовую структуру.

Реализация (Axi-4..Axi-6)

Вводят ρ и его поведение.

Самоартикулируемость (Axi-7..Axi-9)

Связывают 𝖬 с ⟪⟫ и обеспечивают достаточность.

Структурные (T-α, T-2f*)

Тонкие структурные ограничения.

Связь с другими теориями

С ZFC

• Diakrisis не ZFC: structurally different.
• Консистентность: relative (ZFC + 2 inacc).
• Морита: через gauge (α_zfc ∈ 𝓜_Fnd).

С HoTT

• Diakrisis не HoTT: разные подходы.
• Морита: α_hott ∈ 𝓜_Fnd.
• Унивалентность: соответствует gauge-симметрии.

С NCG

• Diakrisis включает NCG как α_ncg.
• α_uhm расширяет α_ncg.

Verum-готовность

Аксиома	Verum-статус
Axi-0	Легко
Axi-1	Сложно (2-cat)
Axi-2	Средне
Axi-3	Легко
Axi-4	Средне
Axi-5	Легко
Axi-6	Средне
Axi-7	Сложно
Axi-8	Очень сложно
Axi-9	Сложно (описание «осмысленности»)
T-α	Легко
T-2f*	Сложно

Дуальная аксиоматика Актика (A-0..A-9 + T-ε + T-2a* + T-ε_c)

Полный параллельный список для ДЦ-примитива Актика. Каждая аксиома — структурный дуал соответствующей ОЦ-аксиомы. Канонический источник формулировок — /12-actic/02-dual-primitive §2; настоящий каталог — нормативная транскрипция.

A-0 — непустотность актов

$\mathrm{Ob}(\rangle\!\rangle \cdot \langle\!\langle) \neq \emptyset \wedge \varepsilon_\mathrm{math} \in \mathrm{Ob}(\rangle\!\rangle \cdot \langle\!\langle)$.

Дуал: Axi-0. Статус: [П].

A-1 — 2-категорная структура ⟫·⟪

$\rangle\!\rangle \cdot \langle\!\langle$ — локально-малая 2-категория с 2-полностью-верным $\iota^\mathrm{act}: \mathrm{End}(\rangle\!\rangle \cdot \langle\!\langle) \hookrightarrow \rangle\!\rangle \cdot \langle\!\langle$.

Дуал: Axi-1. Статус: [П].

A-2 — $\mathsf{A}$ как accessible 2-функтор

$\mathsf{A}: \rangle\!\rangle \cdot \langle\!\langle \to \rangle\!\rangle \cdot \langle\!\langle$ — accessible endo-2-функтор (активация).

Дуал: Axi-2. Статус: [П]. Следствия: существование трансфинитных итераций $\mathsf{A}^\kappa$.

A-3 — выделенный $\varepsilon_\mathrm{math}$

$\varepsilon_\mathrm{math} \in \mathrm{Ob}(\rangle\!\rangle \cdot \langle\!\langle)$ — начальный в подкатегории «подготавливаемых» актов.

Дуал: Axi-3. Статус: [П].

A-4 — $\rho^\mathrm{act}$ через внутренний act-хом

$\rho^\mathrm{act}(\varepsilon) = [\varepsilon_\mathrm{math}, \varepsilon]^\mathrm{act}$.

Дуал: Axi-4. Статус: [П].

A-5 — $\rho^\mathrm{act}$-нетривиальность

$\rho^\mathrm{act}(\varepsilon_1) \simeq \rho^\mathrm{act}(\varepsilon_2) \Rightarrow \varepsilon_1 \simeq \varepsilon_2$.

Дуал: Axi-5. Статус: [П].

A-6 — $\rho^\mathrm{act}$ и $\mathsf{A}$ не перестановочны

$\rho^\mathrm{act} \circ \mathsf{A} \not\cong \rho^\mathrm{act}$ в общем случае.

Дуал: Axi-6. Статус: [П].

A-7 — самоактивируемость ($\mathsf{A}$-5w)

$\varepsilon_\mathsf{A} := \iota^\mathrm{act}(\mathsf{A}) \in \rangle\!\rangle \cdot \langle\!\langle$ — акт «активировать $\mathsf{A}$» сам является объектом $\rangle\!\rangle \cdot \langle\!\langle$; $\rho^\mathrm{act}$ корректно определено на нём, и существует естественное преобразование

$$\rho^\mathrm{act}(\varepsilon_\mathsf{A} \circ \varepsilon) \Rightarrow \mathsf{A}(\rho^\mathrm{act}(\varepsilon)).$$

Дуал: Axi-7. Статус: [П].

A-8 ($\mathsf{A}$-5w*) — критерий нетривиальности $\mathsf{A}$

Строже чем A-7: преобразование A-7 — не всегда изо. Это гарантирует, что $\mathsf{A}$ действительно «активна» (не Ёнеда-представима).

Дуал: Axi-8. Статус: [П].

A-9 — достаточность актов для формализации

$\rangle\!\rangle \cdot \langle\!\langle$ содержит достаточно актов для покрытия всех Rich-метатеорий $S \in \RS$: для каждой $S$ существует $\varepsilon_S$ — акт-перформанс $S$.

Дуал: Axi-9. Статус: [П].

T-ε — не-привилегированность $\varepsilon_\mathrm{math}$

Дуал T-α. Для любого акта $\varepsilon \in \rangle\!\rangle \cdot \langle\!\langle$ с $\nu(\varepsilon) = \nu(\varepsilon_\mathrm{math})$ существует автоморфизм $\sigma \in \mathrm{Aut}_2(\rangle\!\rangle \cdot \langle\!\langle)$ с $\sigma(\varepsilon_\mathrm{math}) = \varepsilon$. Математика-как-практика не привилегирована per se; она — представитель класса актов той же ε-глубины.

Дуал: T-α. Статус: [П].

T-2a* — активационно-стратифицированная комплетация

Ключевая аксиома защиты от парадоксов. Выделение $\varepsilon_P$ по предикату $P$ допустимо ⟺ все вхождения $\mathsf{A}, \sqsupset_\bullet$ в $P$ имеют строго меньшую активационную глубину, чем $\varepsilon_P$.

Дуал: T-2f*. Статус: [П]. Следствия: блокирует пять семейств actic-парадоксов (Рассел-act, Curry-act, Grelling-act, Burali-Forti-act, Жирар-act); универсальное обобщение через Яновский-reducibility (113.T).

T-ε_c — конструктивный gauge-инвариант актов

Дуал T-α_c. В конструктивных R-S gauge-орбита $\varepsilon$ сохраняет constructive content: если $\varepsilon_1 \sim_\mathrm{gauge} \varepsilon_2$ и $\varepsilon_1$ конструктивен, то $\varepsilon_2$ конструктивен.

Дуал: T-α_c. Статус: [П].

Verum-готовность Актика-аксиом

Аксиома	Verum-статус
A-0	Легко
A-1	Сложно (2-cat)
A-2	Средне (accessibility)
A-3	Легко
A-4	Средне (act-hom)
A-5	Легко
A-6	Средне
A-7	Сложно
A-8	Очень сложно
A-9	Сложно
T-ε	Легко
T-2a*	Сложно
T-ε_c	Средне

Следующий документ

/10-reference/02-theorems-catalog.