Каталог логик как артикуляций
Статус
[Т-набр].
Обзор
В Diakrisis различные логики представляются как артикуляции. Это — важное методологическое различие:
- Ни одна логика не является «правильной» для Diakrisis.
- Каждая логика — gauge-выбор.
- Формальная структура Diakrisis сама логико-нейтральна.
Этот документ каталогизирует основные логики и их представление в Diakrisis.
Значение логико-нейтральности
- Gauge-инвариантность: формальные утверждения Diakrisis не зависят от выбора логики.
- Модулярность: разные сборки могут использовать разные логики.
- Совместимость: работа с разными основаниями (ZFC classical, HoTT intuitionistic) — через разные α.
Логики как gauge-классы
В Diakrisis каждая логика — специфическая артикуляция. АПЕЙРОН (как предельная структура) логико-нейтрален (10.C5).
Формальный смысл
Логика L задаётся:
- Синтаксисом (формулы).
- Семантикой (modelling).
- Deduction rules.
В Diakrisis: α_L ∈ ⟪⟫ с ρ(α_L) кодирующим все три.
Шесть базовых логик
α_cl — классическая
ρ(α_cl) — Boolean algebra. Tertium non datur, Де Морган.
Детализация
- Язык: ¬, ∧, ∨, →, ↔, ∀, ∃.
- Семантика: Boolean algebras (частный случай: {0,1}).
- Правила: modus ponens + все tautologies.
- Ключевые аксиомы: ¬¬A → A (double negation), A ∨ ¬A (LEM).
В Diakrisis
- α_cl соответствует стандартной классической логике.
- ρ(α_cl) — функтор на Boolean algebras.
- α_zfc основано на α_cl (ZFC — классическая).
α_int — интуиционистская
ρ(α_int) — Гейтинг algebra. Конструктивная, без TND.
Детализация
- Язык: тот же, что классический.
- Семантика: Гейтинг algebras (обобщение Boolean).
- Правила: без LEM, без двойного отрицания.
- BHK-интерпретация: Брауэр-Гейтинг-Колмогоров — конструктивная.
10.T1: α_int ↔ α_topos (внутренний язык топоса — интуиционистский).
Значение 10.T1
- Внутренний язык любого elementary topos — интуиционистский.
- Классическая логика достигается только в Boolean topoi.
- α_hott, α_topoi — в gauge-классе α_int (для соответствующих фрагментов).
α_lin — линейная (Жирар)
ρ(α_lin) — symmetric monoidal category с ℓ-отрицанием. Ресурсы однократны.
Детализация линейной логики
Линейная логика (Жирар 1987):
- Ресурсная интерпретация: формула — ресурс, используется ровно один раз.
- Два конъюнктива: ⊗ (tensor) и & (with).
- Два дизъюнктива: ⊕ (plus) и ⅋ (par).
- Модальности: ! (of course, unlimited) и ? (why not).
10.T2: α_lin — квантоподобна. α_lin ⊂ α_Q.
Значение 10.T2
- Линейная логика семантически близка к квантовой.
- ⊗ ≈ tensor product в гильбертовом пространстве.
- & ≈ superposition.
- Это делает α_lin полезной в квантовой сборке (УГМ).
α_modal^S — модальная
Семейство: S4, S5, T, K и др. 10.C3: АПЕЙРОН-𝖬 сам — S4-модальный оператор.
Основные модальные системы
| Система | Аксиомы | Интерпретация |
|---|---|---|
| K | K (□-distrib) | базовая |
| T | K + □φ → φ | reflexivity |
| S4 | T + □φ → □□φ | reflexivity + transitivity |
| S5 | S4 + ¬□φ → □¬□φ | равноправные миры |
В Diakrisis
- 𝖬 как S4-модальность: см. /03-formal-architecture/05-modal-interpretation.
- Разные α_S могут работать с разными модальными системами.
- Общая структура — Kripke-semantics.
α_quantum — квантовая (Birkhoff-von Neumann)
Ортомодулярная решётка. Связь с α_opalg и α_Q.
Квантовая логика
Quantum logic (Birkhoff-von Neumann 1936):
- Логика, соответствующая квантовой механике.
- Решётка подпространств гильбертова пространства.
- Неравенство дистрибутивности: a ∧ (b ∨ c) ≠ (a ∧ b) ∨ (a ∧ c) в общем случае.
- Ортомодулярность: слабая форма дистрибутивности.
10.C4: УГМ-логика = α_quantum.
УГМ-логика
- В α_uhm: логика наблюдаемых — квантовая.
- Работа с Γ ∈ D(ℂ⁷) — в контексте orthomodular lattice.
- Связь с C*-алгебрами (через α_NCG).
α_rel — релевантная
Импликация с релевантностью антецедента. Параконсистентна в слабом смысле.
Relevance logic
Relevance logic (Anderson-Belnap 1975+):
- Отвергает: A → (B → A), ⊥ → A (explosion).
- Требует: антецедент должен быть «релевантен» консеквенту.
- Параконсистентность: контрадикции не порождают всё.
В Diakrisis
- α_rel — нишевая, но полезная в некоторых contexts.
- Не основная в любой из стандартных сборок.
- Может быть полезна для анализа пределов (AFN-T — своего рода параконсистентное утверждение).
Таблица
| Логика | α | ν | Морита-класс |
|---|---|---|---|
| Классическая | α_cl | ω | отдельный |
| Интуиционистская | α_int | ω+1 | с α_topos |
| Линейная | α_lin | ω+1 | с α_Q |
| Модальная S4 | α_S4 | ω+1 | c АПЕЙРОН-𝖬 |
| Квантовая | α_q | ω+2 | с α_uhm |
| Релевантная | α_rel | ω+1 | отдельный |
Расширенная таблица
| Логика | Конъюнкция | Дизъюнкция | Отрицание | LEM | Применение |
|---|---|---|---|---|---|
| Классическая | ∧ | ∨ | ¬ | ✓ | mainstream math |
| Интуиционистская | ∧ | ∨ | ¬ | ✗ | HoTT, topoi |
| Линейная | ⊗, & | ⊕, ⅋ | ⊥ | n/a | quantum, resources |
| Модальная S4 | ∧ | ∨ | ¬ | depends | epistemic |
| Квантовая | ∧ | ∨ | ⊥ | ✗ (dist) | УГМ |
| Релевантная | ∧ | ∨ | ¬ | weak | paraconsistency |
Логико-нейтральность
10.C5: АПЕЙРОН не привилегирует логику. Выбор логики — выбор gauge.
Формальный аппарат Diakrisis (Axi-0..Axi-9) не специфицирует логику; это — решение пользователя.
Детализация логико-нейтральности
- Axi-0..Axi-9 выражены в мета-логике (какой — выбираем при реализации).
- Разные мета-логики дают разные модели Diakrisis.
- Диакриtive utterances — инвариантны относительно выбора логики.
Практические следствия
- Можно работать с Diakrisis в classical ZFC (по умолчанию).
- Можно — в intuitionistic HoTT.
- Можно — в linear logic (для квантовых приложений).
Выбор — прагматический, не структурный.
Отличие от стандартных подходов
Большинство мат-оснований имеет встроенную логику:
- ZFC — classical.
- HoTT — intuitionistic.
- LL-based systems — linear.
Diakrisis не привязан к конкретной логике; она — параметр.
Связи между логиками в 𝓜_Fnd
Переходы
- α_int → α_cl: через double-negation трансляция.
- α_cl → α_int: не естественен (требует LEM).
- α_lin → α_int: через экспоненциал !.
- α_cl → α_modal: через трансляция ¬¬ = □.
Морита-связи
- α_cl ∼_Morita α_Bool (classical logic ↔ Boolean algebra).
- α_int ∼_Morita α_Heyting.
- α_lin ∼_Morita α_SMC (symmetric monoidal).
- α_quantum ∼_Morita α_OM (orthomodular).
Пути в 𝓜_Fnd
Разные логики — разные точки 𝓜_Fnd. Пути между ними — translations + modifications.
Дополнительные логики (не в списке 6)
Fuzzy logic
- Значения в [0, 1] (или t-нормах).
- Применение: soft reasoning.
- В Diakrisis: α_fuzzy.
Probabilistic logic
- Вероятностные значения.
- Связь с теорией вероятностей.
- В Diakrisis: α_prob.
Temporal logic
- Время как параметр.
- LTL, CTL, и т.д.
- В Diakrisis: α_temporal, связана с 𝖬-модальностями.
Dependent-type logic (CIC, MLTT)
- Пропозиции как типы.
- Кодирование логики в теория типов.
- Связана с α_CIC, α_HoTT.
Применение в сборках
α_uhm (УГМ)
- Основная логика: α_quantum.
- Дополнительно: α_lin (для CPTP).
- Мета-логика: α_cl (для теорем о УГМ).
α_sm (Стандартная модель)
- Gauge-logic через симметрии.
- Связь с α_modal (gauge-variables).
- Классическая для базового уровня.
α_consciousness
- Различные логики для разных аспектов.
- α_modal (epistemic).
- α_fuzzy (gradations).
- α_quantum (через УГМ).