𝖬 как модальный оператор

Статус

[Т] — S4-интерпретация 𝖬 в 2-категорной модальной семантике (стандарт Fitting 1969 + Келли-Street).

Обзор

Модальная интерпретация 𝖬 — способ понять эндо-функтор 𝖬 как модальный оператор в смысле модальной логики. Это открывает доступ к мощному аппарату модальной логики для работы с Diakrisis.

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

• Семантика: Kripke-семантика даёт интуитивный способ понимания 𝖬.
• Логика: S4-свойства 𝖬 выводимы и проверяемы.
• Связь с философией: модальные операторы традиционно связаны с понятиями «возможного», «необходимого», «знаемого».
• Применения: epistemic logic, modal теория типов — потенциальные расширения.

Теорема

Теорема 04.T1: 𝖬 — S4-модальный оператор.

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

В семантической интерпретации (Kripke-модель):

$\mathsf{M}: \llbracket\cdot\rrbracket \to \llbracket\cdot\rrbracket \Leftrightarrow \Box: \mathcal{P}(\mathrm{Worlds}) \to \mathcal{P}(\mathrm{Worlds})$

где Worlds — миры (артикуляции), □ — необходимость.

Содержание

𝖬 удовлетворяет аксиомам S4-логики:

• K: □(φ → ψ) → (□φ → □ψ).
• T: □φ → φ (рефлексивность).
• 4: □φ → □□φ (транзитивность).

НО: 𝖬 не удовлетворяет S5 (нет симметрии) — в соответствии с необратимостью акта Διάκрисис.

Аксиомы модальной логики

• K (распределительность): следствие функториальности 𝖬.
• T (рефлексивность): 𝖬(α) содержит α (как 0-я итерация).
• 4 (транзитивность): 𝖬(𝖬(α)) = 𝖬^2(α), повторное применение легитимно.

Почему не S5

S5-аксиома: ◇□φ → □φ (симметрия достижимости).

• Требовало бы: α ⊏_κ β ⟺ β ⊏_κ α (симметрия отношения достижимости).
• Но: ⊏_κ не симметрично. Если α ⊏_κ β (α — подартикуляция β на глубине κ), то обратное неверно.
• Феноменологически: акт различения необратим — от более простого к более сложному.

Формальный статус

• S4 для 𝖬 — доказуемо (через accessible endofunctor + unit/multiplication монады).
• S5 для 𝖬 — ложно (демонстрируется конкретным контрпримером в Cat-модели).

Kripke-семантика

• Миры = артикуляции α ∈ ⟪⟫.
• Отношение достижимости R = ⊏_{·}.
• ◇φ(α) = ∃β: α ⊏_· β ∧ φ(β).
• □φ(α) = ∀β: α ⊏_· β ⇒ φ(β).

Детальная формализация

Kripke-фрейм: (W, R), где W = Ob(⟪⟫), R = ⊏_•.

Kripke-модель: (W, R, V), где V: Prop → P(W) — оценка пропозиций.

Валидность:

• α ⊨ φ ⟺ α ∈ V(φ).
• α ⊨ □φ ⟺ ∀β, α R β ⇒ β ⊨ φ.
• α ⊨ ◇φ ⟺ ∃β, α R β ∧ β ⊨ φ.

Соответствие с 𝖬

Для 𝖬 как □:

• α ⊨ □φ ⟺ 𝖬(α) ⊨ φ (для 1-го уровня).
• α ⊨ □^κ φ ⟺ 𝖬^κ(α) ⊨ φ (для κ-го уровня).

То есть: □φ в α ⟺ φ верно в метаизации α.

Пример

Пусть φ = «существует не-тривиальный морфизм».

• α ⊨ φ: в α есть не-тривиальные морфизмы.
• α ⊨ □φ: в 𝖬(α) есть не-тривиальные морфизмы.

Это — осмысленное утверждение, не просто формальная игра.

Сопряжение

𝖬 имеет левый сопряжённый 𝖬^L (по accessibility), дающий ◇ через:

$\mathrm{Hom}(\mathsf{M}^L \alpha, \beta) \simeq \mathrm{Hom}(\alpha, \mathsf{M}\beta).$

Детализация

• Adjoint pair: 𝖬^L ⊣ 𝖬.
• 𝖬^L — «возможность» (◇).
• 𝖬 — «необходимость» (□).

Свойства adjoint pair

• Unit η: id ⟹ 𝖬 ∘ 𝖬^L.
• Counit ε: 𝖬^L ∘ 𝖬 ⟹ id.
• Треугольные тождества: стандартные.

Аксиомы для ◇ = 𝖬^L

Из adjoint pair:

• K для ◇: ◇(φ ∨ ψ) → (◇φ ∨ ◇ψ).
• T для ◇: φ → ◇φ.
• Дуальность: □φ = ¬◇¬φ (если у нас есть отрицание).

Ограничения

• 𝖬^L существует при accessibility 𝖬 (Axi-4).
• В некоторых моделях — 𝖬^L не определён globally, только на подкатегориях.
• Работа с 𝖬^L — более деликатна, чем с 𝖬.

Связь с когезией

Модальная S4 и когезия (Π ⊣ ♭ ⊣ ♯ ⊣ ι) — разные структуры, но могут совмещаться.

Гипотеза 16.H1: 𝖬 коммутирует с когезивными модальностями.

Детализация гипотезы

• 𝖬(Π(α)) ≃ Π(𝖬(α)): 𝖬 сохраняет компоненты.
• 𝖬(♭(α)) ≃ ♭(𝖬(α)): 𝖬 сохраняет дискретность.
• 𝖬(♯(α)) ≃ ♯(𝖬(α)): 𝖬 сохраняет codiscretness.
• 𝖬(ι(δ)) ≃ ι(𝖬_disc(δ)): 𝖬 совместима с ι.

Если все четыре выполняются — 𝖬 и когезия «ортогональны».

Статус гипотезы

• В Cat-модели: частично проверено (для первых двух).
• В α_uhm: открытый вопрос.
• Формальное доказательство — программа Пути Б.

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

• S4-модальность — стандартная.
• Сопряжения à la Ловер — стандартные.
• Наше применение — специфическое.

Источники

• Kripke (1959, 1963): Kripke-семантика модальных логик.
• Ловер (1970): Adjunctions as modalities.
• Moggi (1991): Modal monads в computer science.
• Эводи-Kishida (2008): Topology and modal logic.
• Fourman (1977): Sheaf models of modal logic.

Где не стандартно

• Применение к мат-основаниям (не логике).
• Совместимость с когезией Шрайбер.
• Интерпретация 𝖬 как «эндо-функтор метаизации».

Философская интерпретация

Эпистемическая интерпретация

• □φ в α: «В метаизации α, φ — необходимо».
• ◇φ в α: «В некоторой метаизации α, φ — возможно».

Темпоральная интерпретация

• α R β: «β — будущее α» (в метаизационном времени).
• □φ в α: «всегда после α, φ».
• ◇φ в α: «хотя бы раз после α, φ».

Феноменологическая интерпретация

• 𝖬(α): «α, как о ней говорится».
• □φ: «φ верно о способе говорения».
• ◇φ: «φ возможно в каком-то способе говорения».

Приложения модальной интерпретации

К Escape-теорема (13.T)

• Формулировка: «ρ(𝖬(α_T)) не лежит в ρ(α_T)» переводится в:
• «□ Con(T) — нарушается в T» (Гёдель II в модальной формулировке).

К Fix(𝖬)

• α ∈ Fix(𝖬) ⟺ 𝖬(α) ≃ α.
• В модальной интерпретации: «α — самосогласованная точка», где □ совпадает с id.
• Такие точки — «равновесия модальности».

К Trace(𝖠)

• Trace — последовательность □^κ(α_0).
• Модальная интерпретация: «итеративное применение необходимости».
• При достаточной accessibility — сходимость к Fix(𝖬).

Связь с другими логиками

Intuitionistic modal logic

• Наша S4-структура применима в интуиционистском случае.
• В HoTT-сборке (α_hott) модальности имеют конструктивный характер.

Linear modal logic

• Для УГМ-сборки (α_uhm) линейные модальности могут соответствовать квантовой механике.
• ! и ? операторы линейной логики — candidate для квантовых аналогов □ и ◇.

Homotopy modal logic

• В HoTT: модальности через adjunctions на типах.
• Унивалентность как структурная модальность.

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

/03-formal-architecture/06-duality.