Глава 3. Вывод законов логики из Distinction

От структуры к теоремам: постановка задачи

Что было установлено в Главе 2

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

В завершении Главы 2, в (см. соответствующую главу), было обозначено соответствие, к которому Глава 3 теперь обращается систематически:

• Закон Тождества $L1$ опирается на поля positive и negative (тождественность сторон).
• Закон Непротиворечия $L2$ опирается на поле exclusive.
• Закон Исключённого Третьего $L3$ опирается на поле exhaustive.
• Закон Достаточного Основания $L4$ опирается на саму структуру записи как целого — через требование обоснований для всех полей.

Это соответствие — не риторическое наблюдение. В настоящей главе каждое из перечисленных утверждений будет формально доказано средствами Rocq. Технической опорой служит файл LawsFromDistinction.v репозитория ToS-Coq.

Законы логики и их вывод как теоремы

Онтологическая первичность законов логики. Прежде всего важно зафиксировать онтологический статус законов логики. Согласно метафизике Тома I и зафиксированной в Методологическом введении позиции, законы $L1$, $L2$, $L3$, $L4$, $L5$ — онтологически первичны. Они не следуют из чего-либо более первого; они — сама структура работы Логики на $A=\exists$, условия самой возможности существования чего-либо определённого. Без них не было бы ни актов различения, ни записи Distinction, ни какой-либо формальной системы вообще. Это — факт онтологии, не следствие математической работы.

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

Различие важно. Когда мы говорим, что закон $L1$ «выводится как теорема о Distinction», мы не утверждаем, что в реальности закон тождества возникает из акта различения или зависит от него. Мы утверждаем нечто иное: в формальной записи на языке Rocq имеется структурное соответствие между полями Distinction и законами логики, и это соответствие может быть зафиксировано как доказуемое в Rocq утверждение.

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

Согласно зафиксированной в Методологическом введении позиции — математика как язык описания логической структуры реальности — формальные теоремы Главы 3 описывают, как законы логики проявляются в простейшей формализуемой структуре. Они не создают законы, не постулируют их, не выводят их из чего-то более первого. Они лишь делают видимой ту структуру работы Логики, которая в реальности работает всегда.

Двойная нумерация в работе. В Методологическом введении уже была зафиксирована двойная нумерация законов: онтологическая (Том I) и формальная (Rocq). Онтологически ЗДО работает как мета-закон над всеми остальными; Тождество и Непротиворечие первичны как структурные условия; Закон Исключённого Третьего онтологически производный от них; Закон Порядка — структурное условие иерархии. Формально в Rocq все пять законов представлены самостоятельными теоремами: $L3$ опирается на аксиому classic, $L5$ — на отдельный тип Level. Эта двойственность — не противоречие, а два уровня одной работы: онтологический статус и формальное доказательство.

Технический источник деривации

Технической основой настоящей главы служит файл LawsFromDistinction.v (директория src/foundation/) репозитория ToS-Coq. Файл импортирует две зависимости:

From ToS Require Import foundation.Distinction.
From ToS Require Import TheoryOfSystems_Core_ERR.

Первый импорт — запись Distinction и связанные конструкции (включая distinction_of), разобранные в Главе 2. Второй — файл, содержащий тип Level и связанные с ним структуры порядка (формализация $L5$).

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

• $L1$ и $L2$ имеют три формы — общую (в стандартной логической формулировке для произвольной пропозиции, например Law_of_Identity : forall A, A = A), структурную (как утверждение о произвольной Distinction, например L1_through_distinction) и каноническую (применённую к каноническому различению distinction_of $(P)$).
• $L3$ имеет три формы — общую через аксиому classic, структурную через поле exhaustive и теорему равносильности L3_independence.
• $L4$ имеет четыре формы — самообоснования, контрапозиции, канонического двойного отрицания и классического устранения двойного отрицания.
• $L5$ вынесен в отдельный аппарат типа Level и представлен своим набором теорем о порядке уровней.

Такое неравное распределение форм не случайно: оно отражает различие формального статуса законов — $L1$ и $L2$ конструктивны и читаются из записи прямо, $L3$ требует классической аксиомы, $L4$ имеет несколько рабочих сторон, а $L5$ опирается на отдельный слой формализации. Глава разбирает каждый закон в том числе форм, в каком он действительно представлен в файле.

Перейдём к первому закону — Закону Тождества, и к его формальному представлению как теоремы о Distinction.

Закон Тождества ($L1$)

Формулировка

Закон Тождества — утверждение, что нечто тождественно самому себе. Онтологически это структурное условие самой определённости: без тождества положительная сторона различения не могла бы быть определённой стороной, а растворилась бы в неразличимом (см. (см. соответствующую главу) Главы 2). Закон не вводится нами и не выводится из чего-то более первого — он есть условие самой возможности существования чего-либо определённого.

В формальной системе Rocq закон представлен утверждением о произвольной пропозиции:

$$\forall A:\mathbf{Prop},A=A.$$

В терминах акта различения: положительная сторона тождественна себе; отрицательная сторона тождественна себе.

Три формы теоремы

Файл LawsFromDistinction.v представляет $L1$ в трёх формах, соответствующих трём уровням работы: общим пропозициям, структуре Distinction, каноническому различению.

Общая форма: Law_of_Identity. Самая простая формулировка — для произвольной пропозиции:

Theorem Law_of_Identity : forall (A : Prop), A = A.
Proof. reflexivity. Qed.

Доказательство состоит из единственной тактики reflexivity — встроенной в Rocq тактики, которая закрывает цели вида $x=x$ прямой ссылкой на правило типового равенства (рефлексивность). Это означает, что утверждение вычислимо распознаётся системой как тривиально истинное — без обращения к каким-либо аксиомам, без какой-либо содержательной работы.

Через структуру различения: L1_through_distinction. Закон, выраженный как утверждение о произвольном акте различения:

Theorem L1_through_distinction : forall D : Distinction,
  positive D = positive D /\ negative D = negative D.
Proof. intro D; split; reflexivity. Qed.

Здесь утверждается, что обе стороны произвольного акта различения — положительная и отрицательная — тождественны самим себе. Доказательство: взять произвольное $D$, разделить конъюнкцию на две цели, каждая закрывается тактикой reflexivity. Снова — ни одной аксиомы, ни одного содержательного шага.

Каноническая форма: L1_distinction_preserves. Закон, применённый к каноническому различению, построенному из произвольной пропозиции:

Theorem L1_distinction_preserves : forall P : Prop,
  positive (distinction_of P) = P.
Proof. reflexivity. Qed.

Здесь утверждается: положительная сторона канонического различения, построенного из $P$, есть сама $P$. Это формальная фиксация того, что конструкция distinction_of $(P)$, разобранная в (см. соответствующую главу) Главы 2, сохраняет содержание исходной пропозиции в положительной стороне — что есть прямое выражение $L1$: $P$ остаётся $P$, не превращаясь во что-либо иное.

Тривиальность доказательств

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

Конкретно: поля positive и negative имеют тип Prop (см. (см. соответствующую главу)); пропозиции в CIC автоматически удовлетворяют рефлексивности типового равенства; positive и negative как стороны акта различения по определению являются определёнными пропозициями, не размытыми. Доказательство $L1$ не добавляет ничего к этому устройству — оно лишь фиксирует его как теорему.

В этом смысле тривиальность доказательства есть методологическое свидетельство: $L1$ так непосредственно соответствует структуре полей positive и negative, что между структурой и законом нет дополнительных шагов. Закон Тождества уже встроен в саму типизацию записи.

Содержательный смысл

В соответствии с зафиксированной позицией — математика как язык описания логической структуры реальности — эти формальные теоремы описывают конкретный аспект работы Логики в реальном существующем.

В реальности всякая определённость предполагает тождество того, что определено. Если конкретная физическая система имеет определённое состояние, это состояние есть это состояние, а не другое. Если математическое утверждение «функция $f$ непрерывна в точке $x_0$» имеет смысл, то само это утверждение тождественно себе в любом контексте, где оно используется — иначе само понятие «утверждать» теряло бы смысл. Если химическая молекула имеет ось симметрии $C_3$, то именно $C_3$, а не $C_2$ или $C_4$.

Теоремы $L1$ в Rocq не создают этого структурного факта реальности. Они дают ему формальную запись на языке записи: положительная сторона тождественна себе (L1_through_distinction); конструкция канонического различения сохраняет исходную пропозицию (L1_distinction_preserves). Эти теоремы — не утверждения о самой реальности, а свойства формального объекта Distinction, согласующегося с реальностью благодаря тому, что запись построена как формализация реальной структуры акта различения.

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

Закон Непротиворечия ($L2$)

Формулировка

Закон Непротиворечия — утверждение, что нечто не может быть собой и не собой одновременно в одном отношении. Онтологически это структурное условие самой возможности разделения: без взаимного исключения положительной и отрицательной сторон само разделение распалось бы, поскольку «положительная» и «отрицательная» стороны слились бы в одно (см. (см. соответствующую главу) Главы 2). Как и $L1$, $L2$ — не следствие математической работы, а условие самой возможности существования чего-либо определённого.

В формальной системе Rocq закон представлен утверждением о произвольной пропозиции:

$$\forall A:\mathbf{Prop},\neg (A\wedge \neg A).$$

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

Три формы теоремы

Файл LawsFromDistinction.v представляет $L2$ в трёх формах, параллельных формам $L1$ («Закон Тождества ()»).

Общая форма: Law_of_NonContradiction. Для произвольной пропозиции:

Theorem Law_of_NonContradiction : forall (A : Prop), ~(A /\ ~A).
Proof. intros A [Ha Hna]. exact (Hna Ha). Qed.

Доказательство содержит три тактики:

• intros A [Ha Hna] — введение параметра $A$ и разбор гипотезы $A\wedge \neg A$ на её составляющие: Ha : A (доказательство $A$) и Hna : ~ A (доказательство $\neg A$).
• exact (Hna Ha) — применение Hna (имеющего тип $A\to \mathtt{False}$) к Ha (имеющему тип $A$), что даёт элемент типа False — противоречие, которое и требовалось получить.
• Qed — завершение доказательства.

В отличие от $L1$, здесь есть содержательная работа: мы применяем функциональную природу отрицания ($\neg A=A\to \mathtt{False}$) для получения противоречия. Но эта работа — конструктивная: не требует обращения к каким-либо аксиомам. $L2$ доказуем средствами самой CIC, без расширений.

Через структуру различения: L2_from_distinction. Закон, выраженный как утверждение о произвольной Distinction:

Theorem L2_from_distinction : forall D : Distinction,
  ~(positive D /\ negative D).
Proof. exact L2_exclusivity. Qed.

Доказательство — одна строка: exact L2_exclusivity, где L2_exclusivity — вспомогательная лемма,¹ выражающая работу поля exclusive как утверждения о произвольной Distinction. Само поле exclusive D имеет тип $\neg (‘positive‘D\wedge ‘negative‘D)$, то есть есть прямое доказательство нужного утверждения для конкретного $D$; лемма L2_exclusivity лишь обобщает это до утверждения о любом $D$.

Это — характерная черта работы с записями в Rocq, обсуждавшаяся в (см. соответствующую главу) Главы 2: поля записи сами по себе являются доказательствами соответствующих утверждений. Теорема $L2$ через структуру различения — лишь формальная регистрация того, что доказательство уже есть, встроенное в саму запись.

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

Theorem L2_canonical : forall P : Prop, ~(P /\ ~P).
Proof. intros P [Hp Hnp]. exact (Hnp Hp). Qed.

{ Доказательство дословно повторяет общую форму — L2_canonical и Law_of_NonContradiction тождественны по содержанию. Различие — лишь в позиции в файле и в имени. Здесь важно уточнить, в каком смысле эта форма каноническая: теорема называется так не потому, что синтаксически содержит distinction_of — она работает с произвольной пропозицией $P$ напрямую, — а потому, что относится к канонической паре $P/\neg P$, которая и лежит в основе конструкции distinction_of $(P)$. Каноничность здесь — по предмету (каноническая пара), не по синтаксису записи. }

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

Существенное отличие $L2$ от $L1$ в формальной структуре состоит в следующем. Для $L1$ доказательство тривиально, поскольку рефлексивность типового равенства встроена в саму CIC. Для $L2$ же доказательство опирается на конкретное поле записи — exclusive. Без этого поля закон $L2$ не следовал бы из записи Distinction; пришлось бы постулировать его отдельно или доказывать сложным образом.

Это согласуется с минимальностью записи, разобранной в (см. соответствующую главу) Главы 2: было показано, что без поля exclusive запись теряет статус различения, поскольку положительная и отрицательная стороны могут совпасть. Глава 3 даёт формальный коррелят этому наблюдению: без поля exclusive теорема L2_from_distinction не могла бы быть доказана.

Таким образом, поле exclusive играет двойную роль: содержательно оно фиксирует взаимное исключение сторон акта различения; формально оно есть встроенное доказательство $L2$ для каждой Distinction.

Содержательный смысл

В соответствии с зафиксированной позицией — математика как язык описания логической структуры реальности — теоремы $L2$ описывают конкретный аспект работы Логики в реальном существующем.

В реальности невозможно одновременное наличие и отсутствие одного и того же признака в одном отношении. Молекула не может одновременно иметь и не иметь ось симметрии $C_3$ (в одном отношении к конкретной геометрии и оси). Электрон не может одновременно находиться и не находиться в данном квантовом состоянии (для данной системы измерений). Утверждение «функция $f$ непрерывна в точке $x_0$» не может одновременно быть истинным и ложным (для данного $f$ и данного $x_0$).

Уточнение «в одном отношении» — ключевое, и оно уже было разобрано в (см. соответствующую главу) Главы 2 со ссылкой на формулировку Аристотеля в Метафизике IV.3. Этот же объект (например, химическое вещество) может иметь одну симметрию в одном отношении и не иметь другой в другом отношении; здесь нет противоречия. Закон Непротиворечия запрещает лишь одновременное наличие и отсутствие одного и того же признака в одном и том же отношении.

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

С $L1$ и $L2$ установлены тождество сторон и невозможность их одновременного совпадения. Следующий закон — $L3$ — касается полноты разделения: отсутствия третьего между сторонами.

Закон Исключённого Третьего ($L3$)

Двойной статус закона

Закон Исключённого Третьего занимает особое место среди законов логики. Онтологически он есть условие полноты разделения: при всяком акте различения, в котором уже работают тождество сторон ($L1$) и их исключительность ($L2$), не остаётся места для «третьего» — чего-то, что не было бы ни положительной, ни отрицательной стороной. Это следствие совместной работы первых двух законов на структурном уровне: если есть тождество и есть исключительность, то между сторонами уже нет пространства для иного.

Онтологически $L3$ есть, таким образом, производный закон, выводящийся из совместной работы $L1$ и $L2$. Этот вывод зафиксирован в метафизике Тома I и кратко напомнен в (см. соответствующую главу) Главы 2: если нечто есть определённо (Тождество) и не может одновременно быть и не быть (Непротиворечие), то самим строением различения не оставлено места для третьего. Это — структурное следствие, не самостоятельное условие.

Здесь необходима оговорка, чтобы не возникло недоразумения. Сказанное не есть утверждение, что $L3$ формально выводится из $L1$ и $L2$ в интуиционистской логике. Внутри CIC такой вывод невозможен: интуиционистская логика принимает и рефлексивность равенства, и непротиворечие, но не доказывает $P\vee \neg P$ для произвольной пропозиции $P$. Речь идёт об онтологическом тезисе ToS: полный акт различения не оставляет третьей области между положительной и отрицательной сторонами. Это тезис о структуре различения, а не теорема формального исчисления. Формально же эта полнота фиксируется через аксиому classic — именно потому, что онтологический тезис не имеет конструктивного формального двойника.

Формально в Rocq, однако, $L3$ как утверждение для произвольной пропозиции $\forall P:\mathbf{Prop},P\vee \neg P$ не выводимо конструктивно. Причина обсуждалась в (см. соответствующую главу) Главы 2: чтобы конструктивно доказать дизъюнкцию для произвольной $P$, нужно предъявить конкретный путь — доказательство $P$ или доказательство $\neg P$. Но без знания содержания $P$ алгоритм такого предъявления невозможен. Поэтому в CIC закон фиксируется как аксиома classic.

В этом — двойной статус $L3$: онтологически производный (от $L1$ и $L2$ в структуре различения), формально самостоятельный (поскольку CIC не воспроизводит онтологический вывод). Эта двойственность не противоречие, а проявление различия между онтологической структурой Логики и техническими возможностями конкретной формальной системы.

Формулировка

В формальной системе Rocq закон представлен утверждением о произвольной пропозиции:

$$\forall A:\mathbf{Prop},A\vee \neg A.$$

В терминах акта различения: для произвольного $D:‘Distinction‘$ имеет место $‘positive‘D\vee ‘negative‘D$.

Аксиома classic и её роль

В файле Distinction.v, а через него и в LawsFromDistinction.v, постулируется аксиома:

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

Эта аксиома — одна из двух фундаментальных аксиом репозитория ToS-Coq (вторая — L4_witness, обсуждаемая в последующей главе об аксиоматическом слое). Она утверждает: для всякой пропозиции $P$ имеет место $P\vee \neg P$.

Принципиальный комментарий из репозитория. В исходном коде файла LawsFromDistinction.v к этой аксиоме приложен комментарий, который заслуживает явного цитирования:

L3 is not an EXTRA axiom: it IS our formalization of «distinction is exhaustive». classic = L3.

Это утверждение требует прояснения — и точности. Технически classic является аксиоматическим расширением конструктивной основы CIC: в чистом исчислении индуктивных конструкций утверждение $\forall P,P\vee \neg P$ не доказуемо, и classic добавляется к системе как классический принцип. Отрицать этот технический факт не следует. Но цитированный комментарий говорит о другом — не о техническом статусе classic в CIC, а о её месте внутри ToS. И здесь classic не есть внешняя, посторонняя добавка к онтологии: это формальная запись закона $L3$ — одного из четырёх моментов акта различения, совместной исчерпанности ((см. соответствующую главу) Главы 2). Поле exhaustive в записи Distinction есть конкретное проявление того же содержания: оно постулирует, что для конкретного акта различения $D$ обязательно имеет место одна из двух сторон. Аксиома classic обобщает это до утверждения о произвольной пропозиции.

Таким образом, два уровня нужно держать раздельно. На уровне техники classic — аксиоматическое расширение CIC. На уровне онтологии ToS classic не добавляется к структуре Distinction как нечто чуждое, а выражает в общей форме то, что уже встроено в саму запись через поле exhaustive. Это формальный коррелят онтологического положения: совместная исчерпанность — необходимый момент акта различения, без которого само разделение было бы неполным.

Онтологическое обоснование принятия аксиомы. Принятие classic в ToS обосновано онтологически: согласно метафизике Тома I, в реальности всегда есть определённое положение дел — либо нечто имеет место, либо не имеет (в одном отношении). То, что у нас нет алгоритма для каждой конкретной пропозиции $P$ установить, какое именно положение имеет место, не отменяет онтологического факта: положение дел определено. Конструктивная неразрешимость — эпистемологическое ограничение (невозможность всегда узнать); аксиома classic — фиксация онтологической определённости (одно из двух всегда имеет место).

Формальные теоремы

Файл LawsFromDistinction.v представляет $L3$ в трёх формах.

Общая форма: Law_of_ExcludedMiddle. Закон в стандартной формулировке для произвольной пропозиции:

Theorem Law_of_ExcludedMiddle : forall (A : Prop), A \/ ~A.
Proof. exact classic. Qed.

Доказательство — одна строка: exact classic. Теорема есть прямое применение аксиомы classic к произвольной пропозиции. Это — буквальное выражение того, что цитированный выше комментарий формулирует словами: classic = L3.

Через структуру различения: L3_from_distinction. Закон, выраженный как утверждение о произвольной Distinction:

Theorem L3_from_distinction : forall D : Distinction,
  positive D \/ negative D.
Proof. exact L3_totality. Qed.

{ Доказательство опирается на вспомогательную лемму L3_totality,² выражающую работу поля exhaustive как утверждения о произвольной Distinction. Само поле exhaustive D имеет тип $‘positive‘D\vee ‘negative‘D$, то есть есть прямое доказательство нужного утверждения для конкретного $D$; лемма L3_totality обобщает это до утверждения о любом $D$. }

{ В отличие от Law_of_ExcludedMiddle, L3_from_distinction не требует прямого обращения к аксиоме classic в своём доказательстве — ему достаточно поля exhaustive. Однако само существование поля exhaustive с произвольным содержимым в записи Distinction обеспечивается, в конечном счёте, той же аксиомой: универсальная конструкция distinction_of $(P)$ ((см. соответствующую главу) Главы 2) опирается на classic при построении поля exhaustive для произвольной $P$. Таким образом, classic работает в distinction_of, а L3_from_distinction работает с уже-построенной Distinction. }

Равносильность classic и $L3$-через-различение: L3_independence. Файл содержит ещё одну теорему о $L3$, замыкающую картину:

Theorem L3_independence :
  (forall D : Distinction, positive D \/ negative D)
  -> (forall P : Prop, P \/ ~ P).
Proof. intros _ P. exact (classic P). Qed.

Она утверждает: исключённое третье для всякого акта различения влечёт исключённое третье для всякой пропозиции. Вместе с L3_from_distinction, дающей обратное направление, это показывает, что $L3$-через-различение и classic равносильны по силе — то же самое тождество classic $=$ $L3$, проведённое теперь в обе стороны. Имя теоремы — L3_independence — указывает на её роль: $L3$ не сводится к остальным законам, он несёт собственное содержание, ровно совпадающее с содержанием classic. Стоит, впрочем, оговорить точно, что теорема не делает: она не доказывает — и не может доказать внутри Rocq — метатеоретический тезис о том, что конструктивная логика удовлетворяет $L1,L2,L4,L5$, но не $L3$ (этот тезис подлинно метатеоретичен, ибо говорит о системе без classic, тогда как мы работаем в системе с classic). Теорема фиксирует внутренне доступную часть: точное совпадение $L3$-через-различение и classic.

Поле exhaustive и связь с минимальностью

Положение, параллельное случаю $L2$: для $L3$ доказательство L3_from_distinction опирается на конкретное поле записи — exhaustive. Без этого поля закон $L3$ не следовал бы из записи Distinction.

Это снова согласуется с минимальностью записи, разобранной в (см. соответствующую главу) Главы 2: было показано, что без поля exhaustive запись теряет статус полного разделения, поскольку между сторонами может оказаться «третий путь». Глава 3 даёт формальный коррелят: без поля exhaustive теорема L3_from_distinction не была бы доказуемой; пришлось бы для каждого конкретного $D$ отдельно применять classic к конкретным $‘positive‘D$ и $‘negative‘D$, что противоречит идее структуры различения как самостоятельного объекта.

Таким образом, поля exclusive и exhaustive играют параллельные роли: содержательно они фиксируют две стороны полноты разделения (исключительность и исчерпанность); формально они служат встроенными доказательствами $L2$ и $L3$ соответственно для каждой Distinction.

Содержательный смысл

В соответствии с зафиксированной позицией — математика как язык описания логической структуры реальности — теоремы $L3$ описывают конкретный аспект работы Логики в реальном существующем.

В реальности всякое определённое положение дел определено: либо нечто имеет место, либо не имеет. Молекула либо обладает осью симметрии $C_3$, либо не обладает (в одном отношении к конкретной геометрии). Целое число либо чётно, либо нет. Утверждение либо истинно для данной ситуации, либо нет. Третьего — состояния «ни истинно, ни ложно» — нет в реальной онтологии определённого существования.

Уточнение «в одном отношении», обсуждавшееся при $L2$, действует и здесь: один и тот же объект может находиться в разных положениях по разным признакам или в разных отношениях, и в каждом отношении закон $L3$ работает по отдельности.

Теоремы $L3$ в Rocq не создают этого структурного факта реальности. Они дают ему формальную запись через поле exhaustive и аксиому classic: внутри произвольного акта различения положительная или отрицательная сторона обязательно имеет место. Аксиома classic не добавляет ничего к структуре акта различения — она лишь выражает в общей форме тот факт, который уже встроен в саму запись через поле exhaustive.

С $L1$, $L2$ и $L3$ установлены тождество сторон, невозможность их совпадения и отсутствие третьего между ними. Следующий закон — $L4$ — обращается к обоснованности самого акта различения, и здесь работа выходит за рамки одной записи Distinction к её свойствам как структуры.

Закон Достаточного Основания ($L4$)

Онтологический статус: мета-закон

Закон Достаточного Основания занимает в ToS особое положение среди пяти законов логики, отличное от $L1$, $L2$ и $L3$.

Онтологически, согласно метафизике Тома I, $L4$ — мета-закон. Он не работает «наряду» с Тождеством, Непротиворечием и Исключённым Третьим как один из равноправных законов; он работает над ними, как само действие Логики, в котором обоснование становится возможным. $L1$, $L2$, $L3$ суть структурные условия определённости; $L4$ — мета-структура, в которой эти условия имеют силу, поскольку каждое из них обосновано.

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

Эта мета-роль $L4$ выражается в Rocq двояко. С одной стороны, она встроена в самую систему типов CIC: всякое определение требует обоснования (это типы), всякая теорема требует доказательства (это термы доказательств), всякая конструкция должна быть проверяемой (это ядро системы). Эта встроенность была обсуждена в (см. соответствующую главу) Главы 2 как «работа ЗДО как организационного принципа формальной системы».

С другой стороны, в Rocq есть и конкретное формальное выражение $L4$ — как свойства записи Distinction. Этому выражению и посвящён настоящий раздел.

Формализация: самообоснование

В LawsFromDistinction.v закон Достаточного Основания формализуется через утверждение о самообосновании (self-grounding) акта различения. Содержание этого утверждения таково: для произвольной Distinction $D$, если имеет место положительная сторона, то отрицательная сторона места не имеет.

В формальной записи:

$$\forall D:‘Distinction‘,‘positive‘D\to \neg ‘negative‘D.$$

Почему именно эта формулировка. На первый взгляд эта запись может показаться удалённой от классического ЗДО («всё имеет основание»). Но связь содержательна, и заслуживает прояснения.

Положительная сторона $‘positive‘D$ есть обоснование для определённости акта различения — то, что данный акт различает именно это, а не иное. Если положительное основание имеет место, то противоположная сторона не имеет основания одновременно иметь место — иначе акт перестал бы быть актом различения. Утверждение $‘positive‘D\to \neg ‘negative‘D$ есть, таким образом, выражение того, что наличие основания для одной стороны закрывает основание для противоположной. Самообоснование есть структурное проявление ЗДО на уровне записи: каждое поле Distinction обосновывается не извне, а через связь с другими полями.

Связь с полем exclusive. Формально утверждение $‘positive‘D\to \neg ‘negative‘D$ выводится из поля exclusive, имеющего тип $\neg (‘positive‘D\wedge ‘negative‘D)$. Это — эквивалентные формы: «не оба одновременно» равносильно «если одно, то не другое». Содержательно же эти формы выражают разные аспекты одной структуры: exclusive — симметричное утверждение о несовместности; L4_self_grounding — направленное утверждение о том, что наличие одной стороны исключает другую. ЗДО работает в обеих формах, но в самообосновании оно проявляется как асимметричное следование, что соответствует онтологическому характеру обоснования.

Четыре формы теоремы

Файл LawsFromDistinction.v представляет $L4$ в четырёх формах. Первые две — симметричные применения самообоснования к двум сторонам произвольного $D$; две последние — классические следствия для произвольной пропозиции.

Прямая форма: Law_of_SufficientReason. Самообоснование от положительного к отрицанию отрицательного:

Theorem Law_of_SufficientReason : forall D : Distinction,
  positive D -> ~ negative D.
Proof. exact L4_self_grounding. Qed.

Доказательство — одна строка: exact L4_self_grounding, где L4_self_grounding — вспомогательная лемма,³ выражающая самообоснование как утверждение о произвольной Distinction. Лемма опирается на поле exclusive (через эквивалентное преобразование).

Контрапозитивная форма: L4_contra. Самообоснование в обратном направлении:

Theorem L4_contra : forall D : Distinction,
  negative D -> ~ positive D.
Proof. exact L4_contrapositive. Qed.

Если имеет место отрицательная сторона, то положительная не имеет места. Это — симметричное к Law_of_SufficientReason утверждение, опирающееся на ту же структурную связь полей записи.

Каноническая форма: L4_canonical. Самообоснование для произвольной пропозиции (без обращения к Distinction):

Theorem L4_canonical : forall P : Prop, P -> ~~P.
Proof. intros P Hp Hnp. exact (Hnp Hp). Qed.

Утверждение: если $P$ имеет место, то отрицание $P$ не имеет места — эквивалентно «$P$ имеет место $\Rightarrow$ нельзя одновременно утверждать $\neg P$». Это — стандартное правило интуиционистской логики, доказуемое конструктивно, без обращения к classic. Как и в случае L2_canonical, форма зовётся канонической по предмету, а не по синтаксису: теорема работает с произвольной пропозицией $P$ напрямую, не содержит distinction_of, но относится к канонической паре $P/\neg P$, лежащей в основе distinction_of $(P)$.

Двойное отрицание: L4_double_negation. Здесь форма закона требует обратной импликации:

Theorem L4_double_negation : forall P : Prop, ~~P -> P.
Proof. intros P Hnnp. destruct (classic P) as [Hp | Hnp].
  - exact Hp.
  - exfalso. exact (Hnnp Hnp). Qed.

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

Связь L4_canonical и L4_double_negation. Эти две теоремы выражают противоположные направления в одной паре утверждений: $P\to \neg \neg P$ (доказуемо конструктивно) и $\neg \neg P\to P$ (требует classic). Прямое направление выражает, что наличие основания для $P$ исключает основание для $\neg P$; обратное направление — что отсутствие основания для $\neg P$ само есть основание для $P$. Первое — структурное следствие исключительности; второе — проявление полноты разделения (то же, что $L3$). Поэтому второе направление требует той же аксиомы.

Это стоит подчеркнуть особо. Несмотря на имя L4_double_negation и расположение в блоке $L4$, формальная зависимость этой теоремы — $L3$: устранение двойного отрицания доказывается через destruct (classic P) и потому опирается на классическую аксиому. Поэтому L4_double_negation вернее понимать не как чистое следствие самообоснования $L4$, а как место встречи $L4$ и $L3$: форма принадлежит блоку $L4$, а формальный носитель — $L3$.

Аксиома L4_witness

В репозитории ToS-Coq есть вторая фундаментальная аксиома (помимо classic), связанная с $L4$ — аксиома L4_witness. Её роль — обеспечить не произвольный выбор, а свидетельствование индивидуального существования: переход от утверждения exists x, P x к определённому свидетелю {x | P x}. Это — формальный след тезиса о детерминированности существования, и его не следует смешивать с Аксиомой Выбора: Аксиома Выбора строит выбирающую функцию для произвольного семейства множеств, тогда как L4_witness извлекает свидетеля из одного факта существования. В контексте механизма передачи статуса E/R/R это центральное техническое средство.

Здесь мы лишь упоминаем существование этой аксиомы. Её подробное обсуждение — в последующей главе об аксиоматическом слое ToS, где разбираются обе фундаментальные аксиомы (classic и L4_witness) и их соотношение с принципом $P4$ (отказ от Аксиомы Выбора) и механизмом передачи статуса в E/R/R.

Содержательный смысл

В соответствии с зафиксированной позицией — математика как язык описания логической структуры реальности — теоремы $L4$ описывают конкретный аспект работы Логики в реальном существующем.

В реальности всякое определённое положение дел имеет основание быть таким, каково оно есть. Молекула обладает осью симметрии $C_3$ не произвольно, а в силу конкретной геометрии расположения атомов и связей. Целое число чётно не «случайно», а в силу его конкретной конструкции как кратного двум. Утверждение «функция $f$ непрерывна в точке $x_0$» истинно не на пустом месте, а в силу того, что для всякой $\epsilon >0$ существует соответствующая $\delta$.

При этом наличие основания для одной определённости закрывает основание для её противоположности в одном отношении. Если молекула имеет ось $C_3$, то в том же геометрическом отношении она не имеет «отсутствия оси $C_3$». Если число чётно, то в том же арифметическом отношении оно не нечётно. Самообоснование акта различения формально выражает эту структурную связь.

Особый онтологический статус $L4$ как мета-закона проявляется в том, что во всех приведённых примерах основание того, что конкретная определённость имеет место, лежит не «рядом» с фактом, а под ним — в более фундаментальной структуре реального. Молекула обладает $C_3$ благодаря конкретной структуре связей; число чётно благодаря конкретной конструкции; утверждение истинно благодаря конкретной структуре функции. Эта подложенность оснований — проявление мета-роли $L4$ как самого действия Логики, в котором обоснованность становится возможной.

Теоремы $L4$ в Rocq не создают этой структуры реальности. Они дают её формальное выражение в простейшей форме: самообоснование Distinction как факт того, что наличие одной стороны исключает другую. Полное развёртывание ЗДО как организационного принципа всей формальной системы — через типы, доказательства, конструкции — работает на более широком уровне, не сводимом к одной теореме.

С $L1$, $L2$, $L3$, $L4$ установлены четыре закона, относящиеся к структуре одного акта различения. Последний — $L5$ — касается иерархии актов различения и работает на другом уровне, требующем отдельной формальной структуры. К нему мы переходим в следующем разделе.

Закон Порядка ($L5$)

Уровень работы $L5$: иерархия актов

Закон Порядка отличается от $L1$, $L2$, $L3$, $L4$ уровнем своего действия. Первые четыре закона касаются структуры одного акта различения — тождества сторон, исключительности, исчерпанности, обоснованности. $L5$ делает возможной саму структуру отношений между актами различения — их последовательность, иерархию, упорядочение.

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

Это положение раскрыто в отдельной работе автора по методологии E/R/R⁴, где $L5$ показан как условие самой возможности любой определённой системы. Горизонтально $L5$ проявляется в любой последовательности элементов на одном уровне — в их упорядоченности относительно друг друга. Вертикально — в иерархии уровней: элементы системы уровня $n+1$ суть сами системы уровня $n$. В настоящей главе мы касаемся лишь формальной стороны $L5$: теорем, доказанных в LawsFromDistinction.v. Полное методологическое развёртывание $L5$ через E/R/R — предмет Главы 4 настоящего тома.

Формальный аппарат: тип Level

Поскольку $L5$ производит саму иерархию — делает её возможной как структуру, — его формализация требует отдельной структуры — такой, в которой можно говорить об уровнях и отношениях между ними. В ToS-Coq эта структура — тип Level, определённый в файле TheoryOfSystems_Core_ERR.v.

Level вводится как индуктивный тип, представляющий уровни иерархии. В текущей формализации TheoryOfSystems_Core_ERR.v $L_1$ — не атомарный уровень в смысле «уровня атомов», а фундаментальный уровень Логики и основания; следующий уровень $L_2$ строится над ним, $L_3$ — над $L_2$, и так далее. На Level определён оператор строгого порядка $\ll$ (формально level_lt, сокращённо <<); запись $l_1\ll l_2$ читается как: $l_1$ более фундаментален, ближе к основанию, чем $l_2$. Также определена функция level_depth : Level -> nat, дающая глубину каждого уровня.

Здесь мы не разворачиваем определения Level и $\ll$ в полноте — они принадлежат последующей главе о структуре уровней, где обсуждается формальный аппарат $L5$ как самостоятельной структуры, его роль в работе E/R/R, и связь с принципами $P1$ (Level Separation) и $P2$ (Hierarchy). В настоящем разделе сосредоточимся на теоремах, формулирующих свойства этой структуры как формализацию $L5$.

Теоремы $L5$

Файл LawsFromDistinction.v представляет $L5$ через пять теорем о свойствах типа Level.

Иррефлексивность: L5_hierarchy. Никакой уровень не предшествует самому себе:

Theorem L5_hierarchy : forall l : Level, ~ (l << l).
Proof. exact level_lt_irrefl. Qed.

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

Транзитивность: L5_transitivity. Порядок транзитивен:

Theorem L5_transitivity : forall l1 l2 l3 : Level,
  l1 << l2 -> l2 << l3 -> l1 << l3.
Proof. exact level_lt_trans. Qed.

Если $l_1$ предшествует $l_2$, а $l_2$ предшествует $l_3$, то $l_1$ предшествует $l_3$. Это — стандартное свойство строгого порядка, обеспечивающее, что иерархия согласована: цепочка отношений ведёт от любого нижнего уровня к любому верхнему через промежуточные.

Конкретное отношение: L5_concrete. Конкретное проявление порядка:

Theorem L5_concrete : L1 << L2.
Proof. exact L1_lt_L2. Qed.

Атомарный уровень $L_1$ предшествует уровню $L_2$. Это — не общее утверждение о произвольных уровнях, а конкретное — фиксирующее конкретное отношение в иерархии. Аналогично доказывается $L_2\ll L_3$ и далее.

Цепочка: L5_chain. Объединение конкретных отношений в цепочку:

Theorem L5_chain : L1 << L2 /\ L2 << L3.
Proof. split.
  - exact L1_lt_L2.
  - exact L2_lt_L3. Qed.

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

Отсутствие бесконечного нисхождения: L5_no_infinite_descent. У каждого уровня есть конечная глубина:

Theorem L5_no_infinite_descent : forall l : Level,
  exists n : nat, level_depth l = n.
Proof. intro l. exists (level_depth l). reflexivity. Qed.

Для всякого уровня $l$ существует натуральное число $n$, выражающее его глубину. Название L5_no_infinite_descent следует понимать как интерпретацию, а не как буквальное содержание теоремы. Формально теорема доказывает более слабое утверждение: каждому уровню сопоставляется конечная натуральная глубина, и это тривиально следует из определения level_depth. Она не формулирует и не доказывает отсутствие бесконечной убывающей цепи как утверждение об отношении на последовательностях уровней — то есть не утверждает $\neg \exists f:\mathbb{N}\to ‘Level‘,\forall n,f(n+1)\ll f(n)$. Содержательная интерпретация всё же правомерна: поскольку Level задан индуктивно и каждый уровень имеет конечную глубину, сама конструкция типа указывает на отсутствие неоснованного нисхождения — иерархия обоснована снизу, и спуск по уровням рано или поздно достигает фундаментального уровня $L_1$. Но важно различать: это интерпретация, опирающаяся на индуктивное устройство Level, тогда как сама теорема L5_no_infinite_descent фиксирует лишь конечность глубины. Свойство согласуется с принципом $P4$ (конструктивность, завершённость процессов), который будет подробно разобран в последующей главе об аксиоматическом слое.

Что показывают теоремы $L5$

В отличие от $L1$–$L4$, теоремы $L5$ не привязаны к одной записи Distinction. Они работают с самостоятельной структурой — типом Level и оператором $\ll$. Это — структурное проявление того, что $L5$ производит саму возможность иерархии актов, а не на структуре одного акта.

При этом связь с Distinction сохраняется на онтологическом уровне: каждый акт различения совершается на определённом уровне, и переход от одного акта к другому (например, от различения типов чисел к различению типов функций над ними) есть переход между уровнями. Запись Distinction формализует структуру одного акта; тип Level формализует структуру отношений между уровнями, на которых совершаются акты.

Пять теорем $L5$ — иррефлексивность, транзитивность, конкретные отношения, цепочка, отсутствие бесконечного нисхождения — характеризуют порядок $\ll$ как строгий, транзитивный, конкретно реализуемый, и обоснованный снизу. Это — минимальные структурные условия, при которых иерархия может работать как основа для формальной деривации более сложных структур, что и происходит в последующих частях настоящего тома.

Содержательный смысл

В соответствии с зафиксированной позицией — математика как язык описания логической структуры реальности — теоремы $L5$ описывают конкретный аспект работы Логики в реальном существующем.

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

Иррефлексивность порядка ($l/\ll l$) выражает, что уровень не может предшествовать себе — молекула не предшествует молекуле, число не предшествует самому себе, шаг рассуждения не предшествует самому себе. Транзитивность ($l_1\ll l_2\wedge l_2\ll l_3\to l_1\ll l_3$) выражает, что иерархические отношения согласованы: если элементарные частицы предшествуют атомам, а атомы предшествуют молекулам, то частицы предшествуют молекулам. Отсутствие бесконечного нисхождения выражает, что у иерархии есть основание — какой-то базовый уровень, ниже которого ничего нет.

Теоремы $L5$ в Rocq не создают этих структурных фактов реальности. Они дают им формальное выражение через тип Level и оператор $\ll$. Полное раскрытие $L5$ как структурного условия всей работы с иерархическими системами — в последующих главах: в главе о структуре уровней (формальный аппарат) и в главе о методологии E/R/R (в которой $L5$ соответствует категории Rules — правилам, упорядочивающим работу системы).

С $L1$, $L2$, $L3$, $L4$, $L5$ установлены все пять законов логики в их формальном представлении в Rocq. В файле LawsFromDistinction.v есть и теоремы, объединяющие эти законы в единую структуру — к ним мы переходим в следующем разделе.

Объединяющие теоремы

Пять предыдущих разделов представили формальные деривации каждого из законов $L1$, $L2$, $L3$, $L4$, $L5$ по отдельности. Файл LawsFromDistinction.v содержит также теоремы, объединяющие эти законы в единую структуру. Эти объединяющие теоремы — не сумма уже сказанного, а самостоятельные формальные утверждения, показывающие, что законы работают совместно в одной и той же записи Distinction, в одной и той же иерархии Level, согласованно друг с другом.

Пять законов одновременно: five_laws_from_distinction

Центральная объединяющая теорема в LawsFromDistinction.v формулирует все пять законов как совместное свойство произвольной Distinction в контексте уровней Level:

Theorem five_laws_from_distinction : forall D : Distinction,
  (* L1: stability  *) (positive D = positive D
                        /\ negative D = negative D) /\
  (* L2: exclusivity *) (~ (positive D /\ negative D)) /\
  (* L3: totality   *) (positive D \/ negative D) /\
  (* L4: self-grounding *) (positive D -> ~ negative D) /\
  (* L5: hierarchy  *) (forall l : Level, ~ (l << l)).

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

Объединяющая теорема даёт каждый из пяти законов в его полной форме. Закон $L1$ представлен тождеством обеих сторон — и положительной, positive D = positive D, и отрицательной, negative D = negative D. Закон $L5$ представлен общим утверждением об иррефлексивности для всякого уровня, $\forall l,\neg (l\ll l)$, а не только для базового. Таким образом, теорема не урезает ни одного из законов ради краткости: каждый из пяти конъюнктов есть закон в той же силе, в какой он разобран отдельно в «Закон Тождества ()»–«Закон Порядка ()».

Доказательство теоремы — конъюнкция доказательств каждого из законов по отдельности, разобранных в «Закон Тождества ()»– «Закон Порядка ()». Содержательно теорема показывает, что пять законов не конкурируют и не противоречат друг другу: они суть пять аспектов одной структурной целостности, каждый из которых работает в полную силу, не отменяя других.

Существование непротиворечивой Distinction: laws_consistent

Следующая теорема LawsFromDistinction.v даёт экзистенциальный результат:

Theorem laws_consistent : exists D : Distinction,
  positive D /\ ~ negative D.

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

Существование такого экземпляра — нетривиальный формальный результат. Само по себе определение Distinction как записи с четырьмя полями не гарантирует, что какой-либо экземпляр вообще можно построить с содержательно ненулевыми полями. Теорема laws_consistent показывает, что построение возможно — универсальная конструкция distinction_of $(P)$, разобранная в (см. соответствующую главу) Главы 2, даёт нужный экземпляр для любой доказуемой пропозиции $P$.

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

Парные объединения: L1_L2_combined и L3_L4_combined

Помимо общей пятёрки и экзистенциальной теоремы, LawsFromDistinction.v содержит парные объединения, группирующие законы по два:

Theorem L1_L2_combined : forall D : Distinction,
  positive D = positive D /\ ~ (positive D /\ negative D).
 
Theorem L3_L4_combined : forall D : Distinction,
  (positive D \/ negative D) /\ (positive D -> ~ negative D).

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

Вторая теорема (L3_L4_combined) объединяет совместную исчерпанность и самообоснование. Содержательно — структурная характеристика полноты разделения с обоснованием: либо положительное, либо отрицательное, и если положительное, то не отрицательное.

Зачем парные объединения. Парные объединения — не случайные комбинации. Они выделяют два смысловых блока внутри структуры одного акта различения:

• Блок $L1+L2$ — определённость и несовместность. Сторона есть собой, и она не есть собой и не-собой одновременно. Это — структурное минимальное условие любой определённости вообще, доказуемое полностью конструктивно, без обращения к classic.
• Блок $L3+L4$ — полнота и обоснованность. Между сторонами нет третьего, и наличие одной стороны обосновывает отсутствие другой. Это — структурное условие полноты разделения, в котором появляется зависимость от аксиомы classic (через exhaustive).

Парные объединения, таким образом, не дублируют общую пятёрку, а структурируют её на два уровня: первичные конструктивные условия ($L1,L2$) и условия, требующие классической аксиомы ($L3,L4$ в полной форме). $L5$ работает на отдельном уровне иерархии и в эти парные объединения не входит.

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

Двадцать две теоремы файла LawsFromDistinction.v — три формы для $L1$, три для $L2$, две для $L3$, четыре для $L4$, пять для $L5$, плюс четыре объединяющих — показывают совместно следующее.

Пять законов работают в одной структуре. Запись Distinction с четырьмя полями и тип Level с оператором порядка — это одна формальная структура, в которой все пять законов получают свои формальные представления. Это означает: законы не «прибавляются» один к другому из разных источников; они читаются из одной и той же структуры под разными углами зрения.

Минимальность подтверждена. Каждый закон опирается на конкретное место структуры:

• $L1$ — на поля positive и negative (через рефлексивность их типов Prop);
• $L2$ — на поле exclusive;
• $L3$ — на поле exhaustive (и на аксиому classic в общей форме);
• $L4$ — на лемму самообоснования, выводимую из поля exclusive;
• $L5$ — на тип Level и оператор $\ll$.

Это — структурное подтверждение минимальности записи, разобранной в (см. соответствующую главу) Главы 2 — но минимальность эту нужно понимать точно. Речь идёт о минимальности выбранного структурного интерфейса, а не об абсолютной метатеореме о невозможности любых иных кодировок. Можно представить себе и другую формализацию — например, такую, где отрицательная сторона определяется как $\neg P$, и тогда часть полей не хранилась бы, а вычислялась. Утверждение главы скромнее и точнее: если мы хотим явно хранить положительную сторону, отрицательную сторону, их исключительность, их исчерпанность и уровень иерархии, то каждое из этих мест несёт отдельную, не сводимую к другим формальную работу — четыре поля Distinction плюс тип Level. Это утверждение о минимальности данной онтологически прозрачной записи, а не о невозможности иных формализаций.

Согласованность через laws_consistent. Здесь важна точность. Теорема laws_consistent не является метатеоретическим доказательством непротиворечивости всей формальной системы Rocq или всей формализации ToS — внутренняя теорема Rocq такого доказательства дать не может. Она показывает более скромный, но важный факт: запись Distinction населена конкретным экземпляром, в котором положительная сторона имеет место, а отрицательная — нет. Это локальная реализуемость записи, sanity check: структура не пуста и допускает содержательный пример. Из этого видно, что пять законов, представленных в записи Distinction, не запрещают существования объекта, удовлетворяющего им совместно, — но утверждать на основании одной этой теоремы непротиворечивость всей системы было бы преувеличением.

Связь с зафиксированной онтологией. В соответствии с позицией, зафиксированной в Методологическом введении и проговорённой в «От структуры к теоремам: постановка задачи» настоящей главы, формальные теоремы $L1$–$L5$ не создают и не обосновывают законы логики. Эти законы онтологически первичны; их работа в реальности не зависит ни от какой формальной системы. Совокупность теорем LawsFromDistinction.v показывает иное — что простейший формализуемый объект (запись Distinction) уже несёт в себе все пять законов как свои структурные свойства, доступные для машинной проверки. Это — формальное свидетельство того, насколько глубоко работа Логики встроена в саму возможность определённого существования: даже минимальная формальная запись акта различения недостаточна, чтобы скрыть какой-либо из пяти законов, — все они проявляются в ней неустранимо.

---

---

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

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

Навигация: ← Глава 2. Акт различия: запись Distinction · Глава 4. E/R/R: онтология системы →

Footnotes

1. Лемма L2_exclusivity определена в файле Distinction.v. ↩

2. Лемма L3_totality определена в файле Distinction.v. ↩

3. Лемма L4_self_grounding определена в файле Distinction.v. ↩

4. Horsocrates, The E/R/R Framework: Structure, Resolution, and the Diagnosis of Paradoxes, April 2026. ↩

5. Доказательство опирается на лемму level_lt_irrefl из файла TheoryOfSystems_Core_ERR.v. ↩

6. Применение $L5$ к структуре самого рассуждения — через шесть областей рассуждения $D_1$–$D_6$ (Recognition, Clarification, Framework Selection, Comparison, Inference, Reflection) — предмет отдельной работы автора: Horsocrates, Архитектура Рассуждения (готовится к публикации). В настоящем томе мы лишь указываем на этот факт как ещё одно проявление общего структурного условия $L5$. ↩