Аксиоматика канонического примитива

Статус

[О] — определения + обоснования.

Обзор аксиоматики

13 формальных условий, определяющих канонический примитив Diakrisis. По П-0.2 (экономия аксиом) — минимально необходимый набор. Дополнительные свойства, которые можно вывести из этих 13, не постулируются как аксиомы.

Структура аксиом

Аксиомы делятся на четыре группы:

• Базовые (Axi-0..Axi-3): существование и базовая структура примитивов.
• Реализация (Axi-4..Axi-9): связь примитивов через ρ и 𝖬.
• Структурные (T-α, T-2f*): тонкие структурные ограничения.

Каждая группа — разная роль в построении теории.

Общая стратегия выбора

• Минимум постулатов: по П-0.2.
• Максимум теорем: из 13 постулатов выводится ~200 теорем Diakrisis.
• Чёткое разграничение: аксиомы ≠ определения ≠ теоремы.
• Проверка на независимость: каждая аксиома необходима.
• Проверка на консистентность: вся система имеет модель в Cat.

13 формальных условий

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

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

Существует хотя бы одна артикуляция.

Обоснование

• Без Axi-0 ⟪⟫ могло бы быть пустой категорией. Тогда теория была бы тривиальна (все универсальные утверждения вырождены).
• Феноменологически: если есть акт различения, значит есть по крайней мере одна артикуляция (её след).
• Минимум: одна артикуляция α_0.

Следствия

• Любое доказательство может опираться на существование некоторой α ∈ ⟪⟫.
• Axi-3 (существование α_math) — усиление Axi-0.

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

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

Обоснование

• Локальная малость: чтобы Hom-множества были множествами (а не классами), мы могли работать с ⟪⟫ в стандартной ZFC-мета-теории.
• 2-категория: минимальная структура, удерживающая 2-морфизмы (необходимо для gauge).
• Внутренняя замкнутость: ключевая особенность, выделяющая Diakrisis от стандартных 2-категорий. Позволяет говорить о «эндо-операциях как объектах».

Следствия

• ⟪⟫ имеет все стандартные свойства 2-категорий (ассоциативность, идентичности).
• End(⟪⟫) — тоже 2-категория.
• ι(End(⟪⟫)) ⊆ ⟪⟫ — подкатегория, состоящая из представителей эндо-функторов.

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

$\mathsf{M}: \llbracket\cdot\rrbracket \to \llbracket\cdot\rrbracket$

— 2-функтор (сохраняет 1-морфизмы и 2-морфизмы до когерентных 2-изоморфизмов).

Обоснование

• 𝖬 — операция «говорения об артикуляции»; это должен быть функтор (переводит морфизмы в морфизмы).
• 2-функториальность необходима для gauge (иначе gauge-преобразования не коммутируют с 𝖬).
• Accessibility 𝖬 (требование для trans-конечных итераций) — часть Axi-2 в расширенной форме.

Следствия

• 𝖬 определён для всех α, f, φ.
• Итерации 𝖬^κ корректно определены по трансфинитной индукции.
• По Axi-1, 𝖬 ∈ End(⟪⟫), и значит имеет представителя α_𝖬 = ι(𝖬) ∈ ⟪⟫.

Axi-3 — выделенный α_math

$\alpha_{math} \in \mathrm{Ob}(\llbracket\cdot\rrbracket).$

Обоснование

• Нужна конкретная линза для ρ-реализации. Без α_math — ρ не определено.
• Выбор α_math — часть структуры (разные α_math — разные примитивы).
• α_math — это не просто «какой-то объект», а выделенный (фиксированный).

Следствия

• ρ корректно определено (через Axi-4).
• Разные примитивы отличаются выбором α_math.

Axi-4 — ρ через внутренний хом

$\rho(\alpha) := \mathrm{ev}_{\alpha_{math}}(\alpha) = [\alpha_{math}, \alpha] \in \mathrm{End}(\llbracket\cdot\rrbracket).$

ρ — эндо-операция, полученная через внутренний хом с α_math.

Обоснование

• Внутренний хом [α_math, ·] — стандартная конструкция в закрытой 2-категории.
• ρ превращает α в эндо-операцию, которую можно применять к другим объектам.
• Это — способ реализации артикуляции как «действия».

Следствия

• ρ(α) ∈ End(⟪⟫).
• По Axi-1, ρ(α) представим в ⟪⟫ через ι.
• ρ — функториален (переводит морфизмы α → β в естественные преобразования ρ(α) ⟹ ρ(β)).

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

$\exists \alpha, \beta \in \mathrm{Ob}(\llbracket\cdot\rrbracket): \rho(\alpha) \not\simeq \rho(\beta).$

Обоснование

• Без Axi-5 все ρ(α) были бы эквивалентны; ρ не различало бы артикуляции.
• Минимум нетривиальности: хотя бы две различимые ρ-реализации.
• В большинстве моделей (включая α_zfc, α_hott, α_uhm) — естественно удовлетворяется.

Следствия

• ρ — нетривиальная функция.
• ⟪⟫ содержит различимые артикуляции.

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

$\rho \circ \mathsf{M} \not\simeq \rho \quad \text{в общем}.$

Обоснование

• Без Axi-6, ρ(𝖬(α)) ≃ ρ(α) всегда — и тогда 𝖬 «невидима» через ρ.
• Axi-6 гарантирует, что 𝖬 — содержательная операция, которую ρ различает.
• «В общем» означает: существует α, для которого ρ(𝖬(α)) ≇ ρ(α).

Следствия

• 𝖬-итерации создают различные артикуляции (в ρ-проекции).
• Trace(𝖠) — нетривиальная последовательность.

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

$\exists \alpha_{\mathsf{M}} \in \mathrm{Ob}(\llbracket\cdot\rrbracket): \forall \beta,\; \rho(\alpha_{\mathsf{M}})[\rho(\beta)] \simeq \rho(\mathsf{M}(\beta)).$

Существует артикуляция, представляющая 𝖬.

Обоснование

• Axi-1 гарантирует существование представителя ι(𝖬) = α_𝖬.
• Axi-7 — более сильное: представитель α_𝖬 правильно взаимодействует с ρ через композицию.
• Это — самоприменение: α_𝖬, применённая через ρ, даёт тот же результат, что 𝖬.

Следствия

• α_𝖬 — «категорно-представитель» 𝖬 в ⟪⟫.
• Связь между 𝖬 (оператор) и α_𝖬 (объект) формализована.

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

$\neg \exists \alpha: \rho(\alpha_{\mathsf{M}})(-) \simeq \mathrm{Hom}_{\llbracket\cdot\rrbracket}(-, \alpha).$

α_𝖬 не Ёнеда-представим. (В Cat-модели 10.T1 нарушено; цель — найти не-LP модели.)

Обоснование

• Если α_𝖬 был бы Ёнеда-представим, он сводился бы к стандартному представимому функтору, и вся специфика Diakrisis редуцировалась бы.
• Axi-8 — потенциальный критерий новизны: если удовлетворён, то α_𝖬 — «активный» (не-пассивный) функтор.
• В стандартной Cat-модели нарушается (это — часть AFN-T).

Признание ограничения

• В Cat-модели 10.T1: α_𝖬 = ι(𝖬) и в Cat, ι(𝖬) — Ёнеда-представим через конкретный объект. Axi-8 нарушается.
• Попытки обойти: искать не-LP модели, где Axi-8 выполняется. Открытая задача.
• По AFN-T: полное удовлетворение Axi-8 + accessibility 𝖬 + прочие условия — невозможно.

Следствия

• При работе в Cat-модели: Axi-8 считается целью, не фактом.
• При работе в других моделях: Axi-8 может быть удовлетворён частично.

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

Для любой осмысленной конфигурации ограничений C, существует α_C ∈ Ob(⟪⟫), реализующая C.

Обоснование

• Axi-9 гарантирует, что ⟪⟫ богата — содержит артикуляции для любой разумной конфигурации.
• «Осмысленная конфигурация» — технический термин, уточняемый в моделях.
• В практике: существование Ω̄ (неподвижные точки 𝖬), достаточные α_F для каждого основания F.

Следствия

• 𝓜_Fnd содержит точки для всех известных оснований.
• Можно гарантированно найти α для любой разумной задачи.

T-α — α_math не универсальна

Канонический (классический) вариант T-α (по умолчанию):

$\exists \gamma \in \mathrm{Ob}(\llbracket\cdot\rrbracket): \gamma \not\sqsubset_0 \alpha_{math}.$

— позитивная экзистенциальная формулировка: существует конкретная артикуляция вне поля зрения α_math.

Классический эквивалент через двойное отрицание (применим при классической мета-логике):

$\neg(\forall \gamma \in \mathrm{Ob}(\llbracket\cdot\rrbracket), \gamma \sqsubset_0 \alpha_{math}).$

Две формулировки эквивалентны в классической мета-логике, но различаются в интуиционистской.

Спецификация мета-логики

Корпус Diakrisis работает по умолчанию в классической мета-логике (ZFC + 2 inaccessibles). В этом контексте:

• Canonical T-α (позитивный экзистенциальный вариант выше) — канонический.
• Двойное отрицание эквивалентно экзистенциальному по LEM.
• Gauge-структура и 𝓜_Fnd классически полны.

Конструктивный вариант T-α_c

Для работы в интуиционистских gauge-классах (α_int, α_hott, α_cic) используется усиленный конструктивный вариант:

$\mathbf{T\text{-}\alpha_c}: \mathrm{constructively}\ \exists \gamma \in \mathrm{Ob}(\llbracket\cdot\rrbracket): \gamma \not\sqsubset_0 \alpha_{math}.$

Этот вариант требует явного построения $\gamma$, не полагаясь на LEM. В интуиционистской настройке $\mathbf{T\text{-}\alpha_c} \Rightarrow \mathbf{T\text{-}\alpha}$, но не наоборот.

Применение в Diakrisis:

• Работа в $\alpha_{\mathrm{zfc}}, \alpha_{\mathrm{ncg}}, \alpha_{\mathrm{uhm}}$: использует классический T-α.
• Работа в $\alpha_{\mathrm{int}}, \alpha_{\mathrm{hott}}, \alpha_{\mathrm{cic}}$: использует конструктивный T-α_c.

Совместимость: оба варианта — варианты одной и той же аксиомы при соответствующем выборе мета-логики. Переход между ними — gauge-преобразование в meta-logical layer (logicality gauge).

Обоснование

• Без T-α могла бы быть α_math такая, что все γ ⊏_0 α_math — α_math как «универсальная линза». Это противоречило бы идее gauge-свободы.
• T-α гарантирует, что есть γ вне поля зрения α_math.
• Позитивный вариант (конструктивный) сильнее негативного; каноническое формулирование — позитивное.

Следствия

• Разные α_math дают разные ρ, и ни одна не универсальна.
• Gauge-структура неотделима от нетривиальности (разные α_math — разные точки 𝓜_Fnd).
• Конструктивные gauge-классы сохраняют нетривиальность через T-α_c.

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

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

Рассел-иммунитет (Теорема 10.T2).

Обоснование

• Без T-2f* наивная комплетация {α : P(α)} могла бы приводить к Рассел-подобным парадоксам.
• T-2f* блокирует самореферентные предикаты (P, ссылающийся на α_P).
• Формально: запрет на предикаты неограниченной глубины.

Детали T-2f*

• Глубина предиката: максимальная длина цепи 𝖬, ⊏_κ в выражении P.
• Глубина α_P: ранг α_P в иерархии 𝖬-итераций.
• Требование: глубина P < глубина α_P (строгое неравенство).

Следствия

• Все 5 именных семейств парадоксов (Рассел, Curry, Grelling, Burali-Forti, Жирар) — заблокированы (18.T).
• Универсальная парадокс-иммунность (105.T, /06-limits/10-maximality-theorems): T-2f* блокирует любой Яновский-сводимый самореферентный парадокс (Яновский 2003), не только именные 5 семейств. Включает Кантор, Тарский, Ловер, Гёдель-type, Löb и любой другой парадокс диагонального характера в cartesian-closed категориях.
• Теория консистентна относительно ZFC + 2 инаксессибальных (10.T1).
• (Max-3) из MSFS Definition def:maximality доказан для Diakrisis как теорема 105.T.

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

Теорема 21.T2: каждая аксиома Axi-0..Axi-9 + T-α + T-2f* независима (существует модель, удовлетворяющая всем остальным, но не выделенной).

Таблица независимости

Аксиома	Модель, опровергающая её (при выполнении остальных)
Axi-0	Пустая 2-категория
Axi-1	1-категория без 2-морфизмов
Axi-2	Постоянный функтор (не 2-функтор)
Axi-3	Без выделения
Axi-4	Без внутреннего хома
Axi-5	Тривиальная ρ (все ρ(α) эквивалентны)
Axi-6	Перестановочные ρ и 𝖬
Axi-7	Без α_𝖬
Axi-8	Все α_𝖬 Ёнеда-представимы
Axi-9	Бедная ⟪⟫ (без нужных артикуляций)
T-α	Универсальная α_math
T-2f*	Наивная комплетация без стратификации

Каждая модель — специфическая конструкция, показывающая, что без соответствующей аксиомы теория изменяется.

Методика проверки независимости

1. Взять все аксиомы кроме F.
2. Построить модель M, удовлетворяющую всем остальным.
3. Показать, что в M, F не выполняется.
4. Следствие: F не выводится из остальных.

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

Теорема 10.T1: система имеет модель в Cat. Относительно ZFC + 2 инаксессибальных — консистентна (см. /03-formal-architecture/08-cardinal-analysis).

Стандартная модель в Cat

• ⟪⟫ = 2-категория малых категорий Cat (или подходящая её подкатегория).
• 𝖬 = endofunctor «возьми функторную категорию на α» или подобный.
• α_math = фиксированная классифицирующая категория.
• ⊏_• — через 𝖬-итерации.

В этой модели выполняются Axi-0..Axi-7, Axi-9, T-α, T-2f*. Axi-8 (M-5w*) — нарушается, так как ι(𝖬) в Cat — Ёнеда-представим.

Альтернативные модели

• Не-LP модели: категории, не локально-представимые; там Axi-8 может выполняться. Открытая задача.
• Квантовые модели: модели на основе C*-алгебр или фон Нейман алгебр.
• ∞-категорные модели: работа в Люри HTT.

Ни в одной альтернативной модели всех 13 аксиом одновременно удовлетворить (в сильной форме) не удалось — что согласуется с AFN-T.

Формальные связи между аксиомами

Следствия

• Axi-0 + Axi-1 ⇒ ⟪⟫ непуста и имеет структуру.
• Axi-1 + Axi-2 ⇒ 𝖬 ∈ End(⟪⟫) имеет представителя α_𝖬 = ι(𝖬).
• Axi-1 + Axi-3 + Axi-4 ⇒ ρ корректно определено.
• Axi-4 + Axi-5 ⇒ ⟪⟫ — содержательна.
• Axi-7 ⇒ α_𝖬 удовлетворяет ключевое свойство взаимодействия с ρ.
• T-2f* ⇒ теория консистентна (10.T2, 18.T).

Не-следствия

• Axi-8 не выводится из Axi-0..7, 9, T-α, T-2f*.
• T-α не выводится из Axi-0..9 и T-2f*.
• Axi-6 не выводится из Axi-0..5, 7..9, T-α, T-2f*.

Эти независимости — часть Теоремы 21.T2.

Связь с мета-принципами П-0.x

Аксиома	Связь с принципами
Axi-0..3	Базовое существование (нейтрально к П-0.x)
Axi-4	П-0.4 (замкнутость через внутренний хом)
Axi-7	П-0.4 (самоартикулируемость)
Axi-8	П-0.5 (критерий новизны)
Axi-9	П-0.3 (достаточное богатство без иерархии уровней)
T-α	П-0.3 (без универсальной линзы)
T-2f*	П-0.4 (замкнутость без парадоксов)

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

/02-canonical-primitive/03-derived-notions — ρ, Fix(𝖬), Ω̄, α_𝖬, Trace(𝖠), mindepth.