Перейти к основному содержимому

ZFC как извлечение

Статус​

[Т-набр] — детальная формализация .

Обзор​

ZFC (Zermelo-Fraenkel + Choice) — классическое основание математики XX века. В Diakrisis оно представляется конкретной артикуляцией α_ZFC ∈ ⟪⟫.

Зачем извлекать ZFC​

  • Центральное основание: ZFC — доминирующее основание mainstream математики.
  • Reference point: многие другие основания сравниваются через перевод в ZFC.
  • Проверка Diakrisis: если ZFC не извлекается чисто — проблема в Diakrisis.
  • Демонстрация Универсальное основание Theorem: первый пример 29.T.

α_ZFC​

ν_{α_ZFC} = ω (конечные итерации + аксиомная схема замещения → предельный ω).

Конструкция α_ZFC​

  • Ob(α_ZFC): множества как объекты ZFC.
  • Hom(A, B): функции A → B (в ZFC-смысле).
  • 2-морфизмы: тривиальные (нет 2-структуры в 1-категории Set).
  • α_math: Set или специфический object классификатор.

Для получения 2-категорной структуры нужно поднять ZFC до Cat или topos-варианта. В «чистой» ZFC у нас 1-категория.

Интерпретация ν_ZFC = ω​

  • Конечные итерации 𝖬 — соответствуют конечным множествам.
  • ω-итерация 𝖬 — бесконечность (ω-колимит).
  • За ω (ω+1, ω+2, ...): не естественно для ZFC — требует инaccessible cardinals.

Значит ZFC — «на уровне ω» в нашей классификации.

Соответствие ZFC-аксиом​

ZFCα_ZFC-структура
Extensionalityморфизмы ρ(α_ZFC) по ⊏_0
Pairingкоалимитные пары
Unionколимит
Powersetвнутренний хом [α, ?]
Infinityα_ω ∈ Trace(𝖠)
Фундированиеwell-foundedness ⊏_0
ReplacementAxi-9 (достаточность)
Choiceсуществование глобальных сечений

Детальный разбор каждой аксиомы​

Extensionality (A = B ⟺ ∀x (x ∈ A ⟺ x ∈ B)):

  • В Diakrisis: два объекта α, β ∈ Ob(⟪⟫) эквивалентны ⟺ существует обратимый морфизм.
  • Соответствие естественно через ⊏_0.

Pairing (∀A, B ∃C {A, B} ⊂ C):

  • В Diakrisis: существование копроизведения (coproduct) A + B.
  • Требует структурной полноты Axi-9.

Union (∀A ∃B = ∪A):

  • В Diakrisis: колимит по индексирующему классу.
  • Стандартная 2-категорная конструкция.

Powerset (∀A ∃𝒫(A)):

  • В Diakrisis: внутренний хом [A, Ω], где Ω — subobject классификатор.
  • Не всегда выполняется в нашем общем примитиве (требует дополнительной структуры).

Infinity:

  • В Diakrisis: существование α_ω ∈ Trace(𝖠).
  • Гарантировано Axi-0 + accessibility 𝖬.

Foundation:

  • В Diakrisis: ⊏_0 well-founded.
  • Блокирует бесконечные нисходящие цепи.
  • Соответствует отсутствию α ⊏_0 α' с α' ⊏_0 α''' ⊏_0 ... → α.

Replacement:

  • В Diakrisis: Axi-9 (достаточность).
  • Для любой «описуемой конфигурации» существует α, её реализующая.

Choice:

  • В Diakrisis: существование глобальных сечений ρ (из fibration-структуры).
  • Стандартное применение AC в категорном контексте.

V-иерархия = 𝖬-итерация​

02.T2: фон-Нейман иерархия V_α = 𝖬-итерация в ZFC-проекции ρ(α_ZFC).

Формализация​

  • V_0 := ∅.
  • V_{α+1} := 𝒫(V_α).
  • V_λ := ∪_{β<λ} V_β для предельного λ.

В Diakrisis-проекции:

  • 𝖬^0(⊥) := ∅.
  • 𝖬^{α+1}(⊥) := «powerset-аналог» от 𝖬^α(⊥).
  • 𝖬^λ(⊥) := колимит.

Соответствие V_α ≃ 𝖬^α(⊥) — биекция фон-Нейман иерархии с 𝖬-итерацией.

Значение​

  • V-иерархия — частный случай Trace(𝖠) для α_0 = ⊥.
  • Понятие «кумулятивной иерархии» в ZFC — интерпретируется как 𝖬-развёртывание.
  • Inaccessibles → неподвижные точки 𝖬 в V-иерархии.

Гротендик-universes = Fix-подмножества​

02.T3: Гротендик-universe — подмножество Fix(𝖬) в ZFC-ограничении.

Формализация​

Гротендик universe U — множество, удовлетворяющее:

  • Транзитивно: x ∈ y ∈ U ⟹ x ∈ U.
  • Замкнуто под элементарными операциями (pairing, powerset, union).
  • «Большое»: содержит достаточно для работы математики.

В Diakrisis: U соответствует неподвижной точке 𝖬, т.е. элементу Fix(𝖬).

Связь с inaccessibles​

  • Гротендик universe существует ⟺ существует inaccessible cardinal.
  • Inaccessible cardinal κ ↔ неподвижная точка 𝖬.
  • ZFC + «существует inaccessible» ↔ Diakrisis с Fix(𝖬) ≠ ∅ в ZFC-ограничении.

Морита с ETCS​

По Ловер, ZFC ↔ ETCS Морита-эквивалентны. В Diakrisis: α_ZFC ∼_{gauge} α_ETCS.

Детализация Морита-эквивалентности​

ETCS (Elementary Theory of the Category of Sets, Ловер 1964):

  • Основание на базе теории категорий.
  • Аксиомы о категории Set (elementary topos + choice + NNO).
  • Морита-эквивалентна ZFC (Шульман proof).

В Diakrisis: α_ZFC и α_ETCS — один gauge-класс в 𝓜_Fnd.

Значение для Diakrisis​

Это подтверждает: gauge-структура Diakrisis согласуется с классической теорией Морита-эквивалентности.

  • Если X ∼_Morita Y (по классической) — [α_X] = [α_Y] (в 𝓜_Fnd).
  • Обратное (надеемся): [α_X] = [α_Y] ⟹ X ∼_Morita Y.

Побег (Гёдель)​

По 13.T, 𝖬(α_ZFC) содержит утверждения (G, Con(ZFC), инаксессибалы), не выразимые в ZFC. Это — структурная переупаковка Гёдель.

Детализация​

Гёдель II (1931): Con(ZFC) не доказуема в ZFC (если ZFC консистентна).

В Diakrisis:

  • ρ(α_ZFC): всё, что выразимо в ZFC.
  • ρ(𝖬(α_ZFC)): всё, что выразимо в «мета-ZFC» (ZFC + рефлексивные утверждения).
  • Побег: ρ(𝖬(α_ZFC)) ⊄ ρ(α_ZFC).

Это — формальная переупаковка Гёдель в языке Diakrisis.

Конкретные элементы побега​

  • Con(ZFC): в 𝖬(α_ZFC), но не в α_ZFC.
  • Goodstein's theorem: в 𝖬(α_ZFC) (через ε_0-индукцию).
  • Inaccessibles: в 𝖬^2(α_ZFC) или выше.
  • Large cardinals в иерархии: на разных уровнях 𝖬^κ.

Признанные редукции​

  • Стандартная ZFC-теория.
  • Переупаковка Гёдель.
  • Ловер ZFC/ETCS эквивалентность.

Источники​

  • Zermelo (1908), Fraenkel (1922): ZF аксиомы.
  • von Neumann (1925): V-иерархия.
  • Гротендик (1964): universes.
  • Ловер (1964): ETCS.
  • Шульман (2010): ZFC/ETCS Морита.

Что сохраняется в α_ZFC​

  • Все теоремы ZFC — выводимы через ρ(α_ZFC).
  • Иерархия V — 𝖬-развёртывание.
  • Гёдель II — через побег.
  • Inaccessibles — Fix(𝖬) при соответствующей глубине.

Что не сохраняется​

  • Специфический язык: α_ZFC работает в 2-категорном языке, не на уровне формул ZFC.
  • Конкретная символика: ∈ интерпретируется через ⊏_0.
  • Choice в конкретной формулировке: обобщается до «глобальных сечений».

Это — ожидаемые потери при переводе. Структурное содержание сохраняется.

Применение​

В сравнительном анализе​

Через α_ZFC можно сравнивать ZFC с другими основаниями:

  • ZFC vs HoTT: разные gauge-классы.
  • ZFC vs NCG: разные уровни ν.
  • ZFC vs УГМ: существенная разница (ν_ZFC = ω, ν_uhm = ω·3+1).

В мета-теории​

  • Анализ классов аксиом ZFC через 𝖬-итерации.
  • Изучение «добавлений» к ZFC (large cardinals) через Fix(𝖬).
  • Сравнение со «слабыми» и «сильными» формами ZFC.

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

/04-extractions/02-hott.