Формально-логическая ДЦ-линия

0. Мотивация

Некоторые ДЦ-направления имеют формальную форму — это логики, семантики, теории типов, в которых «акт» уже является первичным концептом на уровне определения. Эти направления дают Актика техническое ядро, в отличие от философских источников (Уайтхед, Варела и т.д.).

Актика поглощает семь таких направлений:

1. Брауэр-Гейтинг-Колмогоров (BHK)-семантика — конструктивный акт доказательства.
2. Мартин-Лёф MLTT — судaction как первичное понятие.
3. Диалогическая логика Лоренцена — доказательство как диалог.
4. Game-семантика Хинтикка — истина как выигрышная стратегия.
5. Жирар Ludics — сетевая семантика, дуал proof normalization.
6. Curry-Howard-Ламбек — пропозиции как типы, типы как практики.
7. Concurrency-формализмы (Actor-model Хьюитт, π-calculus Милнер, CSP Хоар) — параллельный акт как первичный.

1. BHK-семантика как ε-семантика

1.1 Историческая суть

Брауэр (1907), Гейтинг (1930), Колмогоров (1932) независимо обнаружили: интуиционистская логика естественно интерпретируется через понятие конструкции:

• $\llbracket A \wedge B \rrbracket$ = пара (конструкция $A$, конструкция $B$).
• $\llbracket A \to B \rrbracket$ = функция, отображающая конструкции $A$ в конструкции $B$.
• $\llbracket \exists x. A(x) \rrbracket$ = пара (свидетель $a$, конструкция $A(a)$).

Ключевое: BHK-семантика не постулирует множество истинных пропозиций; она определяет истину через акт конструкции.

1.2 Актика-образ

Теорема 121.T (уже в /12-actic/06-actic-theorems). Для любой пропозиции $\phi$: $\llbracket \phi \rrbracket_\mathrm{BHK} = \varepsilon(\alpha_\phi)$.

Разъяснение: акт-интерпретация интуиционистских пропозиций — в точности ε-дуал OC-пропозиции. Интуиционизм — ДЦ-логика по определению; классическая логика — ОЦ-логика.

1.3 Следствие для Verum

Verum-языковая теория типов должна быть интуиционистской (BHK-совместимой). Включение закона исключённого третьего (LEM) — опционально и помечается как классический акт $\varepsilon_\mathrm{LEM}$ с $\varepsilon = \omega + 1$ (акт добавления, не фундаментальная операция).

2. Мартин-Лёф MLTT: предложение = тип = действие

2.1 Три эквивалентности Мартин-Лёфа

Мартин-Лёф в 1984 г. сформулировал:

$$\text{proposition} \equiv \text{type} \equiv \text{set of judgements}.$$

Предложение — как ОЦ-объект. Тип — как формальная структура. Набор суждений — как акт.

2.2 Актика-реформулировка

Мартин-Лёфовская эквивалентность — это канонический изоморфизм $\alpha \leftrightarrow \varepsilon$ в одном частном случае (типовая теория). 108.T обобщает это на все артикуляции.

Строго: Мартин-Лёфовские правила вывода: «предложение A верно» ≡ «я могу привести доказательство A» ≡ «я могу продемонстрировать конструкцию типа A». Третья формулировка — ε-акт. Первая — α-артикуляция. Вторая — их среднее (мост).

2.3 Практическая значимость

MLTT — уже ДЦ-теория (на уровне формальной арифметики и логики). Актика — её ретроактивное философское основание и её обобщение далеко за пределы типовой теории.

3. Диалогическая логика Лоренцена

3.1 Лоренценов вклад

Пауль Лоренцен (1960) формализовал: истинность пропозиции = существование выигрышной стратегии в диалоге между Proponent-ом и Opponent-ом.

• $A \to B$ доказуема ⟺ Proponent может ответить на любой вызов Opponent-а.
• $A \wedge B$ доказуема ⟺ Proponent может защитить как $A$, так и $B$.

3.2 Актика-интерпретация

Диалог — это структурированный набор актов. Proponent-акт-защиты и Opponent-акт-вызова суть $\varepsilon$-акты с координацией. Вся диалогическая схема — конкретный перформанс высокоуровневой практики «формального диалога» с $\varepsilon = \omega + 1$.

Теорема 126.T. Пусть $\mathcal{D}$ — формальный диалог с протоколом правил Лоренцена. Тогда $\mathcal{D} \in \rangle\!\rangle \cdot \langle\!\langle$ с глубиной $\omega + k$, где $k$ — количество ходов в диалоге.

Доказательство: каждый ход — акт-активация; $k$ ходов — $\mathsf{A}^k$-итерация; активация акта-обсуждения добавляет $+1$. ∎

4. Game-семантика Хинтикка–Abramsky

Jaakko Хинтикка (1973) и позже Samson Abramsky с соавторами формализовали: пропозиция = игра между Verifier и Falsifier; $\phi$ истинна ⟺ у Verifier-а есть выигрышная стратегия.

Различие с Лоренценом: Лоренцен подразумевает диалог между людьми; Хинтикка–Abramsky — математическую игру с совершенной информацией.

4.1 Актика-образ

Игровая семантика — реалистическая семантика для линейной и классической логики. В Актика:

$$\mathrm{Game}(\phi) \simeq \mathrm{Perf}(\alpha_\phi).$$

То есть категория game-стратегий для $\phi$ равна категории перформансов артикуляции $\phi$. Это прямое приложение 108.T.

4.2 Связь с категориями

Category of games = symmetric monoidal closed category; это формальная структура на $\mathrm{Perf}(\alpha_\mathrm{linear})$.

5. Жирар Ludics

5.1 Суть ludics

Жан-Ив Жирар в «Locus Solum» (2001) разработал ludics — семантику linear logic через сетевые desseins (дизайны), designs (проекты) и chronicles (хроники). Ключевое: семантика не привязана ни к пропозициям, ни к доказательствам, а к их «сетевой динамике».

5.2 Актика-дуализация

Теорема 120.T (уже в /12-actic/06-actic-theorems):

$$\mathrm{Design}_\mathrm{Жирар} \simeq \mathrm{Perf}(\alpha_\mathrm{linear}),$$ $$\mathrm{Desseins} \simeq \text{2-cells in } \rangle\!\rangle \cdot \langle\!\langle.$$

5.3 Философская значимость

Ludics — первая математическая семантика, явно называющая себя действие-центричной. Проекты — это «что делается»; хроники — «что произошло». Линия: Брауэр → Мартин-Лёф → Жирар-ludics — это ядро формальной ДЦ-традиции, которая в Актика встречает свою обобщённую форму.

6. Curry-Howard-Ламбек

6.1 Общая изоморфия

$$\text{proposition} \leftrightarrow \text{type} \leftrightarrow \text{category}.$$

Curry (1934), Howard (1969), Ламбек (1972) независимо показали: логика ⟺ лямбда-исчисление ⟺ декартово-замкнутые категории.

6.2 Актика-доктринa

В Актика это — один из случаев 108.T:

$$\alpha \leftrightarrow \varepsilon(\alpha) \leftrightarrow \mathrm{Mod}(\alpha) \simeq \mathrm{Perf}(\alpha).$$

Пропозиция = артикуляция; тип = та же артикуляция в другом синтаксисе; категория = модель/перформанс.

6.3 Significance для Verum

Curry-Howard-Ламбек — это стандарт, на котором построены Coq, Lean, Agda. Актика обобщает его до $\alpha$-$\varepsilon$-дуальности, указывая: действие программирования — первично; тип программы и пропозиция спецификации — две стороны одной медали с практикой.

7. Concurrency-формализмы

7.1 Хьюитт Actor model (1973)

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

7.2 Милнер π-calculus (1989)

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

7.3 Хоар CSP (1985)

Тони Хоар: последовательные процессы, синхронизирующиеся по событиям. Базовый акт — совместное событие.

7.4 Общая Актика-дуализация

Все три формализма — чистые ДЦ-формализмы для параллельных систем. В Актика:

$$\varepsilon_\mathrm{send} \sqsupset_\omega \varepsilon_\mathrm{sync} \sqsupset_\omega \varepsilon_\mathrm{compute}.$$

Три primiverных акта-вычисления, связанных координациями через $\sqsupset_\omega$. Это естественные примитивы Актика для построения AC-вычислений.

7.5 Verum применение

Verum должен включать native concurrency на уровне stdlib — не как внешнюю библиотеку, а как встроенное $\varepsilon_\mathrm{send}, \varepsilon_\mathrm{sync}, \varepsilon_\mathrm{compute}$. Это прямая реализация формально-логической ДЦ.

8. Связь с Plotkin и денотационной семантикой

Gordon Plotkin (1975) структурировал денотационную семантику как семантику вычисления, а не просто семантику синтаксиса. Это переходный мост: классическая денотационная семантика — ОЦ (функции между доменами); пост-Plotkin — близко к ДЦ (акты в доменах).

В Актика: денотационная семантика Plotkin — это $\alpha$-сторона дуальности; операционная семантика — $\varepsilon$-сторона; равноправны.

9. Синтетическая сводка: ядро формально-логической ДЦ

Теорема 127.T [Т·L3]. Существует подкатегория $\rangle\!\rangle \cdot \langle\!\langle_\mathrm{formal-logic} \subset \rangle\!\rangle \cdot \langle\!\langle$, состоящая из актов формально-логических ДЦ-традиций (BHK, MLTT, Ludics, Curry-Howard, Диалогическая, Game, Concurrency). Эта подкатегория замкнута под:

1. Конкатенацией актов (|)
2. Параллельной композицией (⊗)
3. Активацией $\mathsf{A}$
4. Gauge-преобразованиями

и локально эквивалентна категории symmetric monoidal closed $(\infty, 1)$-категорий.

Следствие. Формально-логическая ДЦ — математически дисциплинирована и унифицирована внутри Актика. Это не просто «коллекция традиций», а формальная структура.

10. Ссылки

• /12-actic/00-foundations — обзор Актика.
• /12-actic/01-historical-lineage — все 35+ традиций.
• /12-actic/06-actic-theorems — теоремы 120.T, 121.T.
• /12-actic/09-verum-stdlib-sketch — Verum-stdlib для core.action.*
• /04-extractions/06-logics-catalog — классификация логик в ОЦ-корпусе.