Полная родословная действие-центричной мысли

Назначение документа

Метастемология Чурилова называет пять русскоязычных источников (Боярин, Бахтияров, Анохин, Щедровицкий, Мартынов). Этого покрытия достаточно для инженерной практики, но недостаточно для формальной теории: оно упускает 2500 лет философской традиции и, критично, формально-логическую ДЦ-линию внутри самой математики. Настоящий документ разворачивает полную линию из /12-actic/00-foundations §2, фиксируя для каждой точки:

1. ДЦ-вклад автора;
2. соответствие в Актика-аппарате;
3. формальное вложение (где применимо).

Шесть групп, 37 точек.

1. Досократы и античность

1.1 Анаксимандр (≈ 610–546 до н.э.)

Фрагмент B1 DK: τὸ ἄπειρον — беспредельное — как начало (ἀρχή) всех вещей. Ключ: ἄπειρον не вещь; Анаксимандр описывает его как "из чего происходят все сущие и во что они возвращаются", т.е. как активный процесс, порождающий и поглощающий определённости.

Соответствие: $\varepsilon_\mathrm{Apeiron}$ с $\varepsilon = \Omega$ — дуал $\alpha_\mathrm{Apeiron}$ (каталог Diakrisis). Апейрон — acting primordial, не субстрат.

1.2 Гераклит (≈ 540–480 до н.э.)

Фрагменты B12 DK ("в одну реку нельзя войти дважды") и B30 DK ("космос — огонь вечно живой, мерами возгорающийся..."): онтология процесса. Логос — σοφία-в-действии.

Соответствие: динамика-первичнее-статики. Объекты как временные стабильности потока. Формально: любой $\alpha$ есть ε-фаза $\mathsf{A}$-траектории; $\mathsf{A}$-итерация первична перед её фиксированными точками.

1.3 Парменид (≈ 515–450 до н.э.) — негативный контрапункт

Парменид-тезис: только $\tau\grave{o}\; \check{o}\nu$ (бытие) истинно; становление — иллюзия. Это точка, в которой ОЦ отделяется от ДЦ. Исторически западная традиция двинулась за Парменидом; Гераклит оставался маргинальным до Гегеля/Бергсон.

Актика восстанавливает гераклитову линию без отрицания парменидовой: 108.T — обе истинны, как дуалы.

1.4 Платон, Софист 253d

$\delta\iota\acute{\alpha}\kappa\rho\iota\sigma\iota\varsigma$ как «наука различения»: ἡ διακριτική ἐπιστήμη. Платон явно говорит о акте разделения сущего на роды, не об «объекте различения». Само имя проекта (Диакрисис) фиксирует эту позицию.

Соответствие: $\varepsilon_\mathrm{math} = \varepsilon_\mathrm{разл}$ — выделенный акт различения — и есть «математика» в исполнении.

1.5 Аристотель, Метафизика Θ

δύναμις (dynamis) / ἐνέργεια (energeia):

• dynamis — способность/возможность;
• energeia — осуществление/актуальность;
• ἐνέργεια онтологически первичнее: «актуальность определяет возможность, не наоборот» (Meta Θ.8, 1049b5).

Это прямой аристотелианский предок нашей формулы: α = δύναμις, ε(α) = ἐνέργεια.

Формальное вложение: Аристотелева схема встраивается в Актика как пара функторов $\mathrm{dyn} \dashv \mathrm{en}$ (coadjunction) с условием $\mathrm{en} \circ \mathrm{dyn} \simeq \mathrm{id}$.

1.6 Плотин

Ennead V.1: Единое излучает себя как акт (ἐνέργεια) — не как вещь, но как порождающее действие. Нус, Душа — последующие ступени этого активного излучения.

Соответствие: иерархия $\mathsf{A}^k(\varepsilon_0)$ с $\varepsilon_0 = \varepsilon_\mathrm{Apeiron}$: каждая ступень — активация предыдущей.

2. Раннемодерная линия

2.1 Спиноза (1632–1677)

Этика I, опр. 6: natura naturans — природа в акте порождения — vs natura naturata — природа как порождённые вещи. Conatus (II, пред. 7): каждая вещь стремится сохраниться в своём существовании — это не свойство, а активность бытия.

Соответствие: natura naturans = $\rangle\!\rangle \cdot \langle\!\langle$ (метакатегория актов); natura naturata = $\langle\!\langle \cdot \rangle\!\rangle$ (артикуляций); их соединение — 108.T.

2.2 Лейбниц (1646–1716)

Монадология §11: «монада есть чистая активность» (acte pur). Vis activa как центральное понятие метафизики. Субстанция = непрерывное действие.

Соответствие: элементарные единицы $\rangle\!\rangle \cdot \langle\!\langle$ — монада-как-акт, не монада-как-объект.

2.3 Кант (1724–1804)

Критика чистого разума: спонтанность рассудка — акт синтеза, который предшествует любой данности. Категории как правила действия синтеза, не как объекты.

Соответствие: синтез Канта = 2-морфизм в $\rangle\!\rangle \cdot \langle\!\langle$, порождающий единство аппрегензии.

2.4 Фихте (1762–1814)

Grundlage der gesamten Wissenschaftslehre (1794): Tathandlung — «акт-дело». Это акт, который в момент осуществления конституирует свой субъект и свой объект одновременно. Я полагает не-Я и себя самого в одном акте.

Tathandlung — прототип 108.T: артикуляцию и энактмент нельзя разделить иначе, чем в ретроспективном анализе; они со-даны (co-given).

Формальное соответствие: Tathandlung = coequalizer пары (articulate, enact) в $(\infty, \infty)$-категории.

2.5 Гегель (1770–1831)

Дух как процесс самосознания. Диалектика: тезис-антитезис-синтез — триадный акт. Наука логики: категории выводятся друг из друга движением понятия.

Соответствие: гегелева триада = эндо-2-функторная цепь в $\rangle\!\rangle \cdot \langle\!\langle$ (активация, отрицание-активация, синтез-активация); аналогична $\mathsf{M}^k$-итерациям в ОЦ.

2.6 Шеллинг (1775–1854)

Система трансцендентального идеализма (1800): безусловное = чистая продуктивность природы, акт без предпосылок. Позднее — философия откровения как событие.

Соответствие: $\varepsilon_\mathrm{Apeiron}$-акт как безусловное; ε-иерархия выше $\Omega$ — откровение как выход за $(∞, ∞)$.

3. Процесс-философия и прагматизм

3.1 Бергсон (1859–1941)

L'évolution créatrice (1907): durée — длительность — первичная онтологическая реальность. Интеллект объективирует (даёт α); интуиция схватывает процесс (даёт ε). Élan vital — творческая активность жизни.

Ключ: Бергсон явно отказывает первичности дискретных объектов. «Время — ткань реальности; пространственные объекты — наши искусственные срезы её».

Соответствие: durée = $\mathsf{A}$-траектория $\mathsf{A}^\infty(\varepsilon_0)$; интуиция = естественный интерфейс $\rangle\!\rangle \cdot \langle\!\langle$; интеллект = 108.T articulate-функтор в $\langle\!\langle \cdot \rangle\!\rangle$.

3.2 William Джеймс (1842–1910)

Essays in Radical Empiricism: «pure experience» — первичный поток. Различения субъект/объект, акт/объект — продукты опыта, не предпосылки.

3.3 Пирс (1839–1914)

Прагматическая максима: «значение концепции состоит из всех практических следствий её». Знание = habits of action. Триада (знак, объект, интерпретант) — интерпретант есть действие, активирующее знак-объект связь.

Соответствие: Peircean triad — это pre-categorical форма пары articulate/enact; ε(α) = полный паттерн interpretants α.

3.4 Дьюи (1859–1952)

Experience and Nature: опыт = двойное движение undergoing-doing. Знание — не пассивное отражение, а инструмент действия.

3.5 Уайтхед (1861–1947) — ключевой

Process and Reality (1929): актуальные события — атомарные события — это первичная реальность. Объекты («вечные объекты») — абстракции из паттернов актуальные события. Схватывание — акт схватывания одного occasion другим — базовая операция.

Уайтхед даёт нам:

• $\varepsilon_\mathrm{prehend}$ как фундаментальный акт в $\rangle\!\rangle \cdot \langle\!\langle$;
• сращение — процесс оформления актуальное событие — как $\mathsf{A}$-итерация;
• nexus — сеть связанных occasions — как $\rangle\!\rangle \cdot \langle\!\langle$-диаграмма.

Теорема 115.T (Уайтхед-coordinate): квантовые измерения имеют естественное представление как prehension-события в $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{quantum}$.

3.6 Хайдеггер (1889–1976)

Bytie und Zeit: Dasein — бытие, для которого его собственное бытие есть вопрос. Структура заботы (Sorge). Позднее — Ereignis (событие): бытие не «есть», а «событийствует».

Соответствие: Ereignis = 2-морфизм в $\rangle\!\rangle \cdot \langle\!\langle$, который со-производит то, что он связывает.

3.7 Мерло-Понти (1908–1961)

Phénoménologie de la perception: восприятие — телесное действие, не пассивная регистрация. Тело как «intentional arc». Смысл — не в объекте, а в моторно-перцептивной связке.

3.8 Симондон (1924–1989)

L'individu et sa genèse (1958): индивидуация — процесс, из которого возникает индивид. Индивид — стабилизированная фаза, не первичная сущность. Транс-индивидуация — продолжающееся становление через отношения.

Симондон — прямой предшественник нашей пары α/ε: индивид = α, индивидуация = ε(α).

3.9 Делёз (1925–1995)

Différence et répétition (1968): различие как активное самоутверждение, не негация. Ризома vs дерево — операционное, не структурное. Линии ускользания.

Соответствие: deleuzian difference = не-отождествляющее 2-морфизм в $\rangle\!\rangle \cdot \langle\!\langle$; rhizome = non-wellfounded объект Актика-природы.

4. Феноменология + биосемиотика XX века

4.1 Бейтсон (1904–1980)

Mind and Nature (1979): «паттерн, соединяющий» (the pattern which connects). Мышление — не в индивидуальном субъекте, а в паттернах отношений.

Соответствие: паттерн Бейтсон = 2-морфизм в $\rangle\!\rangle \cdot \langle\!\langle$, соединяющий индивидуальные акты в когерентное целое.

4.2 Матурана и Варела

Автопоэзис and Cognition (1972): живая система = самовоспроизводящая активность. Жизнь определяется операционально, через замкнутость производственных процессов.

Теорема 111.T (автопоэзис characterization): $X$ — autopoietic ⟺ $X$ — неподвижная точка $\mathsf{A}$ в соответствующей подкатегории:

$$X \in \mathrm{Fix}(\mathsf{A}) \cap \rangle\!\rangle \cdot \langle\!\langle^\mathrm{biological}.$$

4.3 Варела (1946–2001) — энактивизм

The Embodied Mind (1991, совм. с Томпсон, Rosch): энактивизм — познание = сенсомоторное сопряжение. Мир не «воспринимается»; он энактируется в коупе с организмом.

Это прямо даёт нам имя: enactment в $\rangle\!\rangle \cdot \langle\!\langle$ — технический термин для того, что Варела назвал философски. Без Варела наша терминология была бы невозможна.

4.4 Evan Томпсон

Mind in Life (2007): когнитивный акт — эволюционное продолжение метаболического. Консервирование жизни и схватывание мира — одно движение.

5. Русско-советская линия — в полной широте

5.1 Выготский (1896–1934)

Мышление и речь (1934): высшие психические функции возникают через интериоризацию социальных актов. Сначала act-between-people, потом act-within-person.

Соответствие: культурная интериоризация = функтор из коллективного $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{social}$ в индивидуальный $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{personal}$.

5.2 Леонтьев А.Н. (1903–1979)

Теория деятельности. Молярная единица психики — деятельность (activity), не ощущение и не представление. Иерархия: деятельность → действия → операции.

Соответствие: эта трёхуровневая иерархия = ε-стратификация в Актика (ε = ω² / ω·k / ω).

5.3 Бернштейн Н.А. (1896–1966)

О построении движений: движение — целенаправленное действие, координированное на нескольких уровнях, не рефлекс. Уровни A-E (от тонуса до символической координации).

5.4 Анохин П.К. (1898–1974)

Теория функциональных систем: acceptor of the result of action — предвосхищающий нервный аппарат, который формирует модель будущего результата до его осуществления.

Анохинский акцептор = $\mathsf{A}$-предсказание в $\rangle\!\rangle \cdot \langle\!\langle$: акт включает модель своего ожидаемого исхода.

5.5 Щедровицкий Г.П. (1929–1994) — СМД

Системо-мыследеятельность: мышление + коммуникация + действие как единое функциональное целое. Мыследеятельность — не редукция к одному из трёх, а синтез.

Теорема 122.T (SMD-embedding): Щедровицкая троица вкладывается как синхронизированная тройка $(\varepsilon_\mathrm{think}, \varepsilon_\mathrm{communicate}, \varepsilon_\mathrm{act})$ с обязательствами согласованности:

$$\varepsilon_\mathrm{think} \sqsupset \varepsilon_\mathrm{communicate} \sqsupset \varepsilon_\mathrm{act}, \quad \text{все три в общем pullback-диаграммe}.$$

5.6 Мамардашвили М.К. (1930–1990)

Лекции по античной философии: акт мысли = онтологическое событие. «Мысль состоится только если она себя актуализирует».

5.7 Мартынов Ф.Т.

Универсальный семантический код (УСК): значения — действия в семиотическом пространстве. Грамматика выведена из акт-структуры, не постулирована.

5.8 Бахтияров О.Г.

Активное сознание, Психонетика: практика непосредственной работы с сознанием как с активностью, не как с содержанием.

5.9 Боярин М. — Актика

Прямой предшественник нашего проекта: Актика как теория действия-первичного мышления. Наш раздел 12-actic/ именно развёртывает актику в формально-категорной рамке.

5.10 Чурилов Е. — Метастемология

Управляемая эпистемология → метастемология. Разбор в 07-beyond-metastemology.md.

6. Формально-логическая ДЦ-линия — критически важная

Главное дополнение к Чурилову: формально-логическая ДЦ-традиция внутри самой математики.

6.1 Брауэр (1881–1966)

Интуиционизм: доказательство = ментальный акт конструирования. Математика — не описание платонических объектов, а продукт творческой активности математика (the creative subject).

Брауэр требует: утверждение «существует $x$ с $P(x)$» означает я могу построить такой $x$. Не: в платонической сфере есть такой $x$.

Формальное вложение: Теорема 116.T (Брауэр-embedding). BHK-interpretation доказательств вкладывается в $\rangle\!\rangle \cdot \langle\!\langle$ как $\varepsilon_\mathrm{construct}$-семейство; intuitionistic logic = syntactic shadow этого AC-аппарата.

6.2 Гейтинг (1898–1980)

BHK-интерпретация (Брауэр-Гейтинг-Колмогоров):

• proof of $A \wedge B$ = pair (proof of $A$, proof of $B$);
• proof of $A \vee B$ = choice + proof of chosen;
• proof of $A \to B$ = метод преобразования proof of $A$ в proof of $B$;
• proof of $\exists x. P(x)$ = (свидетель $x$, proof of $P(x)$);
• proof of $\forall x. P(x)$ = метод produces proof of $P(x)$ для любого $x$.

Заметьте: «метод» и «преобразование» — это акты. BHK не о объектах-доказательствах, а о способах доказывать — т.е. о enactments.

6.3 Gentzen (1909–1945)

Natural deduction: правила введения/удаления как акт-схемы. Левое введение $\to$ есть акт «использовать предположение»; правое — акт «сделать предположение». Структурные правила (weakening, contraction) — акты менеджмента ресурса.

Соответствие: sequent calculus sequents = объекты $\rangle\!\rangle \cdot \langle\!\langle$; правила вывода = 1-морфизмы; cut-elimination = $\mathsf{A}$-фиксточка.

6.4 Лоренцен (1915–1994) — диалогическая логика

Dialogische Logik: доказательство = диалог между Proponent и Opponent. Pr утверждает; Op критикует; правила определяют, кто выигрывает когда. Логически истинное утверждение = Pr имеет выигрышную стратегию.

Теорема 117.T (Лоренцен-embedding) (усиленный вариант из 00-foundations): диалогическая игра $G_A$ для утверждения $A$ = объект $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{dial}$; Pr-стратегии = выделенные sub-hom; истинность $A$ ⟺ непустота этого sub-hom.

6.5 Curry (1900–1982), Howard (1926–2017)

Соответствие Curry–Howard: программа = доказательство. Процесс вычисления программы = акт доказательства. Типы = формулы; термы = доказательства; редукция = устранение сечения (cut-elimination).

Сама формулировка Curry–Howard — акт-центрична: доказательство — это процесс редукции, а не статический объект.

6.6 Мартин-Лёф (1942–)

Intuitionistic Type Theory (1984): значение типа = что значит его построить. Фраза «meanings are practices» (лекции 1985, опубл. в Meanings of the logical constants 1996) — философский стержень.

Теорема 118.T (Мартин-Лёф meanings-as-practices):

$$\mathrm{Meaning}(T) = \varepsilon(\alpha_T),$$

где $\alpha_T$ — тип как артикуляция, $\varepsilon(\alpha_T)$ — его enactment как практика.

6.7 Жирар (1947–) — ludics

Le point aveugle (2006–2007): ludics — proof theory, переосмысленная как теория интеракции. Доказательства — designs — объекты с branching выборов; proof composition = interaction между designs.

Ludics — самая зрелая формально-логическая ДЦ-теория на сегодняшний день. Она даёт:

• designs как acts;
• interaction как $\mathsf{A}$-активация;
• daimons как specific acts of giving up;
• orthogonality = coherence between acts.

Теорема 117.T (Жирар-ludics correspondence, усилен): $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{interact}$ — полная под-2-категория, обитающая ludics-designs; $\mathsf{A}$ — normalization-через-interaction; ortho-condition = 2-морфизм-когерентность.

Жирар в 2017-18 говорил: «Logic is a theater of actions» — точнейшая цитата философии Актика.

6.8 Abramsky (1953–)

Игровая семантика для языков программирования: программы — стратегии в играх. С Хайленд, Ong, Nickau: полная абстрактность PCF через игры.

6.9 Хинтикка (1929–2015), Väänänen (1953–)

Теоретико-игровая семантика: $A$ — истинно ⟺ Verifier имеет выигрышную стратегию в соответствующей игре $G_A$.

Теорема 119.T (Хинтикка-correspondence): $\models A \Leftrightarrow$ Verifier $\triangleright G_A$; игра $G_A$ = объект $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{dialogue}$; стратегия = 1-морфизм; истинность = непустота hom-множества.

6.10 Хьюитт (1944–) — Actor Model

Actors (1973): вычисление = сообщения между акторами. Нет состояния вне актов; акторы — первичные сущности.

Теорема 120.T (Actor-embedding): акторы Хьюитт = объекты $\rangle\!\rangle \cdot \langle\!\langle^\mathrm{concurrent}$; сообщение = 1-морфизм; causal-order = $\sqsupset_\kappa$.

6.11 Милнер (1934–2010)

CCS (1980), π-calculus (1989, совм. с Parrow, Walker): процессы — первичны, не значения. Значения — только на каналах коммуникации.

6.12 Хоар (1934–) — CSP

Communicating Sequential Processes (1978): процесс = последовательность коммуникационных актов.

6.13 Plotkin (1946–)

Структурная операционная семантика: значение программы = правила редукции. Не: программа обозначает математический объект; а: программа действует через набор редукций.

7. Синтез — почему все 37 точек образуют одну линию

Несмотря на разнообразие словаря, все 37 авторов согласны в одном методологическом принципе:

Действие / акт / процесс — онтологически и/или эпистемологически первичнее, чем объект / вещь / структура. Последние — стабилизации, остановки, абстракции из первого.

Формально это — одно утверждение: ε предшествует α. Актика-формализация 108.T делает это равенством (дуальность), не строгим неравенством (первенство). Мы идём дальше, чем любой из 37: они утверждали первенство; мы доказываем эквивалентность.

8. Вложение всех 37 традиций в Актика — таблица

Автор	Ключевой концепт	Актика-соответствие	Теорема
Анаксимандр	ἄπειρον	$\varepsilon_\mathrm{Apeiron}$, $\varepsilon = \Omega$	корень каталога
Гераклит	логос-процесс	$\mathsf{A}$-итерация	общий
Платон	διάκрисис	$\varepsilon_\mathrm{math}$	имя теории
Аристотель	energeia/dynamis	пара $\mathrm{en} \dashv \mathrm{dyn}$	108.T
Плотин	Единое-акт	$\mathsf{A}^k$-иерархия	каталог
Спиноза	natura naturans	$\rangle\!\rangle \cdot \langle\!\langle$	108.T
Лейбниц	vis activa	монада-акт	общий
Кант	спонтанность	2-морф. синтеза	108.T
Фихте	Tathandlung	coequalizer articul./enact	108.T основа
Гегель	триада	цепь $\mathsf{A}^3$	114.T
Шеллинг	безусловное	акт сверх $\Omega$	каталог
Бергсон	durée	$\mathsf{A}^\infty$	115.T
Джеймс	pure experience	$\rangle\!\rangle \cdot \langle\!\langle$-background	общий
Пирс	prag. максима	triad = pre-108.T	108.T
Дьюи	experience	undergoing-doing dual	108.T
Уайтхед	актуальные события	$\varepsilon_\mathrm{prehend}$	115.T
Хайдеггер	Ereignis	co-producing 2-морф.	108.T
Мерло-Понти	bodily action	энактивный слой	108.T
Симондон	индивидуация	α/ε прямая	108.T
Делёз	различие	non-id 2-морф.	108.T
Бейтсон	pattern connects	2-морф. coherence	108.T
Матурана-Варела	автопоэзис	$\mathrm{Fix}(\mathsf{A})$	111.T
Варела	энактивизм	имя enactment	foundation
Томпсон	mind-in-life	extended автопоэзис	111.T
Выготский	интериоризация	social→personal $\rangle\!\rangle \cdot \langle\!\langle$	122.T
Леонтьев	деятельность	3-ур. ε-стратификация	122.T
Бернштейн	уровни движения	ε < ω..ω stratification	общий
Анохин	acceptor	$\mathsf{A}$-предсказание	108.T
Щедровицкий	СМД	triple sync	122.T
Мамардашвили	мысль-событие	$\varepsilon_\mathrm{think}$	122.T
Мартынов	УСК	акт-семантика	118.T
Бахтияров	актив. сознание	$\varepsilon_\mathrm{aware}$	общий
Боярин	Актика	весь 12-actic раздел	foundation
Чурилов	Метастемология	subtheory	07-beyond-metastem.
Брауэр	intuitionism	$\varepsilon_\mathrm{construct}$	116.T
Гейтинг	BHK	meanings-as-methods	118.T
Gentzen	natural deduction	sequents as $\rangle\!\rangle \cdot \langle\!\langle$	117.T
Лоренцен	диалогика	$\rangle\!\rangle \cdot \langle\!\langle^\mathrm{dial}$	117.T
Curry-Howard	proofs-as-progs	process-reduction	118.T
Мартин-Лёф	meanings-as-pract.	$\mathrm{Meaning} = \varepsilon$	118.T
Жирар	ludics	$\rangle\!\rangle \cdot \langle\!\langle^\mathrm{interact}$	117.T
Abramsky	игровая семантика	игра=$\rangle\!\rangle \cdot \langle\!\langle$-диаграмма	119.T
Хинтикка	game-sem.	winning=hom-nonempty	119.T
Хьюитт	actors	actor=$\rangle\!\rangle \cdot \langle\!\langle^\mathrm{conc}$	120.T
Милнер	π-calculus	process=object	120.T
Хоар	CSP	comm. seq.	120.T
Plotkin	SOS	rules as acts	117.T

9. Заключение

Актика — не отдельный вклад, а синтез 37+ традиций в один формальный каркас. Значимость дуальной теоремы 108.T именно в том, что она делает все эти традиции формально согласованными, не требуя отказа ни от одной. Метастемология Чурилова охватывает 5 из 37 точек (русскоязычные + частично формально-логические через эвалы); Актика охватывает все 37 и добавляет $(\infty, \infty)$-категорную инфраструктуру, которой у предшественников не было.

10. Ссылки

• /12-actic/00-foundations — главное введение Актика.
• /12-actic/02-dual-primitive — формальное ядро.
• /12-actic/04-ac-oc-duality — полное доказательство 108.T.
• /12-actic/07-beyond-metastemology — вложение Чурилова.
• /12-actic/08-formal-logical-dc — Брауэр-Мартин-Лёф-Жирар в деталях.