Глава 2. Акт различия: запись Distinction

От «есть» к «различено»

Размытость существования до различения

Глава 1 установила первичный факт $A = \exists$ , обнаружила границу его формализации, и указала на акт различения как первое формализуемое. Сейчас, в начале Главы 2, нам предстоит развернуть это указание: рассмотреть акт различения уже не методологически (как точку, в которую переходит настоящая работа после признания границы), а содержательно — что именно в нём происходит, какова его структура, почему он подходит на роль основания математической работы.

Начнём с того, как соотносятся $A = \exists$ и акт различения.

Утверждение $A = \exists$ говорит, что нечто есть, и ничего не говорит больше. Это — максимально содержательное минимальное утверждение: оно фиксирует факт существования и оставляет полностью неопределённым всё остальное. Что именно есть? Сколько его? Каково оно? Какова его внутренняя структура? Все эти вопросы — за пределами $A = \exists$ . Само существующее, как оно дано в $A = \exists$ , размыто: оно есть, но в этом «есть» ещё не выделено ничего определённого.

В терминах метафизики Тома I это онтологическое состояние имеет точное описание. До первого акта различения (того, что Том I называет Светом — акта Логики, различающего спящий статус Источника) есть Логика и Источник как мета-уровневые сущности — первичные факты, устанавливаемые в Томе I, — но нет событий, нет различимых внутренних структур, нет последовательности. Это не «пустота»: Логика и Источник существуют как первичные сущности, — но это ещё не дифференцированное существование. Акт Света, как первое событие различения, актуализирует уже-имеющееся отношение Логики и Источника: Логика различает спящий статус Источника, и это различение становится основанием активации свидетельствующего свойства Источника — Источник переходит из спящего модуса в активный. С этого момента появляется определённость структуры: разделение на актуализированное и неактуализированное, на то, что выделено различением, и то, чем оно не является.

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

Первое определённое утверждение: о границе

Если $A = \exists$ — размытость, то первое определённое утверждение должно быть утверждением о границе: о том, что есть это и не есть то.

Эта формулировка точна. Граница — единственный объект, который вводит определённость, не предполагая её. Объект, свойство, отношение предполагают определённость уже-данного: чтобы говорить об объекте, нужно знать, какого он типа; чтобы говорить о свойстве, нужно иметь его носитель; чтобы говорить об отношении, нужно иметь связываемые им объекты. Эти возможности рассматривались в § 1.4 не как кандидаты на первое формализуемое (там работа шла иначе — через прослеживание условий, делающих $A = \exists$ возможным), но мы можем здесь использовать их как контраст: каждая из них требует чего-то уже-данного, и потому не может быть первым определяющим жестом.

Граница же не требует ничего предшествующего, кроме того, в чём она проводится. Чтобы провести границу, достаточно размытого «есть», уже утверждённого $A = \exists$ , и работы Логики, способной различать. Существующее, в котором проводится граница, уже есть — этого факта не отменяет ни один акт различения. Но стороны как определённые стороны — то, что есть это в опоре на то, что есть не то, — появляются вместе с самим актом. Различение актуализирует структурное отношение, которое до него существовало лишь как возможность, не как определённость.

Это согласуется с тем, как метафизика Тома I описывает первый акт Света. Источник существует и до Света — но в спящем модусе, в котором его свидетельствующее свойство не активировано. Акт Света не создаёт Источник; он актуализирует его свидетельствующее свойство, переводит спящий модус в активный. Так и в производных актах различения: материал, в котором проводится граница, существует и до этого акта — но как определённые стороны разделения, как структурное отношение «это в опоре на не то», он впервые появляется в самом акте. Различение онтологически продуктивно не тем, что создаёт существующее, а тем, что актуализирует определённость в нём.

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

Сходящиеся свидетельства в традиции

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

Спенсер-Браун. В книге Laws of Form (1969)¹ Джордж Спенсер-Браун начинает с одной операции: «Draw a distinction» — проведи различие. Из этого жеста, переданного единственным графическим знаком, он разворачивает всю математическую логику, включая исчисление высказываний и фрагменты арифметики. Для Спенсер-Брауна различение есть предельно простое математическое действие, на котором стоит всё остальное; и не существует ничего структурно более простого, что предшествовало бы ему.

Подход Спенсер-Брауна, при всей оригинальности, имеет общий со ToS структурный остов: различение как первичное действие, из которого выводится дальнейшее. Различия в деталях существенны (Спенсер-Браун работает в графической нотации, его исчисление не охватывает квантификации и более богатых конструкций), но методологический жест — начать с одного акта различения — общий.

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

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

Хайдеггер: онтологическое различие. В Бытии и времени (1927) и в работе Идентичность и различие³ (1957) Мартин Хайдеггер вводит онтологическое различие — различие между бытием (Sein) и сущим (Seiendes). Это — структурно первичное различие, без которого сама постановка вопроса о бытии невозможна.

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

Деррида: différance. Жак Деррида в работе Différance⁴ (1968) вводит неологизм, объединяющий два смысла французского глагола différer: «различать» и «откладывать». Différance — структура, в которой различие производит тождество, а не следует из него.

При всей специфичности подхода Деррида — у него различие онтологически радикально первично, а тождество объектов оказывается их собственным эффектом, — структурный ход в общем направлении совпадает с тем, что работает в акте различения: положительная сторона имеет тождество (закон $L 1$ ) только в опоре на различение от отрицательной. ToS не следует за Деррида в его более радикальных выводах об отсутствии устойчивой онтологии; но фиксирует то же структурное наблюдение: различие актуализирует тождества сторон, не предполагает их заранее данными.

Метафизика Тома I. Наконец — основное для нас свидетельство. В Томе I по метафизике акт различения занимает центральное место: Свет как акт Логики, различающей спящий статус Источника, есть первое событие в онтологии. До этого акта Логика и Источник существуют как мета-уровневые сущности, но без событий — Источник пребывает в спящем модусе, его свидетельствующее свойство не активировано. Акт Света не создаёт Источник; он актуализирует его свидетельствующее свойство, переводя спящий модус в активный. И именно через это первое событие становится возможным само время как структура последовательности актов. ToS опирается на этот результат: акт различения — не один из многих возможных стартов, а структурно первичная точка, в которой возможность определённости впервые переходит в актуальность.

Соответственно, математика как язык описания начинает работать с этого первого акта: математика записывает структуру актов различения, обнаруживаемую в реальности, не создаёт отдельный мир «математических сущностей». Положение, зафиксированное в Методологическом введении — математика есть язык описания логической структуры реальности, — получает в работе Тома I и в анализе акта различения своё первое математическое приложение: Distinction как формальная запись на языке Rocq есть запись логической структуры реальных актов различения, а не самостоятельная математическая сущность.

Эта сходимость — от Спенсер-Брауна, работающего в математической логике, через структурную лингвистику Соссюра и онтологию Хайдеггера, к постструктурализму Деррида и метафизике Тома I — не есть доказательство позиции ToS. Доказательство и обоснование принадлежат собственной линии настоящего тома: деривации законов и принципов из $A = \exists$ . Но эта сходимость показывает, что идея первичности различения не есть произвольное авторское изобретение: она многократно возникает в разных традициях — математической, лингвистической, философской — как устойчивая мыслительная структура, к которой независимо приходят с разных сторон. Это — свидетельство уместности исходной идеи, а не замена её обоснования.

Установив, что акт различения есть тот объект, через который настоящая работа переходит от пред-формального $A = \exists$ к формализуемой математической работе, мы можем теперь рассмотреть его структуру содержательно — что именно в нём происходит, какие четыре момента в нём совмещены и как они связаны между собой. Этому посвящён следующий раздел.

Структура акта различения

Четыре момента одного акта

Когда совершается акт различения, в нём одновременно проявляются четыре момента:

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

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

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

В этом смысле акт различения есть синхронное единство четырёх моментов. Они различимы для анализа — мы можем говорить о каждом отдельно, как делаем сейчас, — но онтологически они одновременны и взаимно требуют друг друга. Запись Record Distinction, которую мы введём в «Формализация в : запись Record Distinction», отразит это единство как одну структуру с четырьмя полями, не как набор независимых утверждений.

Рассмотрим теперь каждый из четырёх моментов содержательно.

Положительная сторона: что значит «есть» в различении

Положительная сторона — то, что есть в смысле совершаемого разделения. Это формулировка требует уточнения, поскольку слово «есть» здесь работает не в том же смысле, как в $A = \exists$ .

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

В терминах метафизики Тома I: положительная сторона — это актуализированный полюс различения. Различение, как мы видели в «От «есть» к «различено»», актуализирует структурное отношение, существовавшее как возможность. Положительная сторона — один из двух полюсов этого актуализированного отношения, тот, к которому относится сам акт выделения.

Закон Тождества $L 1$ применяется к положительной стороне: она тождественна самой себе на протяжении всей теории. Это онтологическое применение Закона Тождества, не формальное правило: положительная сторона есть определённая сторона, и в качестве таковой она устойчиво тождественна себе во всех контекстах, где это различение действует. Без этой тождественности положительная сторона не могла бы участвовать в дальнейших структурах — утверждения о ней не были бы устойчивы, отсылки к ней теряли бы определённость.

Иллюстративный пример. Когда математик утверждает: «число $n$ является чётным», он совершает акт различения, в котором положительная сторона — утверждение « $n$ чётно». Эта положительная сторона тождественна себе: в любом месте дальнейшего рассуждения, обращаясь к утверждению « $n$ чётно», математик имеет в виду одно и то же. Если бы положительная сторона не была тождественна себе, само утверждение становилось бы неопределённым.

Отрицательная сторона: «не это» как полноценный участник

Отрицательная сторона — то, чем положительное не является. И здесь требуется важное уточнение, поскольку обыденное понимание отрицания может ввести в заблуждение.

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

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

Это положение существенно. В стандартной математической работе отрицание иногда понимается как дополнение до универсума: «не $P$ » означает «всё, что есть в универсуме, кроме $P$ ». Это множественное понимание отрицания, в котором отрицательное определено через положительное и универсум. Акт различения работает до этого понимания: в нём отрицательная сторона определена не как дополнение к чему-то более раннему, а со-возникает с положительной в одном акте.

Возьмём прежний пример. Утверждение «число $n$ является чётным» — положительная сторона. Отрицательная сторона — «число $n$ не является чётным» — столь же определена и содержательна. Это не «всё прочее»; это конкретное утверждение, имеющее свою структуру и свой смысл. Без этой определённости акт различения был бы неполон.

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

Взаимное исключение: что невозможно в одном отношении

Третий момент акта различения — утверждение невозможности: положительная и отрицательная стороны не могут одновременно иметь место в одном отношении.

Это — работа Закона Непротиворечия $L 2$ внутри самого акта. Без взаимного исключения само разделение распалось бы: если бы положительное могло быть одновременно отрицательным, граница между ними была бы фиктивной, и весь акт сводился бы к утверждению, что нечто есть (без всякого определённого что).

Формально взаимное исключение записывается так:

\neg (положительное \land отрицательное) .

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

Тонкость: «в одном отношении». Закон Непротиворечия и соответствующее ему взаимное исключение работают относительно конкретного акта различения, не вообще. Это важное уточнение, поскольку без него можно прийти к ошибочному выводу, что одна и та же сущность не может быть положительной стороной в одном различении и отрицательной — в другом.

Между тем это совершенно обычная ситуация. Возьмём число $4$ . В различении «чётное / нечётное» оно стоит на положительной стороне (чётное). В различении «меньше 10 / не меньше 10» оно снова на положительной стороне. В различении «равно 5 / не равно 5» оно на отрицательной стороне. В одном отношении оно занимает определённое место; в разных отношениях — может занимать разные. Противоречия здесь нет, поскольку речь о разных актах различения, и взаимное исключение работает внутри каждого из них.

Аристотель в Метафизике IV.3 формулирует Закон Непротиворечия именно с этой оговоркой: «невозможно, чтобы одно и то же одновременно было и не было присуще одному и тому же в одном и том же отношении»⁵. Слова «в одном и том же отношении» — ключевые. Они показывают, что Закон Непротиворечия не запрещает разные различения одного объекта в разных контекстах; запрещается лишь одновременная принадлежность к обеим сторонам одного различения.

Совместная исчерпанность: что между сторонами нет третьего

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

Это — работа Закона Исключённого Третьего внутри самого акта. Формально:

положительное \lor отрицательное .

«Имеет место либо положительное, либо отрицательное; третьего нет».

Здесь требуется аккуратность в формулировке. В метафизике Тома I, как было указано в Методологическом введении, Закон Исключённого Третьего производен от Тождества и Непротиворечия. Если нечто есть (Тождество) и не может одновременно быть и не быть (Непротиворечие), то между «есть» и «не есть» нет третьего — ничего, что было бы ни одним, ни другим. Это следствие совместной работы первых двух законов, не самостоятельный третий закон.

Однако в формальной системе Rocq, в которой ведётся настоящая работа, Закон Исключённого Третьего не выводим как теорема: для произвольной пропозиции $P$ конструктивного доказательства $P \lor \neg P$ нет. По этой причине в формализации он получает статус самостоятельного $L 3$ — технически отдельное поле записи Distinction и отдельная аксиома classic, на которую опирается конструкция distinction_of («Конструкция distinction_of: построение различия из пропозиции»).

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

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

Над всем — работа ЗДО

Четыре момента — положительная сторона, отрицательная сторона, взаимное исключение, совместная исчерпанность — образуют структуру акта различения. Но они не работают сами по себе. Над всем актом работает Закон Достаточного Основания — мета-структура, в которой четыре момента обоснованы как момент совершаемого акта.

Развернём это положение. ЗДО, как было установлено в Методологическом введении и в (см. соответствующую главу) Главы 1, не есть один из законов наряду с другими. ЗДО есть само действие Логики, в котором обоснование как структура существует. Применительно к акту различения это означает: каждый из четырёх моментов имеет основание, и сам акт как целое имеет основание совершаться так, как он совершается, не иначе.

Конкретно:

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

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

В формальной системе Rocq это положение проявляется специфическим образом. ЗДО не записывается как отдельное поле или аксиома — его работа проявляется в том, что построение конкретного экземпляра Distinction требует предъявления обоснований для всех четырёх полей. Нельзя написать Distinction с произвольными значениями полей, не предъявив их совместной согласованности; компилятор отвергнет такую запись. В этом смысле Rocq как формальная система встраивает работу ЗДО в свою основу: любое определение должно быть обосновано (это типы), любая теорема должна быть доказана (это термы доказательств), любая конструкция должна быть проверяемой (это ядро системы). ЗДО работает как организационный принцип формальной системы, а не как одно из её утверждений.

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

Здесь, однако, нужно сразу провести различение, без которого дальнейшие отсылки к ЗДО и к закону $L 4$ могут смешаться. В настоящем томе мы будем различать три уровня, на которых выступает один и тот же онтологический принцип достаточного основания.

Первый — онтологический ЗДО. Это — само действие Логики, требующее основания, мета-структура, описанная выше. Она не есть поле записи Distinction и не есть теорема Rocq; она есть то, через что запись и теоремы имеют силу.

Второй — закон $L 4$ в слое Distinction. Это — самозаземление различения, формально выразимое в Rocq как утверждение positive D -> ~ negative D: при наличии положительной стороны отрицательная сторона отрицается. Основание этого отрицания даётся самим фактом положительной стороны вместе с исключительностью — полем exclusive. Глава 3 выведет $L 4$ именно в этом виде, как теорему о записи.

Третий — свидетельствование в аксиоматическом слое. Это — отдельный технический след того же принципа: требование, что индивидуальное существование имеет определённого свидетеля. Этот уровень — предмет более поздней главы; здесь мы лишь отмечаем, что он отличен и от онтологического ЗДО, и от закона $L 4$ в слое Distinction.

Смешивать эти три уровня не следует: онтологический ЗДО — принцип, $L 4$ — теорема о записи, свидетельствование — технический приём аксиоматического слоя. Все три суть проявления одного принципа достаточного основания, но работают на разных уровнях формализации.

Четыре момента и пять законов

Подведём промежуточный итог структуры акта различения с точки зрения законов Логики.

Момент акта	Соответствующий закон	Формализация
Положительная сторона	$L 1$ (Тождество)	`positive : Prop`
Отрицательная сторона	$L 1$ (Тождество)	`negative : Prop`
Взаимное исключение	$L 2$ (Непротиворечие)	`exclusive`
Совместная исчерпанность	$L 3$ (Исключённое Третье)	`exhaustive`
Обоснование акта	ЗДО (мета-закон)	встроено в Rocq

Закон Тождества $L 1$ работает дважды — применительно к каждой из двух сторон. Закон Непротиворечия $L 2$ работает один раз — обеспечивая взаимное исключение. Закон Исключённого Третьего $L 3$ работает один раз — обеспечивая совместную исчерпанность. ЗДО работает как мета-структура, проявляющаяся в самой возможности обоснованного построения акта.

Закон Порядка $L 5$ в этой структуре не проявляется явно; его работа относится к иерархии актов различения, не к структуре одного акта. Он будет введён в последующей главе о структуре уровней — как самостоятельная структура Level, формализующая порядок уровней.

Так в акте различения проявляются все законы Логики — одни как содержательные требования к структуре одного акта, другие как организационные принципы работы с актами в целом. Это согласуется с тем, что было обнаружено в § 1.4 Главы 1: акт различения есть простейшее проявление работы законов Логики, доступное для формальной записи.

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

Формализация в Rocq: запись `Record Distinction`

Запись

Установив содержательную структуру акта различения — четыре момента, работающие как аспекты одного акта под мета-структурой ЗДО, — мы переходим к его формальной записи в системе Rocq. Это первый формальный объект настоящего тома, с которым непосредственно работает машинная проверка.

Запись имеет следующий вид:

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

Каждое из четырёх полей формализует один из четырёх моментов акта, разобранных в «Структура акта различения»:

positive : Prop — положительная сторона различения. Утверждение, обозначающее то, что есть в смысле совершаемого разделения.
negative : Prop — отрицательная сторона различения. Утверждение, обозначающее то, чем положительное не является.
exclusive : ~(positive /\ negative) — взаимное исключение. Доказательство того, что положительное и отрицательное не могут одновременно иметь место.
exhaustive : positive \/ negative — совместная исчерпанность. Доказательство того, что одно из двух обязательно имеет место.

Имя конструктора — mkDistinction — следует обычному соглашению Rocq для конструкторов записей: префикс mk означает «построить» (make). Имея четыре поля с правильными типами, можно построить экземпляр записи через вызов mkDistinction p n e h, где p, n, e, h — значения соответствующих полей.

Что есть `Record` в Rocq

Для читателя, знакомого со стандартной математикой, но не работавшего прежде с Rocq, поясним конструкцию Record.

Record — синтаксическая конструкция Rocq, эквивалентная индуктивному типу с единственным конструктором. То есть запись

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

формально эквивалентна определению

Inductive Distinction : Type :=
  | mkDistinction :
      forall (positive negative : Prop),
        ~(positive /\ negative) ->
        positive \/ negative ->
        Distinction.

вместе с автоматически сгенерированными проекциями (функциями positive, negative, exclusive, exhaustive, извлекающими соответствующие поля из экземпляра). Форма Record компактнее и удобнее для работы; содержательно она не отличается от индуктивного определения.

Что значит «определить тип Distinction»? В систему типов Rocq вводится новый тип, экземпляры которого — кортежи из четырёх согласованных значений. Что значит «иметь экземпляр Distinction»? Иметь конкретные значения для всех четырёх полей, причём третье и четвёртое поля — доказательства соответствующих утверждений в терминах первых двух. Без этих доказательств экземпляр построить невозможно: компилятор Rocq отвергнет запись, в которой 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 ‘$ .

Это — одно из проявлений того, что мы обсуждали в «Над всем — работа ЗДО»: ЗДО встроен в саму работу Rocq. Невозможно построить акт различения без явного предъявления оснований для всех его четырёх моментов. Формальная система требует обоснований; требование оснований — работа ЗДО.

Здесь важно сразу различить два случая — общую запись и каноническую конструкцию, — ибо в дальнейшем тексте мы пользуемся обоими, и их смешение ведёт к неточности. В общей записи Distinction поле negative есть самостоятельная пропозиция типа Prop. Оно не определено синтаксически как отрицание поля positive: связь между положительной и отрицательной сторонами задаётся не равенством, а полями exclusive и exhaustive — исключительностью и исчерпанностью. Канонический же случай — конструкция distinction_of, к которой глава перейдёт в «Конструкция distinction_of: построение различия из пропозиции», — выбирает отрицательную сторону равной $\neg P$ : для произвольной пропозиции $P$ он строит каноническое различение $P$ и $\neg P$ . Общая запись, стало быть, шире канонической конструкции: она оставляет отрицательную сторону явной частью акта, не сводя её заранее к отрицанию положительной. Когда ниже мы говорим об отрицательной стороне как о <<том, чем положительное не является>>, речь идёт о каноническом случае; общая запись этого не требует.

Эквивалентная математическая нотация

Для удобства отсылок в основном тексте, помимо Rocq-нотации, мы будем использовать стандартную математическую запись. Акт различения как кортеж записывается так:

D = (P, N, ε, η),

где

$P : Prop$ — положительная сторона;
$N : Prop$ — отрицательная сторона;
$ε$ — доказательство $\neg (P \land N)$ ;
$η$ — доказательство $P \lor N$ .

Тип всех актов различения мы будем обозначать через $Distinction$ — это математическая нотация, под которой подразумевается тип объектов, рассматриваемых в общем тексте тома. В Rocq-листингах и в ссылках на формальный код мы будем использовать моноширинное Distinction — имя, под которым этот же тип фигурирует в репозитории. Это одно и то же содержание в двух нотациях: $Distinction$ — для математической работы в основном тексте, Distinction — для формальной работы в кодовых блоках. Для конкретного экземпляра $D \in Distinction$ его поля доступны через стандартные проекции:

positive (D) = P, negative (D) = N, exclusive (D) = ε, exhaustive (D) = η .

Заметим, что $ε$ и $η$ суть доказательства, не истинностные значения. Это — следствие типизации в Prop, к подробному обсуждению которой мы перейдём в «Почему Prop, а не bool: позиция логического реализма». Здесь зафиксируем лишь: $ε$ и $η$ несут структурную информацию — они показывают, как исключительность и исчерпанность установлены в данном различении, — не сводятся к булевским значениям «true/false».

Универсум `Prop`

Несколько слов об универсуме Prop, в котором живут поля positive и negative. Полное обсуждение выбора Prop (в противопоставлении bool) и связанной с ним позиции логического реализма — предмет следующего раздела, «Почему Prop, а не bool: позиция логического реализма». Здесь укажем технически.

В CIC — исчислении индуктивных конструкций, на котором построен Rocq, — существует иерархия универсумов:

Prop — универсум пропозиций, то есть утверждений. Элементы Prop — это утверждения, которые могут быть доказаны или опровергнуты.
Set — универсум вычислимых данных. Элементы Set — типы конкретных значений: nat (натуральные числа), bool (булевские значения), list (списки) и так далее.
Type — более общий универсум, охватывающий Prop и Set и допускающий определения типов более высокого порядка.

Когда мы пишем positive : Prop, мы фиксируем: положительная сторона есть утверждение (нечто, что может быть истинным или ложным), а не вычислимое значение и не тип данных. То же относится к negative. Поля exclusive и exhaustive не имеют собственного объявления типа в виде Prop; они объявляются по конкретному типу, который зависит от значений positive и negative — именно $\neg (‘ p os i t i v e ‘ \land ‘ n e g a t i v e ‘)$ и $‘ p os i t i v e ‘ \lor ‘ n e g a t i v e ‘$ .

Это — характерная особенность зависимых типов в CIC: тип поля может зависеть от значений других полей. Запись Distinction использует эту возможность: типы третьего и четвёртого полей конструируются из первых двух. Если бы мы попытались определить Distinction в системе без зависимых типов (например, в обычной типизированной теории), это потребовало бы обходных путей.

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

Подведём итог того, что мы получили вместе с записью Record Distinction.

Первый формальный объект настоящего тома. До этого момента изложение работало на содержательном уровне: формулировки, обсуждения, ссылки на Том I по метафизике. С введением Distinction появляется первый объект, который компилятор Rocq принимает в свой язык, который можно записать в файле, проверить машинно, использовать в дальнейших определениях. Этот переход — центральный для всей последующей работы: с него начинается собственно математическая работа.

Универсальный шаблон для последующих структур. Запись Distinction устанавливает образец, по которому будут строиться последующие структуры тома. Идея «зафиксировать тип, указать его поля, требовать обоснований» работает во всех частях:

В Части IV — запись CauchyProcess как процесс с полем сходимости.
В Части XI — запись Group как структура с операцией, нейтральным элементом, обратными элементами и полями ассоциативности.
В Части XII — запись Category как структура с объектами, морфизмами, композицией и полями ассоциативности и тождества.

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

Готовность к выводу законов. С записью Distinction в руках — основание для дальнейших шагов. В Главе 3 будут выведены законы логики $L 1, L 2, L 3, L 4$ как теоремы о свойствах этой записи. Каждое из четырёх полей породит соответствующее утверждение, и доказательство этого утверждения будет тривиальным — оно сведётся к проекции на соответствующее поле или к простому преобразованию. Глава 3 покажет это в деталях.

Установив запись Distinction, мы должны теперь объяснить существенный технический и философский выбор, лежащий в её основе: почему поля positive и negative типизированы в Prop, а не в bool. Этот вопрос имеет не только формальный, но и центральный онтологический смысл, к которому мы переходим в следующем разделе.

Почему `Prop`, а не `bool`: позиция логического реализма

Естественный вопрос

Математический читатель, видя positive : Prop и negative : Prop в записи Distinction, может задать естественный вопрос. Различение есть разделение на «да» и «нет»; почему бы не использовать bool — стандартный тип булевых значений, прямо предназначенный для двоичных альтернатив? Запись выглядела бы так:

Record Distinction_bool := mkDistinction_bool {
  positive_b : bool;
  negative_b : bool;
  ...
}.

Этот вопрос — не технический. Ответ требует ясности относительно того, что есть различение, и относительно того, какую онтологию формальной системы ToS принимает. Настоящий раздел — центральный философский раздел Главы 2 — посвящён этому ответу. Он развёртывается в несколько шагов: техническое различие Prop и bool в CIC; философское различие proof-irrelevance и proof-relevance; позиция логического реализма; соотношение с конструктивизмом, платонизмом и формализмом; следствия для всего настоящего тома.

Различие `Prop` и `bool` в CIC

Начнём с технической стороны.

bool — тип значений. bool в Rocq есть индуктивный тип с двумя конструкторами:

Inductive bool : Set :=
  | true  : bool
  | false : bool.

Утверждение о булевской переменной $b : ‘ b oo l ‘$ решается вычислением. Если у нас есть выражение, возвращающее bool, мы можем его вычислить и получить за конечное число шагов либо true, либо false. Например, выражение Nat.eqb 2 2 (булевское равенство натуральных чисел) вычислится в true; Nat.eqb 2 3 — в false. В обоих случаях алгоритм проверки доступен и завершается.

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

Prop — тип утверждений. Prop есть универсум пропозиций — утверждений, которые могут быть истинны или ложны, но которые не обязательно разрешаются вычислением. Утверждение $P : ‘ P r o p ‘$ доказывается построением терма (объекта в типовой теории), имеющего тип $P$ . Существование такого терма гарантирует истинность $P$ .

Ключевая разница: Prop не предполагает алгоритма проверки. Утверждение $P : ‘ P r o p ‘$ может быть:

доказано — если построен соответствующий терм;
опровергнуто — если доказано $\neg P$ (то есть построен терм типа $P \to False$ );
неразрешимо внутри текущей системы — если ни $P$ , ни $\neg P$ не доказуемо без введения дополнительных аксиом.

Но смысл утверждения $P$ от наличия или отсутствия алгоритма проверки не зависит. $P$ имеет смысл и структуру независимо от того, можем ли мы его проверить вычислением.

Простой пример различия. Булевский предикат хорош там, где мы заранее располагаем процедурой решения: например, Nat.eqb n m — проверка равенства двух натуральных чисел — за конечное число шагов возвращает true или false. Но утверждения с кванторной структурой — вида forall n, exists p,\ … — естественно живут в Prop: они имеют внутреннее логическое строение (кванторы, связки) и требуют доказательства, а не одного вычисленного значения true. Для иных таких утверждений можно построить связанный булевский тест и доказать лемму, связывающую тест с утверждением (так называемую reflection-лемму); но сам по себе bool не заменяет пропозициональную структуру — он хранит результат вычисления, а не само утверждение с его кванторами и доказательством.

Это — характерный пример того, что Prop шире bool. Всё, что разрешимо вычислением, выразимо в bool (и в Prop тоже, через соответствие); но утверждения с кванторной структурой, не сводимые к одному вычислимому тесту, — живут в Prop.

Proof-irrelevance и proof-relevance

Помимо технического различия в способе верификации, между Prop и bool есть и более тонкое различие, связанное со статусом доказательств (или, в случае bool, значений).

Proof-irrelevance. Если у утверждения $P : ‘ P r o p ‘$ есть два разных доказательства $p_{1} : P$ и $p_{2} : P$ , считаются ли они разными? В стандартной математической практике — нет. Доказательство ценно тем, что устанавливает истину; разные пути к одной истине считаются эквивалентными как доказательства. Эта позиция называется proof-irrelevance — доказательственная неразличимость.

В bool proof-irrelevance тривиальна: у каждого булевского значения ровно один способ быть собой. true есть true, false есть false; никаких «разных способов быть true» нет.

Proof-relevance. В более тонкой версии теории типов доказательства имеют структуру, и разные доказательства одной теоремы могут нести разную информацию. Эта позиция называется proof-relevance — доказательственная различимость. Она характерна для интенсиональной теории типов Мартин-Лёфа и для гомотопической теории типов (HoTT), где доказательства идентичности интерпретируются как пути в топологическом пространстве, и разные пути могут быть гомотопически неэквивалентны.

Позиция ToS. В настоящем томе используется стандартная CIC, где Prop по умолчанию не обладает строгой proof-irrelevance, но в большинстве конкретных рассуждений мы можем её принимать (для наших целей структурного анализа разные доказательства одной леммы эквивалентны).

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

В этом смысле выбор Prop вместо bool сохраняет структурную информацию там, где bool её бы потерял. Если бы мы записали positive : bool, мы бы свели положительную сторону к одному из двух значений (true или false); вся структура утверждения, его содержание, его связь с другими утверждениями — всё это исчезло бы. Выбор Prop сохраняет это содержание как часть формального объекта.

Подчеркнём, что для выбора Prop существенно не различие между proof-irrelevance и proof-relevance как таковое — этот вопрос для наших целей второстепенен, — а различие между пропозицией и вычисленным результатом. Prop сохраняет само утверждение: его кванторы, связки, зависимости, его место в доказательстве. bool сохраняет лишь результат вычислимого теста — один бит. Для записи Distinction, в которой положительная и отрицательная стороны суть утверждения с внутренней логической структурой, существенно именно первое. Вопрос о статусе доказательств — relevance они или irrelevance — здесь важен лишь постольку, поскольку он оттеняет это главное различие.

Логический реализм: основная позиция

Перейдём от технического анализа к лежащей в его основе позиции. Эта позиция была установлена в Методологическом введении и работает через весь настоящий том; здесь она получает своё конкретное приложение к выбору Prop.

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

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

Это согласуется с пониманием математики как языка описания логической структуры реальности, зафиксированным в Методологическом введении: положительная сторона различения записывает аспект реальной структуры; она имеет смысл, потому что описываемое есть.

Из реализма — выбор Prop. Это и есть причина, по которой ToS типизирует положительную и отрицательную стороны акта различения в Prop, не в bool.

Записывая positive : Prop, мы утверждаем: положительная сторона различения есть утверждение — нечто, что может быть верно или неверно, нечто, имеющее структуру, не сводимую к вычислимому значению. Утверждение существует как структурный объект; его истинность устанавливается доказательством, не алгоритмом проверки.

Если бы мы выбрали bool, мы бы фактически сказали: положительная сторона различения есть вычислимый результат — один из двух заранее данных исходов. Это сводит акт различения к алгоритму; алгоритм, в свою очередь, есть техническая реализация, не онтологическая структура. Выбор bool тем самым сводил бы Логику к вычислимости — что противоречит онтологической первичности Логики, установленной в Томе I.

Логика первична; вычислимость — частный случай. Это центральное методологическое положение всей работы ToS. Вычислимость есть частный случай работы Логики — случай, в котором структура утверждения такова, что допускает алгоритмическое решение. Но не всякая работа Логики вычислима, и не всякое истинное утверждение имеет алгоритм проверки. Гёдель показал это формально для арифметики (существуют истинные арифметические утверждения, недоказуемые в данной формальной системе); метафизика Тома I показывает это онтологически (Логика как структура бытия не сводится к технике вычисления).

Выбор Prop — последовательное проведение этой позиции на самом базовом уровне. С него настоящий том начинает; от него ветвится дальнейшее.

Конструктивизм и Теория Систем

Распространённое возражение со стороны конструктивно настроенного читателя может звучать так: «Если ToS подчёркивает явные построения, конечные процедуры и проверяемость, почему первый формальный объект типизирован через Prop — а не через вычислимый bool? Не ближе ли вычислимый тип к духу конструктивизма?»

Ответ важен и потому требует аккуратности — в том числе и в самой постановке вопроса. Конструктивная математика и теория типов работают не преимущественно с булевыми значениями: они активно работают с типами, пропозициями, зависимыми типами, свидетельствами и доказательствами. bool — важный инструмент для разрешимых предикатов, но не синоним конструктивизма. Поэтому возражение нельзя понимать как «конструктивизм $=$ bool»; вопрос тоньше, и ответ на него — ниже.

ToS не отвергает конструктивность. Как было показано в Методологическом введении и в анонсе Главы 5, ToS использует механизм $E / R / R$ с явной передачей статуса, без Аксиомы Выбора. Это типично конструктивный подход — даже более строго конструктивный, чем стандартная классическая математика. Принцип $P 4$ (бесконечность как свойство процессов, Часть IV) есть прямое конструктивное положение: работа с бесконечным идёт через явные процессы, не через обращение к «завершённым» бесконечным объектам.

ToS работает конструктивно там, где это возможно, и демонстрирует, что многие классические результаты остаются доказуемыми без обращения к не-конструктивным аксиомам (Choice, Infinity как завершённый объект).

Что отвергается — это сведение Логики к вычислимости. Различие тонкое, но существенное. ToS не утверждает, что Логика есть вычисление — что всякое истинное утверждение имеет алгоритм проверки, или что вне алгоритмически проверяемого ничего не существует.

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

В терминах позиций: ToS — умеренный реализм, использующий конструктивные методы. Логика существует как структура бытия (реализм); работа с математическими описаниями идёт через конструктивные построения (методологический конструктивизм). Эти две позиции согласованы и взаимно дополняют друг друга.

Конкретно для выбора Prop. Запись positive : Prop согласуется и с реалистическим прочтением (есть структурный факт о реальном, не зависящий от наличия алгоритма проверки), и с конструктивным прочтением. Но конструктивное прочтение здесь нужно понять точно. Оно состоит не в том, что для построения Distinction нужно доказать positive: этого не требуется. Положительная сторона positive есть утверждение, а не доказанное утверждение; чтобы построить экземпляр Distinction, нужно предъявить две пропозиции positive и negative и — вот здесь конструктивность — доказательства заявленных связей между ними: exclusive (исключительность) и exhaustive (исчерпанность). Конструктивный аспект состоит в том, что эти связи должны быть предъявлены как термы доказательств, а не постулированы. Доказательство же самой positive понадобится лишь тогда, когда мы захотим установить, что положительная сторона действительно имеет место, — но это отдельный шаг, не нужный для построения записи. Оба прочтения — реалистическое и конструктивное — не противоречат друг другу; они охватывают разные аспекты одной позиции.

Соотношение с платонизмом и формализмом

Чтобы полностью прояснить позицию ToS, поместим её в более широкий ландшафт философий математики.

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

С точки зрения ToS в платонизме есть глубокая правда — идея, что математические объекты реальны, не зависят от индивидуального субъекта, имеют объективную структуру. Эта часть платонизма согласуется с операциональным реализмом ToS, формулированным в Методологическом введении.

Что ToS не разделяет — это сильную онтологическую тезу о месте математических объектов (отдельное идеальное царство). ToS работает с математическими описаниями как со структурными актуализациями, разворачивающимися через акты различения. Они объективны и реальны, но их способ существования — не «отдельное царство», а актуализированная структура в действии Логики на $A = \exists$ .

Формализм. Гильберт в программе оснований: математика есть игра символов по формальным правилам. «Существование» в математике сводится к согласованности символьных манипуляций; вопрос о том, «что эти символы значат» содержательно, выводится за скобки.

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

Что ToS не разделяет — это редукцию математики целиком к символьной игре. ToS работает в формальной системе, но не из формальной системы: формальная система есть техническая реализация работы Логики, не её основание. Содержание математических утверждений дано онтологически (через работу Логики на $A = \exists$ ), формализация — последующий шаг записи.

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

	Платонизм	Формализм	Операциональный реализм ToS
Природа «математических объектов»	Идеальные сущности в отдельном царстве	Символы в формальной игре	Формальные записи логических структур реального
Способ доступа	Усмотрение идеального	Манипуляция символами по правилам	Обнаружение структуры в реальности; формализация в Rocq
Статус истины	Соответствие идеальному	Согласованность вывода	Адекватность описываемому реальному; формальная проверяемость в Rocq
«Чистая математика» (без приложений)	Подлинна (исследует идеальное)	Подлинна (любые согласованные правила)	Подлинна, только если описывает реальную логическую структуру

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

Импликации для последующих частей

Выбор Prop в записи Distinction не есть локальное решение, относящееся только к «Формализация в : запись Record Distinction». С этого момента вся дальнейшая работа будет вестись в Prop-стиле. Каждое утверждение о математических объектах — пропозиция, не булевское значение. Это позволит работать с объектами, чья истинность нетривиальна (требует доказательства), но структура при этом ясна.

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

Часть IV: RealProcess и анализ. Реально существуют процессы приближения — геометрические аппроксимации длины окружности, измерения физических величин с возрастающей точностью, итерационные вычисления. У этих процессов есть общая логическая структура: последовательность приближений со сходимостью. Тип RealProcess := nat -> Q есть формальная запись этой структуры на языке Rocq. Сам процесс $r : ‘ na t ‘ \to ‘ Q ‘$ — вычислимая функция, живущая в Set. Но утверждения о процессе — что он сходящийся, что он представляет конкретное геометрическое или физическое значение, что он мажорирует другой процесс, — пропозиции в Prop. В последующих частях это будет использовано как рабочий подход к формализации классического анализа: данные и сами процессы живут в вычислимых типах, а утверждения об их сходимости и о представляемых ими значениях формулируются в Prop (см. обсуждение принципа $P 4$ и гипотезы континуума в Методологическом введении).

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

Часть XII: категорная теория. Реально существуют семейства однотипных структур с систематическими переносами между ними — физические системы и их преобразования, типы данных в программировании и функции между ними, алгебраические структуры и гомоморфизмы. У этих семейств есть общая логическая структура: композиция переносов, тождественные переносы, согласованность областей. Категорный аппарат есть формальная запись этой логики на языке Rocq. Равенство морфизмов, коммутативность диаграмм, существование универсальных конструкций — пропозиции о реальной структуре связей в семействах. Попытка свести их к bool разрушила бы саму возможность работы с этими реальными структурами.

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

Во всех четырёх случаях работает одна и та же связь: реально существуют процессы и структуры; математика записывает их логическую структуру формально; в Rocq эти записи живут как пропозиции, не как вычислимые значения, потому что описываемые реальные структуры в общем случае не разрешимы алгоритмом проверки. Выбор Prop вместо bool есть систематическое проведение этого положения через всю последующую работу.

Таким образом, выбор Prop в записи Distinction — не локальная техническая деталь, а принципиальное решение, формирующее облик настоящего тома. Это конкретное проявление позиции логического реализма на самом начальном уровне формальной работы. С него начинается, через него проходит вся последующая математическая работа, и в нём согласуются онтологическая позиция метафизики Тома I и техническая практика работы в Rocq.

Установив запись Distinction и обосновав её типизацию в Prop, мы можем теперь перейти к универсальной конструкции, строящей различение из любой пропозиции. Эта конструкция, обозначаемая distinction_of, есть мост между общими утверждениями Rocq и конкретными актами различения. Ей посвящён следующий раздел.

Конструкция `distinction_of`: построение различия из пропозиции

Постановка задачи

Установив запись Distinction и обосновав её типизацию в Prop, мы сталкиваемся с естественным вопросом. У нас есть форма акта различения — четыре поля с определёнными типами. Но у нас пока нет ни одного конкретного экземпляра. Можно ли показать, что эта форма не пуста?

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

Естественный кандидат: для пропозиции $P$ взять

положительная сторона $:= P$ ,
отрицательная сторона $:= \neg P$ .

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

В этом разделе мы реализуем distinction_of формально, разберём, от каких аксиом Rocq она зависит, и обсудим её содержательный смысл.

Что описывается в реальности

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

В реальности distinction_of $(P)$ описывает следующее явление: всякое содержательное утверждение о реальном автоматически порождает структуру различения между состоянием, в котором это утверждение имеет место, и состоянием, в котором оно не имеет места.

Иными словами: если в реальности можно сказать « $P$ » — скажем, «число $n$ чётно», «функция $f$ непрерывна в точке $x_{0}$ », «эта молекула имеет ось симметрии $C_{3}$ », — то одновременно с этим утверждением возникает структурное различение между ситуацией, где $P$ выполнено, и ситуацией, где $P$ не выполнено. Это различение не отдельное явление, а неотъемлемый аспект самого утверждения — утверждать $P$ значит одновременно различать случай $P$ и случай $\neg P$ .

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

Это согласуется с тем, что было установлено в Главе 1: акт различения есть простейшее проявление работы законов Логики, и эта работа уже совершается всегда, когда есть содержательное утверждение. distinction_of делает это совершение явным в формальной записи.

Определение в Rocq

Формальное определение distinction_of в Rocq:

Definition distinction_of (P : Prop) : Distinction :=
  mkDistinction P (~ P) _ _.

Здесь подчёркивания _ стоят на месте обязательств доказательства — они должны быть заменены конкретными доказательствами полей exclusive и exhaustive. Эти обязательства таковы:

exclusive: $\neg (P \land \neg P)$ — закон непротиворечия для пропозиции $P$ .
exhaustive: $P \lor \neg P$ — закон исключённого третьего для пропозиции $P$ .

Перейдём к разбору каждого.

Доказательство exclusive. Утверждение $\neg (P \land \neg P)$ доказуемо в Rocq без всяких аксиом, конструктивно. Доказательство простое: предположим $P \land \neg P$ , то есть имеем одновременно $p : P$ и $n p : \neg P$ . По определению $\neg P$ есть функция $P \to False$ . Применив $n p$ к $p$ , получаем элемент типа False, что и есть искомое противоречие.

В Rocq это записывается:

Lemma no_contradiction_P : forall P : Prop, ~(P /\ ~ P).
Proof.
  intros P [p np]. exact (np p).
Qed.

Тактика intros P [p np] вводит $P$ как параметр и разбивает гипотезу $P \land \neg P$ на две: $p : P$ и $n p : \neg P$ . Команда exact (np p) применяет $n p$ (имеющий тип $P \to False$ ) к $p$ (имеющий тип $P$ ), получая элемент типа False, что завершает доказательство.

Это — проявление Закона Непротиворечия $L 2$ на конкретной пропозиции $P$ . Закон работает универсально: для любой $P$ утверждение $\neg (P \land \neg P)$ устанавливается одним и тем же коротким рассуждением.

Доказательство exhaustive. Здесь ситуация иная. В чистой CIC утверждение $P \lor \neg P$ — закон исключённого третьего — не выводимо для произвольной пропозиции $P$ . Это важнейший факт, заслуживающий явного разбора.

Зависимость от аксиомы `classic`

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

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

Иначе: алгоритма, который для любой пропозиции $P$ возвращал бы доказательство $P$ или доказательство $\neg P$ , не существует. Многие пропозиции (например, утверждения о бесконечных множествах, утверждения о существовании, многие теоретико-числовые гипотезы) не имеют известного конструктивного решения и могут не иметь его в принципе. Поэтому в чистой CIC закон исключённого третьего как универсальное утверждение не теорема.

Аксиома classic. Чтобы работать с законом исключённого третьего в полной общности, Rocq предоставляет аксиому:

Axiom classic : forall P : Prop, P \/ ~ P.

Эта аксиома постулирует: для любой пропозиции $P$ имеет место $P \lor \neg P$ . Она не доказывается конструктивно (как мы видели); она принимается как утверждение классической логики.

В ToS принятие classic обосновано онтологически: согласно метафизике Тома I, Закон Исключённого Третьего — одно из условий работы Логики на $A = \exists$ . В реальности всегда есть определённое положение дел: либо нечто имеет место, либо не имеет (в одном отношении). То, что у нас нет алгоритма для каждого конкретного $P$ установить, какое именно, не отменяет онтологического факта: положение дел определено.

Конструктивная неразрешимость — эпистемологическое ограничение (невозможность всегда узнать, какое из двух имеет место); classic как аксиома фиксирует онтологическую определённость (одно из двух всегда имеет место). Принятие этой аксиомы — ясное выражение позиции логического реализма, обсуждавшейся в «Почему Prop, а не bool: позиция логического реализма»: Логика онтологически первична, вычислимость — её частный случай.

Здесь важна одна оговорка, чтобы не приписать classic больше, чем она даёт. Аксиома classic P даёт доказательство дизъюнкции $P \lor \neg P$ в Prop — но не даёт вычислимого теста, который возвращал бы true или false в зависимости от того, какая сторона имеет место. Иными словами, classic утверждает, что одно из двух верно, но не указывает — какое. Для построения поля exhaustive этого достаточно: exhaustive есть доказательство $P \lor \neg P$ , не вычисленный индикатор стороны. Но если позже понадобится информативный выбор ветви — вычислительное ветвление, зависящее от того, выполнено ли $P$ , — одной classic мало: нужен дополнительный принцип свидетельствования, обсуждаемый в последующей главе об аксиоматическом слое ToS.

Двойная нумерация и статус. В Методологическом введении было зафиксировано: в онтологии Тома I Закон Исключённого Третьего — производный от Тождества и Непротиворечия; в формальной системе Rocq — самостоятельный $L 3$ , опирающийся на аксиому classic. Это — частный случай двойной нумерации законов, и он касается именно конструкции distinction_of: поле exhaustive в записи Distinction, построенной из произвольной пропозиции $P$ , опирается на classic.

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

Полное доказательство в Rocq

С учётом сказанного, полное определение distinction_of в Rocq имеет вид:

Definition distinction_of (P : Prop) : Distinction.
Proof.
  apply (mkDistinction P (~ P)).
  - (* exclusive : ~(P /\ ~ P) *)
    intros [p np]. exact (np p).
  - (* exhaustive : P \/ ~ P *)
    apply classic.
Defined.

Разберём по строкам.

Definition distinction_of (P : Prop) : Distinction. — объявляем функцию, принимающую пропозицию $P$ и возвращающую акт различения. Использование точки вместо := переключает Rocq в интерактивный режим, позволяющий вести построение по шагам тактиками.
apply (mkDistinction P (~ P)). — применяем конструктор mkDistinction, фиксируя первые два аргумента (positive := P и negative := ~ P). Остаются две цели — обязательства доказательства для полей exclusive и exhaustive.
Первая цель: ~(P /\ ~ P). Раскрываем гипотезу $p : P$ и $n p : \neg P$ , применяем $n p$ к $p$ , получаем False. Записывается одной строкой intros [p np]. exact (np p).
Вторая цель: P \/ ~ P. Применяем аксиому classic: apply classic.
Defined. (а не Qed.) — завершает построение, делая определение прозрачным для дальнейшей работы (термы distinction_of $(P)$ можно раскрывать в других доказательствах).

В математической нотации этот же объект записывается короче:

\text{distinction_of}(P) \;=\; \big(P, \neg P, \varepsilon_P, \eta_P\big),

где $ε_{P}$ — доказательство $\neg (P \land \neg P)$ (конструктивное), а $η_{P}$ — доказательство $P \lor \neg P$ (опирающееся на classic).

Что показывает `distinction_of`

Подведём содержательный итог. Конструкция distinction_of показывает следующее.

Универсальность записи Distinction. Здесь стоит развести два разных утверждения — непустоту формы и её универсальность, — ибо они требуют разного. Что тип Distinction не пуст, видно уже на простейшем примере: различение можно построить из True и False, и для этого никакой классический принцип не нужен — исключительность и исчерпанность пары True / False доказываются прямо. Но distinction_of делает больше, чем показывает непустоту: оно устанавливает универсальность записи. Для каждой пропозиции $P$ есть соответствующее различение distinction_of $(P)$ — каноническое различение $P$ и $\neg P$ . Не существует пропозиций, для которых акт различения не строится. И именно эта универсальность, а не простая непустота, требует классического принципа classic: чтобы для произвольной $P$ предъявить поле exhaustive — доказательство $P \lor \neg P$ . Тип Distinction, стало быть, не просто непуст: он достаточно богат, чтобы охватить весь универсум пропозиций, — и цена этого богатства есть обращение к classic.

Каноническая структура утверждения. Каждая пропозиция несёт в себе каноническое различение между собой и своим отрицанием. Это различение не выбирается извне — оно дано самим утверждением, как только утверждение имеет смысл. Утверждать $P$ значит одновременно различать $P$ и $\neg P$ ; distinction_of делает эту одновременность явной в формальной записи.

Мост между утверждениями и актами. distinction_of есть мост между двумя уровнями работы: уровнем утверждений в Rocq и уровнем актов различения как структурных объектов настоящей работы. Любое утверждение, доступное в Rocq, можно рассмотреть как различение и работать с ним в этой структуре — через четыре поля positive, negative, exclusive, exhaustive.

Подготовка к выводу законов. Из distinction_of будут выведены законы логики $L 1, L 2, L 3, L 4$ как теоремы о свойствах Distinction. Глава 3 покажет конкретно: для любого $D : ‘ D i s t in c t i o n ‘$ , в частности для $D = ‘ d i s t in c t i o n_{o} f ‘ (P)$ , проверяются формальные утверждения, выражающие классические законы логики. Это — центральный результат Части I.

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

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

Минимальность записи: можно ли убрать одно из четырёх полей?

Постановка вопроса

Запись Distinction имеет четыре поля: positive, negative, exclusive, exhaustive. Естественный вопрос, особенно для математической аудитории: является ли это минимальным набором? Можно ли получить ту же содержательную работу с меньшим числом полей?

Этот вопрос — не эстетический. В (см. соответствующую главу) Главы 1 было установлено, что первое формализуемое должно стоять в точке равновесия между минимальностью и продуктивностью. Если запись избыточна, мы получили бы дополнительную структуру, не оправданную близостью к границе формализации. Если бы запись была недостаточна, мы потеряли бы возможность выводить из неё дальнейшие структуры (законы логики, дальнейшие построения). Минимальность — структурная характеристика, которую нужно показать, не постулировать.

Метод показа — структурный анализ: рассмотрим, что произойдёт без каждого из полей по очереди, и убедимся, что в каждом случае запись теряет статус различения. Это — не строгое доказательство в формальной системе (минимальность Distinction есть метатеоретическое наблюдение о выборе формализма, не теорема внутри Rocq), но конкретный структурный анализ, на котором стоит наш выбор.

Без полей `positive` или `negative`

Очевидный случай: без одной из сторон нет самого разделения. Запись с тремя полями — например, positive, exclusive, exhaustive без negative — была бы синтаксически бессмысленной: поля exclusive и exhaustive ссылаются на negative в своих типах ( $\neg (‘ p os i t i v e ‘ \land ‘ n e g a t i v e ‘)$ и $‘ p os i t i v e ‘ \lor ‘ n e g a t i v e ‘$ соответственно). Без negative эти типы невозможно даже записать.

Этот случай не требует подробного анализа: positive и negative — две стороны разделения; без обеих разделения нет. Более интересны случаи, когда сами стороны на месте, но одно из условий (exclusive или exhaustive) отсутствует.

Без поля `exclusive`

Рассмотрим запись, в которой поле exclusive удалено:

Record Distinction_NoExcl := mkDistinction_NoExcl {
  positive   : Prop;
  negative   : Prop;
  exhaustive : positive \/ negative
}.

Что мы получили?

В этой структуре positive и negative могут быть одновременно истинны. Никакое условие не запрещает их совпадения. Это означает, что мы можем построить экземпляр такой записи с противоречивым содержанием:

Definition trivial_both : Distinction_NoExcl :=
  mkDistinction_NoExcl True True (or_introl I).

Здесь positive := True, negative := True; поле exhaustive тривиально выполнено (True $\vee$ True — даже одна из сторон даёт всё условие). Получаем «запись», в которой обе стороны одновременно истинны — что есть прямое нарушение самой природы разделения.

Что это значит структурно. Без поля exclusive утрачивается взаимное исключение как часть структуры. Закон Непротиворечия $L 2$ перестаёт быть встроенным в саму запись — он работает «извне», и пришлось бы каждый раз отдельно проверять, что конкретные positive и negative в самом деле несовместны.

Это — не просто неудобство. Это потеря онтологической функции записи. Различение по определению есть структурное разделение на две несовместные стороны; убрав условие несовместности, мы получаем не различение, а лишь пару утверждений, одно из которых имеет место. Это совсем другой объект, выражающий не работу Логики на $A = \exists$ , а лишь дизъюнкцию двух пропозиций.

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

Без поля `exhaustive`

Рассмотрим обратный случай — запись без поля exhaustive:

Record Distinction_NoExh := mkDistinction_NoExh {
  positive  : Prop;
  negative  : Prop;
  exclusive : ~(positive /\ negative)
}.

Что мы получили теперь?

Здесь positive и negative могут быть одновременно ложны. Условие исключительности тривиально выполняется, когда оба утверждения ложны (ложные утверждения не могут совпасть в истинном конъюнктивном высказывании). Мы можем построить:

Definition trivial_neither : Distinction_NoExh :=
  mkDistinction_NoExh False False
    (fun H => match H with conj h _ => h end).

positive := False, negative := False; условие exclusive тривиально (если оба ложны, их конъюнкция тоже ложна, её отрицание истинно). Получаем «запись», в которой ни одна сторона не имеет места — что также есть прямое нарушение самой природы разделения.

Что это значит структурно. Без поля exhaustive утрачивается совместная исчерпанность как часть структуры. Закон Исключённого Третьего $L 3$ перестаёт быть встроенным в запись — может появиться «третий путь», состояние «ни положительное, ни отрицательное», которое разрушает идею полного разделения.

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

Резюме: четыре поля необходимы

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

Поле	Работа	Что теряется без него
`positive`	Содержание положительной стороны	Сторона разделения отсутствует
`negative`	Содержание отрицательной стороны	Сторона разделения отсутствует
`exclusive`	Невозможность совпадения сторон	Стороны могут быть одновременно истинны — разделение распадается
`exhaustive`	Отсутствие третьего между сторонами	Стороны могут быть одновременно ложны — появляется «третий путь»

Каждое поле отвечает за одну работу в структуре акта различения; ни одно не дублирует другое; ни одно не может быть выведено из остальных.

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

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

Можно ли расширить запись?

Логично спросить и обратное: если четыре поля — минимум, то можно ли добавить пятое и получить более богатую структуру?

Формально — да, никто не запрещает добавить дополнительное поле. Однако такое расширение не было бы первым формализуемым в смысле Главы 1: оно содержало бы дополнительные структуры, не оправданные близостью к границе формализации.

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

Дальнейшие расширения — в последующих главах. Это не означает, что настоящий том не вводит структуры, расширяющие Distinction. Напротив, в последующих главах появятся:

В Главе 6 (Часть I) — тип Level как самостоятельная структура для формализации Закона Порядка $L 5$ . Level не входит в саму Distinction, потому что $L 5$ относится к иерархии актов различения, не к внутренней структуре одного акта.
В Части III — структуры отношений между различениями, опирающиеся на Distinction как на базовый объект, но вводящие свою собственную надстройку.
В Части XI — алгебраические структуры (группы, кольца), в которых Distinction используется опосредованно через записи о свойствах элементов и операций.

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

Подготовка к Главе 3 и далее

Минимальность Distinction имеет прямое следствие для Главы 3, в которой из этой записи будут выведены законы логики $L 1, L 2, L 3, L 4$ как теоремы Rocq.

Поскольку каждое из четырёх полей записи отвечает за конкретную работу (тождество сторон, исключение, исчерпанность, совместное обоснование через ЗДО), каждый из выводимых законов будет естественно опираться на одно из полей или их сочетание. Глава 3 покажет это конкретно: $L 1$ выводится из positive и negative (тождество сторон); $L 2$ — из exclusive; $L 3$ — из exhaustive; $L 4$ — как самозаземление различения: из положительной стороны вместе с exclusive (наличие положительной стороны и исключительность дают основание отрицать отрицательную сторону).

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

Установив минимальность записи, мы можем перейти к последнему содержательному вопросу Главы 2: как соотносятся положительная и отрицательная стороны? Можно ли построить Distinction, имея только одну из них? Анонс этой темы — предмет следующего раздела, с полным разворачиванием в последующей главе о со-определении положительного и отрицательного.

Со-определение положительного и отрицательного

Невозможность построить `Distinction` без обеих сторон

Установив минимальность записи Distinction, мы можем сделать ещё одно структурное наблюдение, которое будет иметь существенные следствия для всей дальнейшей работы. Из определения

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

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

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

Структурное единство сторон

Когда мы определяем positive := P, мы одновременно определяем структурно negative как $\neg P$ — именно так работает универсальная конструкция distinction_of $(P)$ , разобранная в «Конструкция distinction_of: построение различия из пропозиции». Положительная сторона определяется в опоре на отрицательную, и наоборот: само то, что положительная сторона полагает, имеет смысл только через различение от того, что отрицательная сторона отрицает.

Иными словами: положительное и отрицательное не существуют отдельно; они со-определяются в одном акте.

Этот принцип — глубокий онтологический факт о структуре различения, согласованный с зафиксированной в Методологическом введении позицией: математика как язык описания логической структуры реальности. В реальности нет «положительного без своего отрицательного» — любое утверждение о реальном получает смысл через различение от того, что оно не утверждает. Сказать «это — ось симметрии $C_{3}$ » — значит одновременно сказать, чем эта ось не является (не $C_{2}$ , не $C_{4}$ , не $C_{6}$ ). Сказать «функция $f$ непрерывна в точке $x_{0}$ » — значит одновременно сказать, что она не разрывна в этой точке. Положительное содержание утверждения и его отрицание приходят вместе.

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

С этим разделом основное содержание Главы 2 завершено. Запись Distinction введена; её типизация в Prop обоснована; универсальная конструкция distinction_of построена; минимальность записи показана; принцип со-определения положительного и отрицательного зафиксирован. Остаётся подвести итог Главы 2 — что было достигнуто. Этому посвящён последний раздел.

Итог Главы 2

Глава 2 ввела первый формальный объект настоящей работы — запись Distinction, формализующую акт различения. Подведём итог достигнутого.

Что мы получили

Первый формализуемый объект. Структурная запись Record Distinction с четырьмя полями (positive, negative, exclusive, exhaustive) — формальная запись на языке Rocq логической структуры акта различения, как он работает в реальности. Четыре поля соответствуют четырём моментам акта, содержательно разобранным в «Структура акта различения», и работают как аспекты одного целого, не как независимые утверждения.

Типизация в Prop. Положительная и отрицательная стороны различения — пропозиции, не вычислимые булевские значения. Это — конкретное проявление позиции логического реализма, зафиксированной в «Почему Prop, а не bool: позиция логического реализма»: Логика онтологически первична, вычислимость — её частный случай. Каждое утверждение о реальном имеет смысл независимо от наличия алгоритма проверки, и формальная запись на языке математики должна сохранять эту структуру.

Универсальная конструкция distinction_of. Для любой пропозиции $P$ конструкция distinction_of $(P)$ строит соответствующее различение с положительной стороной $P$ и отрицательной $\neg P$ . Это — мост между утверждениями Rocq и актами различения как структурными объектами: всякое содержательное утверждение о реальном автоматически несёт в себе каноническое различение.

Зависимость от classic. Конструкция distinction_of опирается на аксиому classic ( $\forall P, P \lor \neg P$ ) для построения поля exhaustive. Эта зависимость — техническая: в чистой CIC закон исключённого третьего не выводим. Онтологически закон производный (от Тождества и Непротиворечия); формально — самостоятельная аксиома, что согласуется с двойной нумерацией законов, зафиксированной в Методологическом введении.

Минимальность записи. Структурный анализ («Минимальность записи: можно ли убрать одно из четырёх полей?») показал: каждое из четырёх полей необходимо; удаление любого из них приводит к потере статуса различения. Без exclusive стороны могут совпасть (запись теряет исключительность); без exhaustive стороны могут отсутствовать обе (запись теряет полноту). Минимальность Distinction — структурное свойство, а не выбор удобства, согласованное с положением этой записи как первого формализуемого (Глава 1, § 1.4).

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

Связь с Главой 1

В Главе 1 была установлена методологическая матрица настоящего тома: при встрече со структурной границей формализации признать её, не сокращать, и двинуться к ближайшему формализуемому объекту. В Главе 2 эта матрица была применена впервые.

Признание границы. $A = \exists$ остаётся пред-формальным основанием, не формализуется в записях Rocq. Граница, установленная в § 1.3, сохраняется.
Не сокращать. Не вводятся искусственные конструкции, пытающиеся обойти эту границу (как Axiom A_exists : True или подобные); $A = \exists$ остаётся как фундаментальный факт онтологии Тома I.
Двинуться к ближайшему формализуемому. Этим формализуемым оказался акт различения, развёрнутый в Главе 2 как Distinction. Первое формальное определение сделано; собственно математическая работа начата.

В этом смысле Глава 2 завершает работу, начатую в Главе 1: то, на что указывала Глава 1 как на первое формализуемое, в Главе 2 стало реальным объектом Rocq, готовым для дальнейших построений.

Связь с онтологической позицией

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

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

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

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

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

Навигация: ← Глава 1. Первоначало: A = ∃ · Глава 3. Вывод законов логики из Distinction →

Spencer-Brown G., Laws of Form. London: Allen & Unwin, 1969. Русский перевод: Спенсер-Браун Дж., Законы формы / Пер. Б. А. Старостина, А. С. Карпенко. Москва: Аграф, 2009. ↩
Соссюр Ф. де, Курс общей лингвистики. Москва: Логос, 1998. Оригинал: de Saussure F., Cours de linguistique générale, 1916. ↩
Heidegger M., Identität und Differenz. Pfullingen: Neske, 1957. Русский перевод: Хайдеггер М., Идентичность и различие / Пер. А. В. Денежкина. Москва: Гнозис, 1997. ↩
Derrida J., Marges de la philosophie. Paris: Minuit, 1972. Русский перевод: Деррида Ж., Поля философии / Пер. Д. Ю. Кралечкина. Москва: Академический Проект, 2012. ↩
Аристотель, Метафизика, IV.3 1005b19–23. Греческий оригинал: $\overset{α}{˙} δ \overset{v}{ˊ} ν α τ o ν$ $γ \overset{α}{ˋ} ρ$ $\overset{o}{˙} τ ιo \tilde{v} ν$ $τ \overset{o}{˙}$ $α \overset{v}{˙} τ \overset{o}{˙}$ $\overset{v}{˙} π \overset{α}{ˊ} ρ χ ε ι ν$ $τ ε$ $κ α \overset{ι}{ˋ}$ $μ \overset{η}{ˋ}$ $\overset{v}{˙} π \overset{α}{ˊ} ρ χ ε ι ν$ $τ \tilde{ω}$ $α \overset{v}{˙} τ \tilde{ω}$ $κ α \overset{ι}{ˋ}$ $κ α τ \overset{α}{ˋ}$ $τ \overset{o}{˙}$ $α \overset{v}{˙} τ \overset{o}{ˊ}$ . ↩

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

Проводник