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

Модельная теория Diakrisis

Статус​

[Т] — классические мета-теоремы установлены: 41.T1 полнота (Гёдель), 41.T2 компактность (Malcev), 41.T3-T4 Löwenheim-Skolem, 41.T5 stability (Shelah).

Обзор​

Модельная теория Diakrisis — применение стандартной model-theoretic техники к нашей 2-категорной структуре. Цель: установить классические мета-свойства (полнота, компактность, категоричность) для Diakrisis.

Зачем модельная теория​

  • Мета-обоснование: доказать, что Diakrisis имеет хорошие логические свойства.
  • Классификация моделей: понять, какие модели существуют.
  • Связь с классической теорией: использовать существующий аппарат.
  • Готовность к Verum-формализации: Путь Б требует хорошей модельной теории.

Классические мета-теоремы​

Полнота (41.T1)​

First-order часть Diakrisis дедуктивно полна. Стандартная Гёдель-полнота.

Формулировка​

Для first-order подъязыка L_0 Diakrisis:

T⊢ϕ⇔T⊨ϕ.T \vdash \phi \Leftrightarrow T \models \phi.

То есть: синтаксическая доказуемость = семантическая валидность.

Доказательство (контур)​

  • L_0 — фрагмент языка Diakrisis, ограниченный first-order.
  • Применение теоремы Гёделя о полноте first-order логики.
  • Deduction theorem + Soundness + Completeness.
  • Ограничение: работает только для first-order части, не для полной 2-категорной.

Ограничения​

  • высшего порядка часть (2-категорная структура) — не подпадает под Гёдель-полноту.
  • Полнота для higher-order — проблематична (теоремы Вака-Клепфа и Генкин).
  • В Diakrisis мы работаем с Henkin-моделями для higher-order части.

Компактность (41.T2)​

Компактность выполняется. Следствие: существование нестандартных моделей.

Формулировка​

Для теории T ⊆ L_0:

Каждое конечное подмножество T имеет модель⇒T имеет модель.\text{Каждое конечное подмножество } T \text{ имеет модель} \Rightarrow T \text{ имеет модель}.

Следствия компактности​

  • Нестандартные модели: если T имеет бесконечную модель, она имеет модели произвольной кардинальности.
  • Типы: существуют полные типы, не реализованные в стандартных моделях.
  • Ультрапродукты: стандартная техника построения нестандартных моделей.

Löwenheim-Skolem (41.T3, 41.T4)​

  • Downward: малые модели.
  • Upward: большие.

Downward LS (41.T3)​

Если T имеет модель размера ≥ κ (неисчислимого), то T имеет модель любого размера λ ≥ |L|.

Следствие: даже если Diakrisis описывает большие структуры, существуют «счётные» модели.

Upward LS (41.T4)​

Если T имеет бесконечную модель, то T имеет модели произвольно больших размеров.

Следствие: никакая теория не может фиксировать кардинальность (классическая проблема).

Stability (41.T5)​

Diakrisis — stable-теория в смысле Shelah. Управляемая таксономия моделей.

Формулировка stability​

Теория T стабильна, если для всякого λ, количество типов над моделью размера λ ограничено полиномом от λ.

Следствия stability​

  • Хорошая классификация моделей: по Shelah's classification theorem.
  • Существование sauvedards-моделей: канонические представители.
  • Forking и non-forking extensions: стандартный аппарат.

Craig interpolation (41.T6)​

Выполняется.

Формулировка​

Для T_1, T_2 ⊆ L и φ ∈ L:

T1∪T2⊢ϕ⇒∃ψ∈L1∩L2:T1⊢ψ и T2⊢ψ→ϕ.T_1 \cup T_2 \vdash \phi \Rightarrow \exists \psi \in L_1 \cap L_2: T_1 \vdash \psi \text{ и } T_2 \vdash \psi \to \phi.

Значение​

  • Обеспечивает модульность теории.
  • Позволяет «изолировать» части теории.
  • Применяется в автоматическом доказательстве.

Beth definability (41.T7)​

Неявные определения = явные.

Формулировка​

Если P неявно определимо из T (любые две модели T, согласующиеся на L{P}, согласуются на P), то P явно определимо из T.

Значение​

  • Консервативность: добавление неявно определимого P не добавляет мощности.
  • Элиминация определений: любое неявное определение превращается в явное.

Категоричность​

По теореме 88.T: Diakrisis категоричен — все модели (∞,∞)-эквивалентны.

При фиксированных кардинальных ресурсах все модели 2-эквивалентны (теорема 25.T — 2-уровневая версия).

Детализация категоричности​

κ-категоричность: теория T категорична в кардинальности κ, если все модели T размера κ изоморфны.

Для Diakrisis:

  • В ℵ_0: зависит от конкретных реализаций.
  • Для крупных кардиналов: категоричность по Морлею может быть верна.

Связь с классификационной теорией Shelah​

  • Stable theories классифицируются по spectrum функции.
  • Diakrisis — вероятно «superstable» (сильная форма stability).
  • Spectrum: максимум ℵ_0-категоричность + κ-категоричность для крупных κ.

Следствие​

Diakrisis — классически хорошо-поведенческая теория с полной мета-теоретической структурой.

Практические следствия​

  • Автоматическая верификация: можно применять стандартные прувер-техники.
  • Предсказуемое поведение: нет патологий, нарушающих стандартные ожидания.
  • Хорошая параметризация: семейства моделей управляемы.

Ограничения​

  • высшего порядка: 2-категорная часть требует более тонкой модельной теории.
  • AFN-T: некоторые утверждения не first-order формулируемы; модельная теория для них ограничена.

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

Все классические мета-теоремы — редукции к стандартной модельной теории. Не новое, но применимое.

Источники​

  • Гёдель (1929): completeness theorem.
  • Malcev (1936): compactness.
  • Löwenheim (1915), Skolem (1920): Löwenheim-Skolem.
  • Craig (1957): interpolation.
  • Beth (1953): definability.
  • Shelah (1978): classification theory.

Всё — стандартный арсенал. Применение к Diakrisis — проверочное упражнение, не новый результат.

Модели в разных формализмах​

В Cat (стандартная модель)​

  • ⟪⟫ = Cat (2-категория малых категорий).
  • Все первопорядковые теоремы — верны.
  • Axi-8 нарушается (ограничение в Cat).

В HoTT​

  • ⟪⟫ = универсум типов.
  • Унивалентность как gauge-симметрия.
  • Проблема: HoTT требует univalence, что усиливает теорию.

В (∞,1)-топосах (Люри)​

  • ⟪⟫ = специфический (∞,1)-топос.
  • высшего порядка модельная теория.
  • Более богатая структура.

В не-LP категориях (программа)​

  • Попытка найти модели, где Axi-8 выполняется.
  • Открытая задача.
  • По AFN-T: полное удовлетворение невозможно.

Связь с Verum-формализацией​

Модельная теория обеспечивает основу для Verum-формализации УГМ (Путь Б):

  • Доказательство теорем в first-order фрагменте — полная Verum-проверка.
  • высшего порядка теоремы — через Henkin-модели или сильные прувер'ы.
  • Компактность даёт гибкость в определении моделей.

Специфические для Diakrisis модельные вопросы​

Интерпретация Axi-8​

  • В Cat-модели: нарушается.
  • В альтернативных моделях: цель, не факт.
  • Вопрос: существует ли модель, удовлетворяющая всем 13 аксиомам одновременно в строгой форме?
  • Ответ (по AFN-T): в определённом смысле — нет.

Модели с gauge​

  • Gauge-инвариантные модели — подкласс.
  • Специфическая gauge-группа может фиксировать класс моделей.
  • Применение: УГМ-сборка имеет специфическую gauge-структуру S₇ × ...

Модели с когезией​

  • Cohesive ∞-топосы (Шрайбер) как модели.
  • Обеспечивают Π ⊣ ♭ ⊣ ♯ ⊣ ι структуру.

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

/03-formal-architecture/08-cardinal-analysis.