Глава 5. Со-определение A и ¬ A

Различие против разделения

Откуда мы пришли

К началу настоящей главы цепь, прослеженная в Главах 1–4, дошла до своего завершающего звена. Из пред-формального первоначала $A = \exists$ был выделен акт различения как первое формализуемое; этот акт получил запись Distinction с четырьмя полями (Глава 2); из структуры записи были выведены законы $L 1$ – $L 5$ (Глава 3); после законов были введены принципы $P 1$ – $P 4$ и структура $E / R / R$ как следующий онтологический слой, а в Главе 4 — и её метафизическое применение к Абсолюту.

Архитектурно эти звенья образуют цепь

A = \exists \to ‘ D i s t in c t i o n ‘ \to L 1 - L 5 \to P 1 - P 4 \to E / R / R .

При этом, как было отмечено в Главах 3 и 4, в текущей формализации звенья этой цепи представлены разными файлами и не всегда сведены в одну единую теорему: вывод $L 1$ – $L 5$ из Distinction и вывод $P 1$ – $P 4$ из законов суть формальные теоремы, тогда как мост $P 1$ – $P 4 \to E / R / R$ есть архитектурная интерпретация, а применение $E / R / R$ к Абсолюту — метафизический, а не машинно-проверенный шаг. Настоящая глава не двигает цепь дальше. Она возвращается к её первому звену — к записи Distinction — и развёртывает то, что в её устройстве было зафиксировано, но не было полностью раскрыто содержательно. А именно: положительная и отрицательная стороны акта различения не есть две отдельные вещи, которые потом как-то соотнесены. Они со-возникают в самом акте, и это со-возникновение — не вспомогательное замечание о Distinction, а центральное свойство структуры.

\sloppypar В § 2.6 настоящей работы это было обозначено как невозможность построить Distinction, имея лишь одну из сторон. Тогда наблюдение играло минималистскую роль — оно входило в общую проверку минимальности записи: каждое поле необходимо. Сейчас, после того как вся деривационная цепь развёрнута, та же структурная особенность получает другое значение: она есть содержательное выражение того, что отрицание в Теории Систем — не операция над уже готовым, а аспект первичного акта. Это — основная позиция настоящей главы, и её развёртывание требует сначала зафиксировать, чем со-определение отличается от всех других видов связи между сторонами.

Начнём с противопоставления двух установок: разделения готового и различения в одном акте.

Две установки: разделение и различение

В стандартной установке к работе с противоположностями мир состоит из готовых объектов. Существует объект $A$ — частица, утверждение, понятие. С этим объектом можно произвести операцию отрицания. В результате операции получается другой объект — $\neg A$ — который по построению есть «то, что не $A$ ». Структурно эта установка имеет три такта:

Дан объект $A$ — сам по себе, без $\neg A$ .
Применяется операция отрицания: $\neg (\cdot)$ .
Получается второй объект $\neg A$ — сам по себе, как результат применения операции.

Время в этих трёх тактах не имеет физического значения; речь идёт о логическом порядке: сначала есть $A$ , потом — $\neg A$ как производное. Назовём эту установку разделением готового: работа с двумя объектами, один из которых первичен, а второй получен из первого операцией.

В установке, разворачиваемой в ToS, картина иная. Нет первичного объекта $A$ , к которому затем применяется операция, дающая $\neg A$ . Есть акт различения, в котором обе стороны — то, что выделяется, и то, относительно чего оно выделяется, — возникают совместно. Структурно эта установка имеет один такт:

Совершается акт различения; в этом акте $A$ и $\neg A$ заданы одновременно как две стороны одного устройства.

Назовём эту установку различением в одном акте: работа с одной структурой, имеющей две стороны как свои аспекты, а не как два самостоятельных объекта, связанные между собой производным образом.

Разделение готового и различение в одном акте — это не два описания одной операции. Это две разные онтологические установки относительно того, что такое отрицание и каков статус его сторон.

В первой установке отрицание есть действие над объектом; во второй — структурное условие того, что объект вообще может быть обозначен как $A$ . В первой $A$ может мыслиться отдельно от $\neg A$ ; во второй такое отдельное мышление невозможно, поскольку без указания того, чем $A$ не является, само $A$ ещё не выделено.

Возражение: разве это не одно и то же

Первое возражение к различию двух установок состоит в следующем. Допустим, есть операция отрицания $\neg (\cdot) : P r o p \to P r o p$ . Применённая к $A$ , она даёт $\neg A$ . Но ведь сама эта операция определена так, что $\neg A$ и $A$ взаимно исключительны и совместно исчерпывают пространство возможностей. Разве не получается то же, что и в одном акте? Зачем вводить разницу между двумя установками, если результат один и тот же?

Различие здесь не в результате, а в онтологическом статусе объектов. В установке разделения готового $A$ есть до применения операции: оно мыслится как осмысленный объект сам по себе, его свойства могут быть установлены и зафиксированы, и лишь после этого совершается действие, дающее $\neg A$ . В установке различения в одном акте $A$ не имеет осмысленного статуса до акта различения: до того, как выделено, чем $A$ не является, нет и самого $A$ как определённости. Существует только пред-формальная неразличённость, разобранная в § 2.1.

Это различие имеет конкретные следствия. Если $A$ есть до $\neg A$ , то можно ставить вопрос: «каковы свойства $A$ , рассматриваемого изолированно, без отсылки к $\neg A$ ?». Этот вопрос имеет смысл в рамках разделения готового — ибо $A$ как готовый объект имеет собственные свойства. В рамках различения в одном акте этот вопрос не имеет содержания: говорить об $A$ без $\neg A$ — значит говорить о том, что ещё не выделено как определённость, то есть о пред-формальном, к которому формальные предикаты не применяются.

Со-определение: определение в строгом смысле

Чтобы дальнейшая работа была точной, зафиксируем, что именно подразумевается под со-определением.

Со-определение — это структурная одновременность задания, при которой ни одна из сторон не может быть указана раньше другой ни порядком конструкции, ни логическим выводом, ни эпистемическим доступом.

Это определение требует уточнений по трём направлениям, поскольку со-определение легко спутать с тремя другими видами связи между объектами.

Со-определение и взаимная зависимость. В взаимной зависимости есть два объекта $X$ и $Y$ , существующих самостоятельно, между которыми установлено отношение, по которому каждый зависит от другого. Например, давление и объём газа в изотермическом процессе связаны соотношением $P V = const$ : зная одно, можно определить другое. Но $P$ и $V$ как физические величины существуют сами по себе — они могут быть измерены по отдельности, у них есть размерность, они могут фигурировать в других уравнениях независимо. Взаимная зависимость — это отношение, наложенное на уже-существующие объекты.

Со-определение в нашем смысле другое. Положительная и отрицательная стороны акта различения не имеют статуса сами по себе, между которыми затем устанавливается отношение. Они появляются как стороны одного устройства, и вне этого устройства не существуют как определённости. Метафорически: $P$ и $V$ — два предмета на столе, связанные верёвкой; положительная и отрицательная стороны — два конца одной верёвки, и вне неё нет ни концов, ни сторон.

Со-определение и эквивалентность. В классической логике эквивалентность утверждает: $P ⟺ Q$ , то есть $P$ имеет место тогда и только тогда, когда имеет место $Q$ . Это — симметричное отношение между двумя пропозициями, которые обе осмысленны вне эквивалентности. Можно спросить о $P$ отдельно — доказуемо ли оно, ложно ли оно, в каких моделях оно выполняется. Эквивалентность лишь фиксирует, что эти вопросы получают один и тот же ответ для $P$ и для $Q$ .

Со-определение — не эквивалентность. Положительная и отрицательная стороны акта различения не эквивалентны — они, напротив, взаимно исключительны (поле exclusive). Но именно через эту взаимную исключительность они и определяют друг друга: что значит $positive D$ — определяется тем, что это есть не $negative D$ , и обратно. Эквивалентность — это отношение между независимо осмысленными пропозициями; со-определение — это совместное обретение ими осмысленности.

Со-определение и взаимная выводимость. Можно представить ситуацию, где из утверждения $A$ формально выводится утверждение $B$ , и обратно. Например, в группах: «элемент $g$ коммутирует со всеми элементами» и « $g$ принадлежит центру группы» — два утверждения, взаимно выводимых друг из друга по определению центра. Каждое из них использует понятия, уже введённые в теории групп, и каждое осмысленно само по себе как утверждение об элементе $g$ . Выводимость — это логический шаг, совершаемый на уже определённых утверждениях.

Со-определение работает на одну ступень глубже — там, где формальный вывод ещё не может быть совершён, поскольку самих определённостей, между которыми мог бы быть совершён вывод, ещё нет. Со-определение задаёт сами эти определённости; формальный вывод возможен лишь после того, как со-определение совершено.

Итог трёх различений можно записать так. Взаимная зависимость есть отношение между готовыми объектами. Эквивалентность есть отношение между готовыми пропозициями. Взаимная выводимость есть формальный шаг на готовых утверждениях. Со-определение есть одновременное обретение двумя сторонами своей определённости в одном структурном акте; всё перечисленное предполагает уже-произошедшее со-определение и работает на его результате.

Связь с § 2.6

В § 2.6 настоящей работы было показано, что нельзя построить Distinction, имея лишь положительную сторону без отрицательной, и наоборот. Технически это было выражено через структуру конструктора mkDistinction, требующего все четыре поля одновременно: ни одно из полей нельзя предъявить без остальных.

Этот вывод был получен в контексте обсуждения минимальности записи: каждое поле необходимо, ни одно нельзя удалить без потери структуры. Со-определение тогда выступало как одно из четырёх наблюдений о невозможности удаления, наряду с обсуждением полей exclusive и exhaustive.

Сейчас та же структурная особенность рассматривается в другой роли — не как одно из четырёх частных наблюдений, а как общая онтологическая позиция относительно отрицания. Положительное и отрицательное со-определяются — это не частное и техническое свойство записи Distinction; это следствие того, как ToS видит саму операцию отрицания: как аспект первичного акта, не как операцию над готовым объектом.

Где в книге работает разделение, а где — различение

Не следует понимать различение двух установок как полемическое: будто установка разделения готового — неправильная, а установка различения в одном акте — правильная. Обе установки имеют свою область применения.

Разделение готового — естественная установка во всех ситуациях, где объекты уже существуют и операция отрицания применяется к ним как к данности. Когда математик пишет $\neg (x = y)$ , он опирается на $x = y$ как на уже-определённое утверждение, и его отрицание есть осмысленная операция, дающая другое утверждение. Это рабочее правило классической логики, и оно остаётся в силе.

Различение в одном акте — более глубокая установка, работающая на другом уровне. Она отвечает на вопрос: откуда вообще берётся определённость $x = y$ как таковая, которая затем может быть подвергнута отрицанию? Ответ: из акта различения, в котором $x = y$ и $\neg (x = y)$ со-возникают как две стороны устройства; только после этого со-возникновения можно работать с одной из сторон, применяя к ней формальные операции.

ToS не отменяет работу классической логики на её уровне; ToS углубляет её, указывая на структуру, без которой эта работа была бы невозможна. Различение между установками — это различение между рабочим уровнем формальной логики (разделение готового) и онтологическим основанием этой работы (различение в одном акте). Подробное соотношение этих двух уровней — центральное содержание § 5.4 настоящей главы.

Зафиксировав концептуальное различие между разделением и различением и определив со-определение в строгом смысле, мы можем теперь обратиться к тому, как это различие выражено в самой записи Distinction — как формальное устройство, в котором четыре поля задаются одним конструктором, требующим их одновременного предъявления.

Формальное выражение со-определения

Запись как одновременное предъявление четырёх полей

В § 5.1 со-определение было зафиксировано как структурная одновременность задания: ни одна сторона различения не может быть указана раньше другой ни порядком конструкции, ни логическим выводом, ни эпистемическим доступом. Сейчас покажем, как эта одновременность выражена в записи Distinction — не как комментарий о её свойстве, а как структурное устройство самого типа.

Напомним запись:

Record Distinction := mkDistinction {
  positive   : Prop;
  negative   : Prop;
  exclusive  : ~ (positive /\ negative);
  exhaustive : positive \/ negative
}.

Существенно следующее. Record в Rocq — это конструкция, которая для построения экземпляра требует одновременного указания значений для всех объявленных полей. Нельзя предъявить два поля, а два других оставить ненаписанными: тогда у CIC нет экземпляра — есть лишь намерение его построить, не доведённое до конца. Только в момент, когда все четыре поля positive, negative, exclusive, exhaustive заданы конкретными значениями, конструктор mkDistinction успешно применяется и порождает экземпляр типа Distinction.

Этот факт — не особенность Rocq, а общее свойство записей в типизированных языках. Запись формально определяет, что экземпляр есть четвёрка значений, согласованных по типам. Четвёрка без одного элемента не есть четвёрка с пропущенным четвёртым — это ничто, ещё не построенный объект.

Зависимая типизация: связь полей внутри записи

В записи Distinction четыре поля не равноправны структурно. Поля positive и negative — обычные значения типа Prop. Но типы полей exclusive и exhaustive зависят от уже заданных значений positive и negative:

Тип поля exclusive есть $\neg (‘ p os i t i v e ‘ \land ‘ n e g a t i v e ‘)$ . Это выражение не имеет смысла, пока positive и negative не указаны: $\land$ и $\neg$ нужно к чему-то применять.
Тип поля exhaustive есть $‘ p os i t i v e ‘ \lor ‘ n e g a t i v e ‘$ . То же замечание: дизъюнкция требует обе стороны как конкретные пропозиции.

Этот вид типизации — стандартная конструкция CIC, в которой типы поздних полей записи могут ссылаться на значения ранних полей. Здесь она даёт следующее структурное следствие: нельзя построить поле exclusive в отрыве от полей positive и negative, поскольку самый тип этого поля упоминает оба. Аналогично для exhaustive.

Содержательно это означает, что взаимная исключительность и совместная исчерпанность — не самостоятельные утверждения, существующие сами по себе и потом «приставленные» к двум сторонам. Они — утверждения о двух сторонах, и без сторон у них нет предмета. Структурно это та же связь, что между « $x$ больше $y$ » и самими $x, y$ : без $x$ и $y$ утверждение о сравнении не имеет смысла. В записи Distinction эта связь зафиксирована не в комментариях и не в неформальных пояснениях, а в самой системе типов.

Конструктор `mkDistinction` как единый акт

Применение конструктора mkDistinction есть формальный единый акт построения экземпляра. Сигнатура конструктора такова:

‘ mk D i s t in c t i o n ‘ : \forall (p n : P r o p), \neg (p \land n) \to (p \lor n) \to ‘ D i s t in c t i o n ‘.

Конструктор принимает четыре аргумента, идущих один за другим, и возвращает экземпляр типа Distinction. Применение конструктора с тремя аргументами — ещё не экземпляр; это частично применённая функция, которая ждёт четвёртый аргумент. Только при подаче всех четырёх аргументов получается готовый Distinction.

Это означает следующее. В системе типов может существовать частично применённый конструктор — например, выражение mkDistinction P — но это не экземпляр Distinction: это корректный терм функционального типа, ожидающий остальные аргументы. Чего в системе типов нет — так это объекта типа Distinction, в котором была бы задана только положительная сторона, а отрицательная, exclusive и exhaustive — нет. Либо есть завершённый экземпляр Distinction со всеми четырьмя поданными и согласованными по типам компонентами, либо есть незавершённое применение конструктора — функция, а не экземпляр. Промежуточного объекта <<Distinction с одной лишь стороной>> в CIC не бывает.

Завершённый экземпляр Distinction — это формальное выражение того, что в § 5.1 было названо различением в одном акте. Не объект с одной стороной, к которому потом добавляется вторая, а экземпляр, для которого все четыре компонента интегрально требуются сразу.

Стоит подчеркнуть: синтаксический порядок аргументов конструктора ( $p$ перед $n$ , оба перед exclusive, и так далее) есть особенность записи. Структурно все четыре компонента одинаково необходимы для завершённого экземпляра; синтаксический порядок их перечисления не есть онтологический порядок появления сторон.

Случай `distinction_of P`: одна пропозиция,

        обе стороны

В записи Distinction стороны $‘ p os i t i v e ‘$ и $‘ n e g a t i v e ‘$ — два независимых поля. В принципе можно указать их совершенно различными пропозициями, если только exclusive и exhaustive удастся доказать. Но в Rocq есть конструкция, которая по произвольной пропозиции $P$ одним действием строит соответствующее различение:

Definition distinction_of (P : Prop) : Distinction :=
  mkDistinction
    P                               (* positive   *)
    (~ P)                           (* negative   *)
    (fun H => match H with          (* exclusive  *)
              | conj p np => np p
              end)
    (classic P).                    (* exhaustive *)

В этом случае — наиболее показательном для темы со-определения — все четыре поля порождаются из одного аргумента $P$ :

Поле positive есть $P$ .
Поле negative есть $\neg P$ — не как «второй объект», который мы каким-то отдельным образом ввели, а как синтаксическая инверсия того же $P$ , типа Prop, через логическую связку $\neg$ .
Поле exclusive есть * конструктивное* доказательство несовместности $P$ и $\neg P$ — лямбда-выражение $λ H . match H with ⟨ p, n p ⟩ \Rightarrow n pp$ , которое работает для любого $P$ без обращения к каким-либо аксиомам.
Поле exhaustive есть применение классической аксиомы classic: $P \lor \neg P$ . Эта аксиома — предмет отдельного обсуждения, к которому настоящая работа вернётся в последующей главе об аксиоматическом слое.

Что показывает distinction_of P: для построения канонического различения по $P$ нужна одна пропозиция $P$ плюс принятый в ToS принцип $L 3$ , формально представленный как аксиома classic. Отрицательная сторона $\neg P$ и доказательство несовместности exclusive строятся без дополнительных содержательных данных — прямо из устройства логических связок. А вот совместная исчерпанность exhaustive не строится конструктивно: она требует $L 3$ , то есть обращения к classic. Поэтому точная формула такова: одна пропозиция $P$ задаёт обе стороны и их несовместность; их совместная исчерпанность добавляется принципом $L 3$ .

Иными словами: акт различения, формализованный в Distinction, запускается от одной пропозиции — но с самого начала содержит обе стороны и обе связки между ними. Не «есть $P$ , потом добавим $\neg P$ и связки», а: «есть $P$ , и это значит, что есть $P$ , $\neg P$ , их несовместность и их исчерпанность — одно структурное целое, описываемое экземпляром типа Distinction».

Что значит «со-определение встроено в тип»

Сведя сказанное, получаем следующее.

В типизированных языках программирования и в системах формального вывода типа Rocq то, что нельзя построить — значит то, чего нет в смысле формальной системы. Не «существует, но запрещено к построению», а не существует как объект данного типа. Это не моральный запрет и не методическая рекомендация — это структурное свойство типа.

Применительно к Distinction это означает: экземпляр этого типа с одной стороной без другой не существует. Не существует в Rocq, не существует в CIC, не существует в любой системе, реализующей запись с зависимыми полями. Не как факт эмпирический, проверяемый перебором, а как факт о типе: сама форма Record с такими типами полей этого не допускает.

Со-определение положительного и отрицательного — не дополнительное свойство, которым Distinction обладает; это устройство, которым Distinction является.

Между этими формулировками — существенное различие. Свойство объекта — это утверждение, которое для объекта можно доказать или опровергнуть. Устройство — это то, без чего объект перестаёт быть собой. Если у Distinction убрать со-определение сторон (скажем, разрешить экземпляры с одной стороной), это будет не Distinction с уменьшенным числом свойств, а другой тип — который ToS не использует, потому что он не выражает структуру акта различения.

Зафиксировав, что записано в типе, обратимся теперь к обратной стороне того же наблюдения: что именно невозможно построить, если попытаться обойтись без одной из сторон или без одной из связок.

Невозможность односторонней `Distinction`

От положительного содержания к запрету

В § 5.2 было зафиксировано положительное содержание со-определения: запись Distinction устроена так, что её четыре поля задаются одновременно, типы полей exclusive и exhaustive зависят от positive и negative, а конструктор mkDistinction есть единое применение, принимающее все четыре аргумента сразу. Это — что записано в типе.

Сейчас рассмотрим обратную сторону того же наблюдения: что невозможно построить, если попытаться обойтись без одной из сторон или без одной из связок между ними. Этот разбор не вводит новых структур; он лишь разворачивает следствия того, что зафиксировано в § 5.2 — но именно через разбор того, чего сделать нельзя, становится особенно отчётливо видно, насколько со-определение не есть дополнительное свойство Distinction, а есть способ его существования.

Что значит «невозможно» в типизированной системе

В разговорной речи «невозможно построить» может звучать как риторический оборот — мол, никто пока не построил, или построение слишком сложно. В системе типов CIC это — точное технико-теоретическое утверждение.

Когда мы говорим, что нельзя построить экземпляр Distinction без отрицательной стороны, мы имеем в виду следующее: не существует выражения в языке CIC, которое имело бы тип Distinction и при этом обходилось без указания значения поля negative. Не существует ни как программа, ни как доказательство, ни как любая иная форма терма — проверка типов в любой корректной реализации CIC, включая Rocq, отвергнет любое такое выражение как синтаксически некорректное.

Невозможность в системе типов есть структурная, не эмпирическая невозможность. То, что не имеет правильного типа, не существует как объект данного типа — независимо от усилий, времени и изобретательности.

Это — важный момент. В Главе 3 законы $L 1$ – $L 5$ были выведены как теоремы о произвольной Distinction — утверждения, которые держатся на каждом экземпляре. В § 5.3 настоящей главы мы переходим к другому виду утверждений: о самом существовании экземпляров. Эти утверждения работают не на уровне свойств Distinction, а на уровне условий возможности быть экземпляром этого типа. Соответственно, они доказываются не через вывод теоремы, а через прямой структурный анализ типа.

Невозможность без отрицательной стороны

Предположим, мы хотим построить экземпляр Distinction, имея лишь положительную сторону — некоторую пропозицию $P$ — и не вводя отрицательную. Структурно это означает: подать конструктору mkDistinction один аргумент $P$ и попытаться получить экземпляр.

Подача mkDistinction P даёт не Distinction, а частично применённую функцию ожидающую остальных аргументов. Чтобы перейти от этой функции к экземпляру, нужно подать ей вторую пропозицию — значение поля negative. Без этой пропозиции конструктор не может быть полностью применён, и никакого экземпляра не возникает.

Можно возразить: «а если просто пропустить поле negative, например, оставить его незаполненным?». В типизированной системе такого действия нет. negative объявлено как поле типа Prop; в момент применения конструктора это поле должно получить конкретное значение типа Prop. Слова «оставить незаполненным» не имеют формального аналога: либо у поля есть значение, либо конструктор не применён.

Можно возразить иначе: «а если положить negative равным True — то есть подать в качестве отрицательной стороны тождественно истинное утверждение?». Этот случай содержательно поучителен. Конструктор mkDistinction — к нему перейдём через шаг — требует ещё и доказательств exclusive и exhaustive с типами, упоминающими обе стороны. Если positive есть $P$ , а negative есть True, то exclusive должен иметь тип $\neg (P \land ‘ T r u e ‘)$ , что равносильно $\neg P$ . Это уже не утверждение об устройстве различения, а просто утверждение об истинности $\neg P$ — которое в общем случае ложно. Следовательно, подача True как отрицательной стороны не строит различение для произвольного $P$ — она работает только тогда, когда $\neg P$ имеет место.

Содержательно это означает: если мы пытаемся пропустить «реальное» отрицание — $\neg P$ — и подсунуть на роль отрицательной стороны любое другое утверждение, то либо запись не строится (типы exclusive и exhaustive не доказуемы), либо она строится, но не выражает различение по $P$ : она выражает различение по чему-то другому. Само Distinction без содержательной отрицательной стороны не получается ни в каком смысле.

Невозможность без поля `exclusive`

Перейдём к двум другим полям. Поле exclusive имеет тип $\neg (‘ p os i t i v e ‘ \land ‘ n e g a t i v e ‘)$ — утверждение о взаимной несовместности сторон. Что произойдёт, если попытаться построить запись без этого поля?

Структурно: невозможно, потому что записи Distinction без этого поля просто нет в CIC. Но рассмотрим более интересный сценарий: представим, что мы определили другой тип — скажем, WeakDistinction — с тремя полями вместо четырёх, без exclusive. Что мы потеряем?

По теореме L2_from_distinction¹ поле exclusive в записи Distinction тождественно есть закон $L 2$ для данного экземпляра: $\neg (‘ p os i t i v e ‘ D \land ‘ n e g a t i v e ‘ D)$ . Иными словами, не отдельное утверждение, выводимое из чего-то ещё, а само поле записи есть структурная реализация $L 2$ на этом экземпляре.

Соответственно, удаление поля exclusive означает: на полученной структуре закон $L 2$ перестаёт держаться структурно — полученный тип допускает экземпляры, в которых положительная и отрицательная стороны могут быть совместны.

Но если стороны различения могут быть совместны, то это уже не различение. Содержательно: если $P$ и $\neg P$ могут одновременно иметь место, то нет того зазора между ними, который делает $P$ и $\neg P$ двумя сторонами, а не одной размытой ситуацией. Запись без exclusive описывает не акт различения с двумя сторонами, а совмещение — структуру, в которой обе пропозиции присутствуют без отчётливого отделения. Это не Distinction — это другая, вырожденная конструкция.

Невозможность без поля `exhaustive`

Симметричная картина с полем exhaustive. Его тип — $‘ p os i t i v e ‘ \lor ‘ n e g a t i v e ‘$ . По теореме L3_from_distinction² это поле тождественно реализует $L 3$ на экземпляре.

Удаление поля exhaustive даёт тип, на котором $L 3$ структурно не держится: возможны ситуации, когда ни положительная, ни отрицательная сторона не имеет места — между ними появляется «третье», некий зазор, не покрываемый ни одной из сторон.

Содержательно: если ни $P$ , ни $\neg P$ не имеют места, то $P$ ещё не выделено как определённое утверждение — ни в своём утверждении, ни в своём отрицании. Это — пред-формальная размытость, разобранная в § 2.1: ситуация до акта различения. Запись без exhaustive описывает не акт различения, а его отсутствие; не разделение с границей, а раздвоение без полного покрытия.

Объединяя два предыдущих подраздела: exclusive запрещает наложение сторон, exhaustive запрещает зазор между ними. Без обоих этих запретов положительная и отрицательная стороны не есть две стороны одного различения — они есть просто две пропозиции, которые могут что угодно делать друг с другом.

Лемма `co_constitution` и точная формальная опора

        со-определения

В Rocq-репозитории ToS³ есть лемма, носящая имя со-определения:

Lemma co_constitution : forall P : Prop,
  (P -> exists Q, Q = ~P) /\ ((~P) -> exists Q, Q = P).

Здесь требуется точность относительно того, что именно эта лемма доказывает. Её доказательство в репозитории — split; intro H; eexists; reflexivity — тривиально, и тривиальность эта показательна: предпосылки $P$ и $\neg P$ в нём фактически не используются. С тем же успехом доказуемы и более простые утверждения $\forall P, \exists Q, Q = \neg P$ и $\forall P, \exists Q, Q = P$ . Поэтому co_constitution не является сильным доказательством со-определения в смысле зависимости истинности или осмысленности сторон. Её содержание скромнее: как только пропозиция $P$ дана как объект языка, выражение $\neg P$ уже синтаксически доступно как пропозиция. Это — минимальный синтаксический след со-определения, а не полная формализация центрального тезиса главы.

Точную формальную опору тезиса главы дают другие утверждения — о связи сторон внутри полного экземпляра Distinction. В любом Distinction отрицательная сторона логически эквивалентна отрицанию положительной, и наоборот:

negative D <-> ~ positive D и positive D <-> ~ negative D.

Эти эквивалентности доказываются из полей записи: направление negative D -> ~ positive D следует из поля exclusive (несовместность сторон), а обратное ~ positive D -> negative D — из поля exhaustive (исчерпанность). Именно они прямо выражают то, что говорит глава: стороны не заданы синтаксически одна через другую, но в полном различении они логически со-определены через два правила, exclusive и exhaustive.⁴

Существенно, что эти эквивалентности — именно логические эквивалентности ( $\leftrightarrow$ ), а не синтаксические равенства пропозиций. Формально мы получаем negative D <-> ~ positive D, но не negative D = ~ positive D: переход от $P \leftrightarrow Q$ к $P = Q$ потребовал бы отдельного принципа (пропозициональной экстенсиональности), который в базовых аксиомах ToS не принят. Это различение важно: стороны со-определены логически, но не отождествлены синтаксически.

Со-определение и пять законов

Сводя сказанное в трёх предыдущих подразделах, получаем:

Без отрицательной стороны экземпляр Distinction не строится — сами типы полей exclusive и exhaustive требуют её упоминания.
Без поля exclusive структурно теряется $L 2$ , и запись описывает совмещение, не различение.
Без поля exhaustive структурно теряется $L 3$ , и запись описывает раздвоение с зазором, не различение.

Все три «без» приводят не к ослабленной Distinction, а к другой структуре, не выражающей акт различения. Со-определение сторон — не одно из свойств Distinction, которое можно изолировать и аккуратно ослабить; оно сцеплено с теми самыми структурными законами, через которые Distinction является тем, что она есть.

Особенно важно следующее наблюдение, и здесь требуется точность относительно того, что фиксирует формализация. В файле Distinction.v единая теорема five_properties_of_distinction утверждает, что для всякой $D : ‘ D i s t in c t i o n ‘$ держатся четыре свойства различения: устойчивость ( $L 1$ ), исключительность ( $L 2$ ), исчерпанность ( $L 3$ ) и самообоснование ( $L 4$ ). Пятый закон $L 5$ в эту теорему не входит: $L 5$ касается иерархии уровней и не является свойством отдельного экземпляра $D$ . Он добавляется в файле LawsFromDistinction.v — объединяющая теорема five_laws_from_distinction там подключает иерархический слой, причём $L 5$ в ней представлен иррефлексивностью базового уровня и от конкретного $D$ не зависит (как было разобрано в Главе 3).⁵

Это наблюдение имеет существенный смысл в свете настоящего раздела: если бы со-определение не было встроено в структуру, можно было бы построить Distinction, на которой часть свойств держится, а часть — нет. Но именно потому, что со-определение не отделимо от устройства записи, любое успешное построение экземпляра сразу даёт все четыре структурных свойства $L 1$ – $L 4$ ; иерархический $L 5$ при этом обеспечивается отдельным слоем формализации.

Со-определение сторон и удержание структурных свойств $L 1$ – $L 4$ — не два независимых свойства Distinction, а одно структурное обстоятельство, рассмотренное с двух сторон: со стороны сторон и со стороны законов.

Что показывает невозможность

Перейдём от перечисления невозможностей к ответу на вопрос: что показывает эта невозможность в целом, как философское наблюдение о работе ToS.

Невозможность односторонней Distinction означает, что нет содержательной ступени, на которой акт различения имел бы лишь одну сторону без другой. В частности:

Нет ступени «есть положительная сторона, но отрицательная ещё не возникла». Эта ступень — грамматически формулируемая — структурно не реализуется.
Нет ступени «есть две стороны, но они ещё не разделены». Эта ступень также невозможна: разделение есть само поле exclusive, без которого нет двух сторон, а есть две произвольные пропозиции.
Нет ступени «есть две стороны, разделённые, но между ними что-то ещё». Эта ступень исключена полем exhaustive: третьего нет.

Иными словами: в ToS невозможно описать «частичное» различение, в котором какая-то часть структуры есть, а другая ещё не пришла. Акт различения либо есть, и тогда есть все четыре поля и все пять структурных следствий — либо его нет, и тогда мы имеем пред-формальную размытость, к которой Distinction как тип неприменим.

Этот вывод имеет важное методологическое следствие, к которому обратимся в § 5.4: операция отрицания в ToS не работает на «отдельно взятых» утверждениях. Она работает только на утверждениях, уже вовлечённых в акт различения — то есть на полях positive и negative некоторого экземпляра Distinction. Это значит, что отрицание не есть операция, применяемая после, а есть аспект устройства, дающего обозначениям статус осмысленных пропозиций.

Зафиксировав, что обходиться без одной из сторон или без одной из связок структурно невозможно, перейдём к развернутому обсуждению самой операции отрицания — к различению двух её ролей: классической операции, действующей на готовых утверждениях, и аспекта первичного акта, делающего эти утверждения возможными.

Отрицание: операция или аспект

Постановка различения

В предыдущих разделах настоящей главы было показано, что положительная и отрицательная стороны акта различения со-определяются в одном структурном акте. Сейчас сделаем следующий шаг: рассмотрим, что это со-определение означает для самого понятия отрицания. В обычном обращении с логикой отрицание понимается одним способом — как операция, превращающая одно утверждение в другое. В ToS обнаруживается, что у отрицания есть два различных статуса, которые в стандартной постановке не различаются, но онтологически работают на разных уровнях.

Эти два статуса можно обозначить так:

Отрицание как операция — действие, которое применяется к уже-данной пропозиции и возвращает новую пропозицию.
Отрицание как аспект — одна из двух сторон акта различения, не получаемая применением действия, а со-возникающая с другой стороной.

Утверждение, развиваемое в настоящем разделе: оба статуса работают в ToS, но на разных уровнях. Операция вторична; аспект первичен. Между ними — не противоречие, а структурное соотношение.

Развернём оба статуса последовательно.

Классическая операция $\neg : P r o p \to P r o p$

В классической и интуиционистской логике, а также в их реализации в CIC, отрицание — это синтаксическая операция. Формально:

\neg : P r o p \to P r o p, \neg P = def P \to ⊥.

То есть: отрицание пропозиции $P$ есть утверждение << $P$ влечёт ложь>>. Здесь важна точность по Карри–Ховарду: доказательство $\neg P$ — это функция, которая из любого предполагаемого доказательства $P$ строит элемент пустого типа $⊥$ , то есть выводит противоречие. Формула $\neg P$ есть объектное утверждение $P \to ⊥$ внутри CIC, а не мета-утверждение <<у $P$ нет доказательства>>: эти два прочтения важно не смешивать — $\neg P$ говорит о наличии функции $P \to ⊥$ , а не об отсутствии чего-либо. Определение задано через стрелку и тип $⊥$ (пустой тип, тождественно ложная пропозиция).

С этой операцией работают так. Сначала дана некоторая пропозиция $P$ — например, «натуральное число $n$ простое» (для какого-то конкретного $n$ ). Затем к этой пропозиции применяется $\neg$ , и получается новая пропозиция $\neg P$ — « $n$ не простое». Доказательство того, что конкретное $n$ — например, $n = 4$ — не является простым, есть конструкция терма типа $\neg P$ , то есть конструкция функции из $P$ в $⊥$ — то есть способа из предположения « $4$ простое» вывести противоречие (например, через предъявление разложения $4 = 2 \cdot 2$ , противоречащего определению простоты).

В такой постановке отрицание есть:

двухместная связь: оно соотносит две пропозиции — исходную $P$ и производную $\neg P$ ;
асимметричная: $P$ есть до $\neg P$ — именно потому, что $\neg P$ получается применением к $P$ ;
определимая: $\neg P$ задана формулой через $\to$ и $⊥$ , и не требует никакой дополнительной структуры, кроме уже имеющегося в CIC аппарата.

Эта операция корректна, работает, и используется в ToS-репозитории на каждом шагу. В частности, в выражении distinction_of P отрицательная сторона задаётся именно как $\neg P$ — применение классической операции к $P$ . Никакого спора с классическим отрицанием ToS не ведёт.

Отрицание как роль в записи `Distinction`

Но рядом с операцией работает другой статус отрицания, зафиксированный в самой записи Distinction. Рассмотрим сигнатуру записи ещё раз:

Record Distinction := mkDistinction {
  positive   : Prop;
  negative   : Prop;
  exclusive  : ~ (positive /\ negative);
  exhaustive : positive \/ negative
}.

В этой сигнатуре поле negative имеет тип Prop — то есть оно есть просто пропозиция, наряду с полем positive. Поле negative не определено как $\neg‘ p os i t i v e ‘$ . В сигнатуре нет уравнения вида:

‘ n e g a t i v e ‘ = \neg‘ p os i t i v e ‘.

В принципе, при построении конкретного экземпляра Distinction поля positive и negative могут быть совершенно произвольными пропозициями — лишь бы удалось предъявить доказательства exclusive и exhaustive.

Конструкция distinction_of P есть один частный способ построить Distinction — способ, при котором отрицательная сторона задаётся именно как $\neg P$ . Но запись Distinction сама по себе не требует, чтобы negative было результатом применения $\neg$ к positive. Запись требует лишь, чтобы две стороны были взаимно исключительны и совместно исчерпывающи — условия, которые могут быть удовлетворены разными способами.

В записи Distinction поле negative — это позиция, синтаксически независимая от поля positive. Запись задаёт роль; способ её заполнения — отдельный вопрос, решаемый при актуализации, не самой записью.

Синтаксический и логический уровни

Сделанное наблюдение требует существенного уточнения, без которого оно может быть понято слишком сильно. Уточнение касается двух разных уровней, на которых работает соотношение между positive и negative.

Уровень синтаксиса. На уровне синтаксиса CIC поля positive и negative в записи Distinction независимы. В сигнатуре нет уравнения, связывающего их. При построении конкретного экземпляра можно подать в negative любую пропозицию — лишь бы удалось предъявить доказательства exclusive и exhaustive. Запись не пишет «negative есть отрицание positive»; она оставляет открытым, чем будет negative в каждом конкретном случае.

Уровень логики. На уровне логического содержания дело обстоит иначе. Из доказательств exclusive и exhaustive — то есть из самих требований к взаимной исключительности и совместной исчерпанности — следует, что negative и $\neg‘ p os i t i v e ‘$ логически эквивалентны.

Это утверждение легко проверить структурно. Если exclusive утверждает $\neg (‘ p os i t i v e ‘ \land ‘ n e g a t i v e ‘)$ , а exhaustive — $‘ p os i t i v e ‘ \lor ‘ n e g a t i v e ‘$ , то их совокупность эквивалентна утверждению $‘ n e g a t i v e ‘ \leftrightarrow \neg‘ p os i t i v e ‘$ :

Из negative следует $\neg‘ p os i t i v e ‘$ — это переформулировка exclusive (если positive, то не negative, и контрапозитивно).
Из $\neg‘ p os i t i v e ‘$ следует negative — это прямое применение exhaustive: одна из сторон обязана иметь место, и если не положительная, то отрицательная.

Иными словами: любые две пропозиции, удовлетворяющие exclusive и exhaustive относительно positive, оказываются логически эквивалентны $\neg‘ p os i t i v e ‘$ . Содержательно negative всегда есть отрицание positive, даже если синтаксически оно записано иначе.

Что именно показывает запись. Наблюдение, которое делает запись Distinction — не в том, что содержательно negative отличается от $\neg‘ p os i t i v e ‘$ . Содержательно они совпадают, и это совпадение есть прямое следствие требований к взаимной исключительности и совместной исчерпанности. Наблюдение в другом: роль «отрицательная сторона» задана в записи независимо от операции $\neg$ . Запись говорит: «есть две позиции, удовлетворяющие таким-то условиям». Операция $\neg$ есть один из способов задать содержимое второй позиции, исходя из содержимого первой — и в случае distinction_of именно так дело и обстоит. Но запись не определяет вторую позицию через операцию; запись определяет вторую позицию через её структурную роль в акте различения.

Синтаксически negative независимо от $\neg‘ p os i t i v e ‘$ ; логически — эквивалентно ему. Запись Distinction фиксирует синтаксический уровень: роль «отрицательная сторона» вводится независимо от операции $\neg$ , хотя по содержанию они в любом экземпляре совпадают.

Зачем нужно это различение

Возникает естественный вопрос: если на логическом уровне negative и $\neg‘ p os i t i v e ‘$ совпадают, имеет ли значение их синтаксическая независимость? Можно ли просто принять, что negative есть $\neg‘ p os i t i v e ‘$ , и упростить запись?

Значение имеет. Различение синтаксического и логического уровней фиксирует, что понятие отрицательной стороны не выводится из понятия положительной через применение операции. Это — не техническое замечание о синтаксисе CIC; это онтологическое утверждение о статусе двух сторон в акте различения.

Структурное следствие первое. Если бы negative было определено как $\neg‘ p os i t i v e ‘$ синтаксически, то отрицательная сторона была бы производной конструкцией над положительной — то, что получается, когда к positive применили операцию. Это — именно та установка разделения готового, которая была разобрана в § 5.1: сначала $A$ , потом $\neg A$ как результат действия.

Запись Distinction оставляет обе стороны в равном синтаксическом статусе: ни одна не есть «результат операции над другой». Это согласуется с установкой различения в одном акте: обе стороны со-возникают как стороны структуры, не как объект и его производное.

Структурное следствие второе. В $E / R / R$ -разборе («Связь с E/R/R: уровень схемы и уровень экземпляра») имена полей positive и negative на уровне схемы записи суть ролевые слоты. Если бы negative синтаксически зависело от positive, то слот <<отрицательная сторона>> концептуально сводился бы к операции над содержимым слота <<положительная сторона>>. Это смешивало бы уровень ролевых слотов и уровень их наполнения: слот есть имя позиции, тогда как операция работает с содержимым позиций. Синтаксическая независимость полей позволяет сохранить это разделение чистым.

Структурное следствие третье. Возможны другие структуры в ToS — не Distinction — где аналогичная картина «две стороны, со-возникающие как стороны устройства» обнаруживается, но нет операции, через которую одна сторона выражалась бы синтаксически через другую. Запись Distinction в её синтаксической независимости полей служит образцом для таких структур; если бы Distinction была написана через negative $=$ $\neg‘ p os i t i v e ‘$ , она была бы вырожденным случаем, не показательным для общего паттерна.

Связь с E/R/R: уровень схемы и уровень экземпляра

Сделанное наблюдение получает точную формулировку в терминах $E / R / R$ -разбора, развёрнутого в Главе 4. Здесь, однако, необходимо явно развести два уровня чтения записи — иначе возникнет видимое противоречие с формализацией.

Дело в том, что слова positive и negative обозначают две разные вещи: имя поля в схеме записи и значение этого поля в конкретном экземпляре. На уровне схемы записи Distinction как типа имена полей positive и negative — это ролевые слоты, позиции <<положительная сторона>> и <<отрицательная сторона>>. На уровне же конкретного экземпляра $D : ‘ D i s t in c t i o n ‘$ значения positive $D$ и negative $D$ — это конкретные пропозиции, и именно они суть элементы E/R/R-разбора: файл ERRFromDistinction.v определяет список элементов как err_elements D = [ positive D; negative D ]. Соответственно, итоговая разметка двухуровневая:

Компонент	Уровень	E/R/R-категория
`positive`, `negative` (имена полей схемы)	схема записи	Roles (слоты)
`positive` $D$ , `negative` $D$ (значения)	экземпляр $D$	Elements
`exclusive` $D$ , `exhaustive` $D$	экземпляр $D$	Rules

Оба прочтения законны и не противоречат друг другу: они относятся к разным уровням. Когда настоящая глава говорит, что positive и negative — роли, речь идёт об уровне схемы: имя позиции (<<положительная сторона>>, <<отрицательная сторона>>) задаётся самой записью Distinction, тогда как наполнение позиции — конкретная пропозиция — появляется при актуализации, и на уровне экземпляра это наполнение есть элемент.

В разметке уровня схемы отрицательная сторона — это не <<противоположность>> положительной как готового объекта, а вторая позиция в одной структуре, симметричная первой. Обе позиции равноправны: ни одна не имеет онтологического первенства перед другой. Симметрия записи видна непосредственно из её сигнатуры — поля positive и negative оба объявлены одинаково (типа Prop), без указания, что одно есть <<исходное>>, а другое — <<полученное из исходного>>.

С точки зрения generative order (Глава 4): сначала задаются правила (тип Distinction, требования exclusive и exhaustive), затем распределяются роли (positive и negative как позиции), и лишь после этого в роли подбираются элементы (конкретные пропозиции при актуализации). Отрицание как операция работает на уровне Elements — когда уже есть пропозиция, ей сопоставляется другая через синтаксическое $\neg$ . Отрицание как аспект работает на уровне Roles — задаётся позиция, в которую затем может быть помещена пропозиция.

Соотношение операции и аспекта по уровням E/R/R

Существенно, что эти два статуса отрицания — операция и аспект — не противоречат друг другу и не конкурируют. Они работают на разных уровнях.

Уровень Elements (отрицание как операция). На этом уровне есть конкретные пропозиции — $P$ , $Q$ , « $n$ простое», « $n$ чётно», « $a$ делит $b$ » и т. д. Операция $\neg$ берёт пропозицию и возвращает другую пропозицию. На этом уровне работает классическая логика, и работает корректно. Все теоремы, доказывающие $\neg P$ для конкретного $P$ , остаются доказанными.

Уровень Roles (отрицание как аспект). На этом уровне ещё нет конкретных пропозиций — есть структура акта различения, в которой выделены две позиции. Эти позиции называются «положительная сторона» и «отрицательная сторона», но наполнение их — дело актуализации. На этом уровне отрицательная сторона не есть результат применения операции; она есть вторая позиция, со-существующая с первой по структуре акта.

Связь уровней. Когда совершается конкретный акт различения по пропозиции $P$ (то есть когда применяется distinction_of P), оба уровня совмещаются: конкретное наполнение позиций positive и negative даётся именно через применение операции $\neg$ к $P$ . В этом частном случае операциональное отрицание и аспектуальное отрицание совпадают по результату — но не по структуре, на которой они работают.

Классическое отрицание не отменяется. Оно встраивается в более общую структуру: операция $\neg$ есть один из способов заполнения роли negative, а не определение того, что эта роль есть.

Следствия для понимания операций в томе

Различение операции и аспекта имеет несколько важных следствий, к которым настоящая работа будет возвращаться в дальнейших частях.

Первое: статус операций как методологическая позиция. В стандартной математике принято говорить об «операциях» (сложение, умножение, отрицание, дифференцирование, проекция), как если бы они были первичными объектами, действующими на готовых элементах. ToS показывает, что у каждой такой операции — если её рассмотреть структурно — есть аспектуальный двойник: то, что операция делает, на более глубоком уровне есть раскрытие аспекта, уже встроенного в структуру. Отрицание здесь — простейший и наиболее показательный случай, поскольку оно встроено в саму запись акта различения.

Второе: примат структуры над процедурой. В формализме CIC экземпляр Distinction существует как целое с четырьмя полями — не как результат пошагового применения операций. Это согласуется с общей онтологической позицией ToS, разобранной в Главе 4: Rules первичны по отношению к Roles, а Roles — по отношению к Elements (generative order). Структура задаёт возможности процедур; процедуры не создают структуру.

Третье: ограничение на «операционализацию». Не всякую структуру можно адекватно описать через перечисление операций над её элементами. Если структура содержит со-определённые аспекты — как positive и negative в Distinction — то попытка представить эти аспекты как «объект и результат операции над ним» искажает структуру: упускается со-возникновение, неотделимое от самого устройства.

Различение операции и аспекта — частный случай более общей закономерности: то, что в формальной работе предстаёт как процедура, часто есть разворачивание уже-имеющейся структуры. Эта линия будет проходить через всю настоящую работу. В частности, в Части III (числовые системы) и в Части XI (групповые структуры) подобные наблюдения будут применены к таким операциям, как сложение и противоположный элемент группы.

Зафиксировав структурное различение операционального и аспектуального отрицания, перейдём к рассмотрению того, как со-определение положительного и отрицательного — как структурный факт акта различения — обнаруживается не только в формальной записи Distinction, но и в нескольких различных традициях философской и научной мысли, и в чём состоит сходящееся свидетельство этих независимых обнаружений.

Параллели и предвосхищения

Сходящиеся параллели

Интуиция со-определения сторон — идея, что противоположности не есть самостоятельные сущности, между которыми затем устанавливается отношение, а возникают как стороны одного устройства — не нова. Она проступает в нескольких традициях мысли, удалённых друг от друга по времени, языку и культурному контексту: в структурной лингвистике, гегелевской диалектике, классической китайской философии, в раннем буддизме. Эти традиции не общались между собой; они различны по методу, словарю и предмету. И тем не менее каждая из них — разными средствами и в разных терминах — приходит к одному и тому же структурному наблюдению.

Это сходство удалённых традиций мы рассматриваем как эвристическую параллель, а не как доказательную опору ToS: совпадение независимых перспектив повышает правдоподобие того, что наблюдение схватывает нечто структурное, но само по себе ничего не доказывает. Формальная сила тезиса главы лежит не в этих параллелях, а в устройстве записи Distinction, разобранном в предыдущих разделах.

Настоящая работа добавляет к этим параллелям нечто иной природы: формальное прослеживание со-определения в записи Distinction. Зависимые типы полей exclusive и exhaustive, требующих обе стороны для самой своей осмысленности, дают со-определению точную форму — независимо от того, как оно было видено у Соссюра, у Гегеля или в восточных текстах. Понимание этого формального результата удобно достигается именно на фоне традиций, в которых близкая структура была видна содержательно, но формализована быть не могла — не от недостатка усилий, а от отсутствия подходящего формального аппарата.

В настоящем разделе мы рассмотрим четыре традиции: соссюровскую структурную лингвистику, развившийся из неё структурализм Якобсона, гегелевскую диалектику и восточные традиции (инь-ян и взаимозависимое возникновение Нагарджуны). Каждая рассматривается коротко — ровно настолько, чтобы выделить ту точку, в которой она перекликается с со-определением, и ту точку, в которой её рассмотрение отличается от формального аппарата ToS. Подчеркнём заранее: это — параллели и предвосхищения, а не свидетельства в доказательном смысле.

Соссюр: значение через различие

Наиболее точная параллель к со-определению из всех рассматриваемых традиций обнаруживается у Фердинанда де Соссюра. В его Курсе общей лингвистики⁶ формулируется одно из центральных положений структурной лингвистики — о том, что в языке нет ничего, кроме различий.

Содержательное наполнение этого тезиса таково. Значение знака — слова, морфемы, любого языкового элемента — не есть свойство, присущее знаку самому по себе. Знак не имеет значения изолированно. Значение знака есть его позиция в системе других знаков — то, чем он отличается от соседних, конкурирующих с ним за роль в той же парадигме.

Пример Соссюра. Французское слово mouton и английское sheep обозначают одно и то же животное — овцу. Можно было бы подумать, что у этих двух слов одно и то же значение. Но в английском есть отдельное слово mutton для обозначения мяса овцы, а во французском — нет: то же mouton обозначает и животное, и его мясо. Значение английского sheep не равно значению французского mouton — именно потому, что sheep находится в системе с mutton, а mouton — в системе, где такого противопоставления нет. Значение sheep конституируется отличием от mutton; без этого отличия значение было бы иным.

Структурное содержание. Главное в позиции Соссюра — не тезис о произвольности знака (это другая, отдельная линия), а тезис о реляционной природе значения. Знак не имеет содержания в отрыве от системы; содержание знака есть его роль в системе различий, и эта роль не может быть указана без указания других ролей.

Это — структурное содержание, прямо параллельное тому, что показывает запись Distinction: положительная сторона не имеет содержания вне акта различения; её содержание есть её роль в устройстве, и эта роль не выделяется без указания отрицательной стороны.

Точка отличия. В чём состоит различие между обнаружением Соссюра и формальным обнаружением. Соссюр работает на уровне общего наблюдения о структуре значения; его аппарат — описательный, не формальный. У него нет записи, фиксирующей со-определение как конкретное структурное устройство. Тезис «в языке нет ничего, кроме различий» остаётся утверждением о языке вообще, не формализуемой конструкцией.

Запись Distinction даёт со-определению то, чего соссюровский аппарат не даёт: точную форму. Не общее положение, а конкретный тип в CIC, на котором можно работать формально — доказывать теоремы, выводить следствия, опираться в дальнейших конструкциях. Это не значит, что формальный результат <<идёт дальше>> соссюровского — это означает, что одна и та же структура видна с двух сторон: со стороны анализа значения и со стороны формального устройства. Оба прочтения — эвристически параллельны, указывают на один и тот же структурный мотив.

Структурализм Якобсона: бинарные оппозиции

Линия, заданная Соссюром, была развита в первой половине XX века в работах Романа Якобсона и Пражского лингвистического кружка. Якобсон показал, что в фонологии значения фонем выражаются через бинарные оппозиции: звук <<б>> в русском отличается от <<п>> одним признаком — звонкостью (во всём остальном они одинаковы), и вся фонологическая система языка может быть описана как пересечение нескольких таких оппозиций.

Структурно это та же картина, что и со-определение в Distinction: две стороны оппозиции имеют смысл только как стороны оппозиции, не как самостоятельные сущности — <<звонкость>> содержательна лишь в паре с <<глухостью>>. Якобсоновский материал по существу иллюстрирует то же реляционное устройство, что и соссюровский, только на фонологическом материале; поэтому мы ограничиваемся этим компактным указанием. Точка отличия от ToS та же, что у Соссюра: Якобсон работает в пределах лингвистической предметности, тогда как запись Distinction не привязана к языку и относится к самой структуре выделения определённости в любой области.

Гегель: диалектическое со-возникновение

Иная — более общая, но и более туманная — параллель к со-определению проступает у Гегеля. В Науке логики⁷ Гегель разворачивает то, что принято называть диалектическим движением понятий. Здесь требуется оговорка. В популярной рецепции гегелевская диалектика часто описывается через схему тезис–антитезис–синтез; но как краткое описание его собственного метода эта схема спорна и упрощает гегелевскую логику (сам Гегель этой триады в таком виде не формулировал). Для нас важна не эта схема, а более глубокий мотив — взаимная определённость противоположностей; именно его мы и выделяем в гегелевском материале.

Применительно к интересующей нас теме существенно следующее наблюдение Гегеля. Чистое бытие (Sein) и чистое ничто (Nichts), взятые в своей абсолютной неопределённости, у Гегеля оказываются тождественны: без всяких внутренних определений <<есть нечто>> и <<нет ничего>> одинаково пусты по содержанию. Их различие появляется лишь в становлении (Werden) — движении от одного к другому, в котором каждое получает определённость через противоположность. Бытие не есть до ничто; ничто не есть до бытия; оба со-возникают в едином движении становления.

Структурное содержание. Идея Гегеля, в её абстрактной форме, прямо резонирует с со-определением: противоположности не существуют как готовые объекты, между которыми затем устанавливается отношение. Они со-возникают в одном движении; их идентичность есть взаимное определение через противоположность.

Точка отличия первая: время. Гегелевское со-возникновение разворачивается во времени — в движении становления. Это — временная структура. Distinction в ToS не разворачивается во времени: четыре поля интегрально требуются для одного экземпляра, построенного одним применением конструктора mkDistinction. Со-определение в ToS — структурно мгновенно, не процессуально.

Это различие существенно. У Гегеля противоположности можно мыслить как «возникающие друг из друга» в смысле движения мысли; в ToS противоположности заданы в одном такте, и нет «движения», в котором одна предшествует другой. Гегелевская картина допускает интерпретацию, в которой временная последовательность важна; ToS такую интерпретацию исключает — структура акта различения не имеет внутренней последовательности.

Точка отличия вторая: снятие. У Гегеля движение тезиса и антитезиса завершается снятием (Aufhebung) — особым переходом, в котором противоположности сохраняются и одновременно преодолеваются в синтезе. В ToS никакого снятия нет. Положительная и отрицательная стороны акта различения остаются двумя сторонами; они не сливаются в синтез и не образуют третью сущность над собой. Distinction имеет ровно две стороны, и закон $L 3$ исключает «третье».

Точка отличия третья: формализация. Гегелевская диалектика, при всей её влиятельности, никогда не была формализована. Попытки её формализации — от Маркса до современных аналитических разборов — остаются интерпретациями, не превращающими гегелевские категории в работающий формальный аппарат. Distinction есть конкретная запись с конкретными правилами; гегелевское со-возникновение остаётся содержательной интуицией, не формальной структурой.

Сводя сказанное: у Гегеля видна структура со-определения, и Гегель её достаточно глубоко проговаривает — но проговаривает её в рамке, в которой работает время, снятие и неформализуемая диалектика. В ToS та же структура обнаруживается в другой рамке — структурной, вневременно’{й}, формальной. То, что Гегель описывал как движение мысли, в формальной работе оказывается устройством структуры — но это два разных подхода к одному и тому же структурному факту, не присвоение гегелевской мысли формализмом.

Восточная традиция: метафорические предвосхищения

Корот-ко упомянём ещё две традиции, в которых интуиция со-определения видна особенно отчётливо, но в форме, далёкой от формализации.

Инь-ян в классической китайской философии. В И цзин⁸ и в позднейшей даосской мысли центральная пара инь и ян выступает не как два самостоятельных принципа, между которыми установлено противопоставление, а как две стороны одного устройства мира. Инь без ян не имеет смысла: тьма без света не есть тьма; женское без мужского не есть женское; пассивное без активного не есть пассивное. Каждое определяется через другое и не существует отдельно от него.

Эта формулировка — содержательно параллельная со-определению в Distinction — имеет в китайской традиции образный, не формальный характер. Она работает как способ смотреть на мир, не как формальный аппарат, в котором можно доказывать теоремы.

Пратитья-самутпада у Нагарджуны. В Муламадхьямака-карике Нагарджуны (II–III век н. э.)⁹ развёрнут принцип пратитья-самутпада — «взаимозависимое возникновение». Согласно этому принципу, никакая сущность не существует сама по себе; всякое существующее возникает в зависимости от других существующих и не имеет самостоятельной идентичности. Применительно к противоположностям это означает: ни одна противоположность не есть сама по себе; обе со-возникают как стороны взаимной зависимости.

И здесь параллель с со-определением — прямая. Но и здесь формализации нет: пратитья-самутпада — общефилософское положение о всех существующих, не конкретный тип в формальной системе.

Что общего, что различно. Восточные традиции — инь-ян и пратитья-самутпада — видят в со-определении общий принцип устройства существующего. Они выходят за пределы конкретных оппозиций (как у Соссюра и Якобсона) и за пределы конкретного движения понятий (как у Гегеля) к общеонтологической позиции: ничто не существует самостоятельно; всё определено через другое.

ToS в формальной части настоящего тома такого общеонтологического утверждения не делает. Distinction есть формализация конкретного акта различения, не утверждение о всём существующем. Формула <<ничто не существует самостоятельно; всё определено через другое>> для технически ориентированной главы слишком широка, и мы берём её только как эвристическую параллель, а не как доказательную опору ToS. Онтологическая позиция настоящей работы — которую разрабатывает Том I и которая проступает в Главе 4 о $E / R / R$ — по структуре перекликается с восточной: вся система $E / R / R$ работает так, что элементы системы получают свою определённость через Roles, а те — через Rules; ни один уровень не определён в отрыве. Та же структурная закономерность, которую восточные традиции видят в общем устройстве существующего, в ToS прослеживается формальным путём — не как заимствование восточной позиции и не как доказательство от неё, а как ещё одна эвристическая параллель к тому же структурному мотиву.

Что даёт формализация

Все четыре традиции — Соссюр, Якобсон, Гегель, восточные тексты — видят со-определение. Каждая описывает его своими средствами и в своих терминах. Каждая остаётся на уровне содержательной интуиции, философской позиции или описательной модели; ни одна не доводит со-определение до формальной записи, в которой оно стало бы работающим инструментом.

Что добавляет к этой картине формализация ToS.

Первое: точность. Формальная запись делает явным то, что в традициях оставалось размытым. Со-определение Соссюра — общий тезис о значении; со-определение у Гегеля — движение понятий; инь-ян — образ. Distinction есть конкретная структура с конкретными четырьмя полями и конкретной зависимостью между ними. Точность здесь не значит сужения — наоборот: точная форма обнаруживает структуру, которую размытые формулировки прятали.

Второе: проверяемость. Формальная запись позволяет доказывать утверждения о со-определении. Леммы, разобранные в § 5.3, и теоремы, выведенные в Главе 3 — это формальные результаты, имеющие силу в CIC. Соссюровское «в языке нет ничего, кроме различий» не есть теорема и не может быть доказано или опровергнуто; это — общее наблюдение. Утверждения ToS о со-определении суть формальные теоремы, проверяемые Rocq.

Третье: возможность развёртывания. Формальная запись позволяет строить на её основе дальнейшие конструкции. Distinction есть фундамент, на котором стоят законы $L 1$ – $L 5$ (Глава 3) и принципы $P 1$ – $P 4$ (Глава 4); на этой основе будут построены числовые системы (Часть III), функциональные пространства, групповые структуры и многое другое в последующих частях. Соссюр, Гегель, восточные тексты — каждый останавливался на со-определении как на наблюдении о структуре существующего; ToS делает со-определение рабочим инструментом, на котором строится последующее.

Формализация ToS не отменяет содержательных интуиций традиций и не присваивает их. Со-определение есть структурный факт акта различения, и ToS обнаруживает его так же независимо, как Соссюр обнаружил его в анализе значения, а Гегель — в анализе движения понятий. Формальная работа даёт этому одному и тому же структурному факту точную, проверяемую и развёртываемую форму — и тем самым делает доступным как аппарат то, что без формы оставалось содержательным наблюдением.

Зафиксировав место со-определения в традиции и природу того, что добавляет к нему формальное обнаружение в Distinction, перейдём к завершающему содержательному наблюдению настоящей главы — наблюдению о двух методологических установках, различение которых работает не только в формальной работе, но и в самом подходе к познанию.

Две методологические установки

Возврат к двум установкам

В § 5.1 настоящей главы было введено различие двух установок к работе с противоположностями — разделения готового и различения в одном акте. Это различие было введено в качестве концептуальной рамки, в которой затем разворачивались формальные наблюдения о записи Distinction (§ 5.2, § 5.3), о статусе отрицания (§ 5.4), и о сходящихся свидетельствах в традиции (§ 5.5).

Сейчас, в финальном разделе главы, та же концептуальная пара рассматривается с другой стороны: методологически — не как тезис о структуре акта различения, а как способ работать с определённостями в формальной деятельности. У этих двух установок есть конкретные следствия для того, как разворачивается работа математика, и эти следствия стоят отдельной фиксации — не как моральное наставление, а как методологическое наблюдение, которое будет применимо во всех последующих частях настоящего тома.

Различение в работе математика

Установка различения — когда работа ведётся в рамке «есть структура, у которой есть две стороны, со-определяющие друг друга» — проявляется в математической работе следующим образом.

Первое: введение объекта вместе с его дополнением. Когда математик вводит новый объект — класс, отношение, структуру — он одновременно вводит и то, относительно чего этот объект выделяется. Чётное число вводится не <<само по себе>>, а как одна сторона дихотомии чётно/нечётно — эта дихотомия точна для целых и натуральных чисел (для других структур её пришлось бы оговаривать отдельно). Простое число вводится не изолированно, а внутри классификации натуральных чисел, где рядом находятся составные числа — и особый случай единицы, которая не является ни простым, ни составным. Группа вводится вместе с её гомоморфизмами в другие группы — то есть с тем, чем эта конкретная группа отличается от других групп с тем же носителем. Категория, как мы увидим в Части VIII, вводится сразу с обоими аспектами — объектами и стрелками — которые не существуют один без другого.

Эта одновременность введения объекта и его дополнения не есть эстетическая черта — она есть структурное следствие того, что определённость объекта задаётся его местом среди соседних определённостей. Изолированное определение, не указывающее, чем объект отличается от соседних, — не определение, а имя.

Второе: проверка ролей при работе со структурой. В установке различения работа со структурой включает в себя проверку того, что роли в структуре заполнены согласованно. Это проверка типа «соответствуют ли элементы своим ролям?», «выполнены ли правила, удерживающие структуру?» — та самая проверка хорошей сформированности, разобранная в § 4.9.3 Главы 4 и связанная с $E / R / R$ -разбором.

В установке различения такие проверки естественны и регулярны: когда структура задана как устройство с ролями и правилами, естественно смотреть, выполнены ли правила. В установке разделения готового такие проверки нерегулярны: если объекты «уже даны», вопрос об их согласованности с ролями не возникает — роли вообще не работают.

Третье: сохранение связи между уровнями. Generative order (Глава 4) утверждает: правила задают роли, роли подбирают элементы. Эта последовательность не должна нарушаться. В установке различения связь между уровнями сохраняется: всякий конкретный объект работы держится с правилами и ролями, через которые он введён. В установке разделения связь может быть утрачена: объект, отделённый от своего структурного основания, теряет определённость — но эта потеря не сразу видна тому, кто пользуется объектом как готовым.

Разделение и потеря связи

Установка разделения готового — когда работа ведётся в рамке «есть готовые объекты, с которыми мы выполняем операции» — не есть ошибочная установка. Она работает на своём уровне, и большая часть повседневной математической работы происходит именно в ней. Когда вычисляют производную, доказывают теорему о пределах, решают дифференциальное уравнение — работают с объектами как с готовыми, не возвращаясь каждый раз к структурному вопросу о том, как эти объекты конституированы.

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

Первый сценарий: парадоксы. Парадокс Рассела¹⁰ возникает именно в установке разделения готового: «множество всех множеств, не содержащих себя» вводится как готовый объект, без проверки того, согласована ли эта запись со структурой уровней ( $P 1$ , иерархия). В установке различения такого объекта попросту не возникает — запись не проходит проверку хорошей сформированности ещё до того, как может возникнуть парадокс.

Второй сценарий: фрагментация формальных областей. Если различные формальные области — алгебра, анализ, топология, теория категорий — развиваются как замкнутые на себя дисциплины, без удержания связи между их основаниями, возникает фрагментация математического знания. Каждая область становится самостоятельной системой готовых объектов; связи между областями устанавливаются позднее, через специальные конструкции — функторы, эквивалентности, переводы. В установке различения эти связи присутствуют с самого начала: разные области суть разные актуализации одной структуры $E / R / R$ , и их связь не есть позднее добавление, а есть структурное обстоятельство.

Третий сценарий: онтологическая забывчивость. Самый тонкий сценарий — когда работа в установке разделения готового приводит к забвению пред-формальных оснований, на которых стоит формальная работа. Объекты математики начинают казаться самодостаточными — существующими «сами по себе», без отсылки к структуре акта различения, к законам логики, к Абсолюту как мета-системе. Это — именно та утрата онтологического основания, которую разбирает Том I и которая в Томе II получает противовес через строгую методологию формализуемого первого, разобранную в Главе 1.

Различение и разделение не есть две противоположные методологии, из которых одна правильная, а другая нет. Это — две установки, работающие на разных уровнях глубины. Разделение готового — рабочая установка повседневной формальной деятельности; различение в одном акте — структурная установка, к которой нужно возвращаться всякий раз, когда повседневная работа упирается в основания.

Между уровнями

Полезно сформулировать соотношение двух установок ещё точнее. Это — не выбор между ними, а соотнесение уровней, на которых они работают.

На уровне Elements работает установка разделения готового. Здесь есть конкретные пропозиции, числа, функции, элементы групп, точки пространств. С ними работают операции, к ним применяют теоремы, их подставляют в формулы. Это — рабочая поверхность математики, и на ней установка разделения адекватна.

На уровне Roles и Rules работает установка различения в одном акте. Здесь вопросы не об объектах, а о позициях и о правилах, их связывающих. Здесь существенно, что положительная и отрицательная стороны со-определены; что элементы соответствуют ролям; что правила удерживают структуру. На этом уровне установка разделения готового не работает — потому что объектов в обычном смысле здесь нет; есть устройство, в котором объекты получают свои позиции.

Переход между уровнями происходит, когда работа с объектами сталкивается с вопросом об объектах. Когда математик вычисляет производную, он работает в установке разделения. Когда он спрашивает «а что такое производная?», он переходит на уровень Roles — к вопросу о том, какую роль производная играет в структуре анализа, какие правила её удерживают, какое место она занимает в общем устройстве. Здесь работает установка различения.

Так понятая, пара различение/разделение не противопоставляет два способа делать математику; она различает два уровня, на которых математика работает — и которые в ToS оба сохранены, оба нужны и оба работают.

С этим финальным методологическим наблюдением Глава 5 завершается. В Главе 6 настоящей части обсуждаются технические аксиомы Rocq, на которые опирается работа с Distinction, — классическая аксиома classic и аксиома L4_witness, реализующая механизм передачи статуса через E/R/R вместо Аксиомы Выбора. Тема со-определения, развёрнутая в настоящей главе, будет возвращаться в последующих частях каждый раз, когда речь пойдёт о структурах с парами сторон — от двойственности в категориях (Часть VIII) до обратных элементов в группах (Часть XI).

Часть: Часть I. Перво-различие и законы логики · Том: «Математика»

Понятия: Парадокс · Логика · Формализация

Навигация: ← Глава 4. E/R/R: онтология системы · Глава 6. Аксиоматический минимум и механизм статуса →

В файле LawsFromDistinction.v теорема L2_from_distinction утверждает, что $\neg (‘ p os i t i v e ‘ D \land ‘ n e g a t i v e ‘ D)$ для всякой $D : ‘ D i s t in c t i o n ‘$ , и её доказательство есть прямое применение L2_exclusivity — то есть прямая ссылка на поле exclusive записи. ↩
Аналогично L2: в LawsFromDistinction.v теорема L3_from_distinction утверждает $‘ p os i t i v e ‘ D \lor ‘ n e g a t i v e ‘ D$ для всякой $D$ и доказывается прямым обращением к полю exhaustive. ↩
Лемма расположена в файле Distinction.v в секции, обозначенной как co-constitution. ↩
В текущей версии репозитория эти эквивалентности отдельными именованными леммами не оформлены — их формальное содержание полностью обеспечено полями exclusive и exhaustive, но самостоятельных лемм negative_iff_not_positive и positive_iff_not_negative в файле пока нет. Их добавление сделало бы формальную опору со-определения явной; это — естественное направление уточнения репозитория. ↩
Подробный разбор объединяющей теоремы и формы, в которой в неё входит $L 5$ , — в § 3.7 Главы 3. ↩
Cours de linguistique générale, опубликован в 1916 году по записям лекций 1906–1911 годов учениками Соссюра (Ш. Балли и А. Сеше). Цитируемое положение — из части II, главы IV <<Значимость языкового знака>> (раздел 4). В оригинале: <<dans la langue il n’y a que des différences>>. Русский перевод фразы варьируется по изданиям; ниже приводится её смысловая, а не буквальная передача. ↩
Wissenschaft der Logik, в первой редакции — 1812–1816 годы, во второй — 1832 год. ↩
Книга Перемен, один из старейших памятников китайской мысли; складывалась как корпус с конца II тысячелетия до н. э.; в виде, известном европейской традиции, — с X–III веков до н. э. ↩
Mūlamadhyamakakārikā — основной труд Нагарджуны, центральный текст философской школы мадхьямака. ↩
Парадокс был кратко упомянут в § 4.2.2 Главы 4 в связи с принципом $P 1$ ; полное обсуждение — в § 4.8 Главы 4 после введения мета-системы Абсолюта. ↩

Путь Мудрости

Проводник