Глава 4. E/R/R: онтология системы

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

Совокупность теорем файла LawsFromDistinction.v, разобранная в Главе 3, показала: одна структура — запись Distinction вместе с типом Level — уже несёт в себе все пять законов логики $L1,L2,L3,L4,L5$ как свои структурные свойства. При этом сами законы остаются онтологически первичными: они не выводятся из акта различения как из источника, а лишь прослеживаются в нём как теоремы — что есть методологический шаг в формальной системе, не онтологическое утверждение об их происхождении.

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

Ответ, разворачиваемый в настоящей главе, состоит в следующем. Из деривационной цепи, начатой в Главе 2 и продолженной в Главе 3, есть ещё один шаг, не сделанный до сих пор. После законов $L1$–$L5$ следует промежуточное звено — четыре принципа, выводимые из законов как их структурные следствия. А после принципов следует завершающее звено — структура E/R/R (Elements / Roles / Rules), реализующая необходимые условия системности. Архитектурно полная цепь книги имеет вид:

$$A=\exists \to \text{Distinction}\to L1\text{–}L5\to P1\text{–}P4\to E/R/R.$$

Здесь, однако, нужна точность относительно того, что именно формализовано. Звенья $\text{Distinction}\to L1$–$L5$ и $L1$–$L5\to P1$–$P4$ суть формальные теоремы Rocq (файлы LawsFromDistinction.v и PrinciplesFromLaws.v). Завершающее же звено разобрано в файле ERRFromDistinction.v, и этот файл фиксирует более узкое ядро цепи, чем полная архитектурная схема: он выводит E/R/R-структуру прямо из записи Distinction и законов, не проводя отдельной формальной теоремы вида <<из $P1$–$P4$ следует E/R/R>>. Полный мост через $P1$–$P4$ есть концептуальная интерпретация архитектуры — он содержательно верен и может быть впоследствии усилен отдельной теоремой, но сейчас как единая формальная зависимость в репозитории не записан. Эту разницу между архитектурной схемой книги и фактическим содержанием файла мы будем держать в виду на протяжении всей главы.

Начнём с завершения деривационной цепи.

Четыре принципа

От законов к принципам

Законы $L1$–$L5$, выведенные в Главе 3, суть условия определённости в их самом общем виде. Чтобы из этих условий получилась структура системы, нужен ещё один промежуточный шаг — выявление принципов, в которых законы работают вместе.

Таких принципов четыре: $P1$ (иерархия), $P2$ (предшествование критерия), $P3$ (интенсиональное тождество), $P4$ (конечная актуальность). Каждый получается из совместной работы конкретных законов:¹

Принцип	Содержание	Источник
$P1$	Иерархия ($S\notin S$)	$L1+L5$
$P2$	Предшествование критерия	$L5$
$P3$	Интенсиональное тождество	$L1+L4$
$P4$	Конечная актуальность	$L5$

Каждый принцип фиксирует структурное следствие из законов, которое уже работает в записи Distinction, но проявляется явно только когда речь идёт об устройстве систем. Рассмотрим каждый.

$P1$: иерархия

Структурное содержание. В любой системе $S$, организующей элементы под некоторым критерием, организатор располагается на уровне выше организуемого. По $L1$, $S$-как-организатор имеет определённое тождество, не размывающееся; по $L5$, уровень организуемого ниже уровня организатора. Совместная работа $L1$ и $L5$ даёт асимметричную иерархическую структуру: $\text{Level}(\text{организатор})>\text{Level}(\text{организуемого})$.

Формальная теорема. Иерархическая асимметрия выражается в Rocq иррефлексивностью оператора порядка:

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

В $L5$-иерархии работают также конкретные структурные свойства: $L_1\ll L_2$ и $\neg (L_2\ll L_1)$ (уровень основания $L_1$ строго ниже второго); $l\ll LSl$ для любого $l$ (каждый уровень строго ниже своего преемника); асимметрия (если $l_1\ll l_2$, то $\neg (l_2\ll l_1)$).²

Следствие: $S\notin S$. Если бы система $S$ содержала себя как свой собственный элемент, она была бы одновременно организатором и организуемым — то есть располагалась бы на двух разных уровнях одновременно. Это означало бы $\text{Level}(S)<\text{Level}(S)$ — что противоречит иррефлексивности. Таким образом, ни одна система не содержит себя.

Следствие: парадокс Рассела блокирован. «Множество всех множеств, не содержащих себя» предполагает конструкцию, в которой вопрос о самопринадлежности осмыслен. По $P1$ такой вопрос не имеет определённого содержания: самопринадлежности нет ни в одной правильно построенной системе.³

$P2$: предшествование критерия

Структурное содержание. По $L5$, всякая операция располагается выше операнда: операция предполагает операнд как уже существующий. Применительно к системам: критерий, определяющий систему, есть операция над тем, чему он адресован; следовательно, он располагается на уровне выше уровня результата. Это предшествование критерия: уровень критерия $<$ уровня системы, которую он задаёт.

Формальная теорема. Принцип представлен в двух формах:

Theorem P2_from_L5 : forall L (C : Criterion L), P2_valid L C.
Proof. exact P2_always_holds. Qed.
 
Theorem P2_structural : forall L (C : Criterion L),
  crit_level_witness L C << L.
Proof. intros L C. exact (crit_level_valid L C). Qed.

Структурная встроенность. Особенность $P2$ в том, что она не следует из закона как самостоятельная теорема, а встроена в саму запись критерия. Поле crit_level_valid в записи Criterion требует доказательства предшествования уровня критерия уровню системы. Без этого доказательства критерий невозможно построить — Rocq отказывается компилировать определение.

Это параллельно тому, как $L2$ встроена в запись Distinction через поле exclusive ((см. соответствующую главу) Главы 3): закон работает не «извне», а как часть структуры, без которой сама структура невозможна.

Следствие: запрет циркулярных определений. Из $P2$ выводится формальный запрет на построение критерия, уровень которого совпадает с уровнем определяемой им системы:

Theorem P2_no_circularity : forall L,
  ~ exists C : Criterion L, crit_level_witness L C = L.

Иначе говоря: «$S$ есть то, что удовлетворяет $S$» — формулировка, заблокированная самой типовой системой Rocq, поскольку требует построить критерий, нарушающий $P2$.

Следствие: возможность пошагового определения. Положительная сторона $P2$ — обеспечение последовательности определений. Каждое новое определение в Rocq может опираться на уже-определённое и расположенное на уровне ниже. Эта последовательность — структурное условие самой возможности построения формальной системы.

$P3$: интенсиональное тождество

Структурное содержание. По $L1$, всякая система имеет определённое тождество ($S=S$); по $L4$, это тождество требует достаточного основания. Основание системы — её критерий, то, через что она есть именно она. Совместная работа $L1$ и $L4$ даёт: тождество системы определяется через её критерий, не через её элементы. Это — интенсиональное тождество.

Формальные теоремы. $P3$ представлено четырьмя утверждениями — свойствами отношения интенсионального равенства systems_intensionally_equal:

Theorem P3_reflexivity : forall L (S : System L),
  systems_intensionally_equal S S.
 
Theorem P3_symmetry : forall L (S1 S2 : System L),
  systems_intensionally_equal S1 S2 ->
  systems_intensionally_equal S2 S1.
 
Theorem P3_transitivity : forall L (S1 S2 S3 : System L),
  systems_intensionally_equal S1 S2 ->
  systems_intensionally_equal S2 S3 ->
  systems_intensionally_equal S1 S3.
 
Theorem P3_from_L1_L4 : forall L (S1 S2 : System L),
  sys_criterion L S1 = sys_criterion L S2 ->
  sys_pos_bound L S1 = sys_pos_bound L S2 ->
  sys_uniqueness L S1 = sys_uniqueness L S2 ->
  systems_intensionally_equal S1 S2.

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

Следствие: тождество через критерий, не через элементы. В традиционной теории множеств действует экстенсиональное тождество: «$A$ и $B$ имеют одни и те же элементы, значит $A=B$». В ToS работает интенсиональное тождество, которое сильнее: даже если две системы содержат одни и те же элементы, они не тождественны, если эти элементы получены под разными критериями. Рассмотрим классический пример из евклидовой геометрии: множество равносторонних треугольников (критерий — три равные стороны) и множество равноугольных треугольников (критерий — три равных угла) на плоскости содержат одни и те же фигуры. Но критерии существенно различны: один опирается на меру сторон, другой — на меру углов. По $P3$ эти две системы экстенсионально совпадают, но интенсионально не тождественны: они имеют разные основания, разные способы быть тем, чем они являются.

Следствие: онтологический приоритет критерия. Из $P3$ вытекает, что система определяется не тем, что в ней, а через что она есть. Критерий — не описание содержания, а онтологическое основание (см. (см. соответствующую главу) Главы 2). Это положение проводит существенное методологическое различие между ToS и теоретико-множественным подходом, и оно работает через всю последующую часть тома.

$P4$: конечная актуальность

Структурное содержание. По $L5$, всякий процесс имеет последовательную структуру (стадия за стадией). На каждой стадии завершено конечное число шагов; каждый шаг добавляет конечное число элементов; конечные шаги, умноженные на конечные добавления, дают конечный итог. Применительно к системам: на каждой конкретной стадии $t$ актуально присутствует конечное количество элементов: $|S_t|<\infty$.

Формальные теоремы. В Rocq принцип формализован через тип RealProcess $:=\mathbb{N}\to \mathbb{Q}$ — последовательность рациональных чисел, индексированная натуральными:

Theorem P4_from_L5 : forall (R : nat -> Q) (n : nat),
  exists q : Q, R n = q.
 
Theorem P4_no_completed_infinity :
  forall q : Q, exists (n : Z) (d : positive), q = n # d.
 
Theorem P4_finite_at_each_stage : forall (R : nat -> Q) (n : nat),
  exists (num : Z) (den : positive), R n = num # den.

На каждой стадии $n$ процесс $R$ выдаёт одно конкретное рациональное число — отношение конечных целых.

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

Философская интерпретация $P4$. На скромный формальный факт опирается более широкая интерпретация принципа $P4$: бесконечность следует понимать как неограниченный процесс, а не как завершённый объект. Бесконечное множество в традиционной теории мыслится как завершённый актуально-бесконечный объект; интерпретация $P4$ предлагает вместо него процесс, не ограниченный сверху по числу шагов, но в каждый конкретный момент имеющий конечное состояние. То, что называют бесконечным множеством, ToS склонна понимать как неограниченный процесс — саму последовательность $R$, а не её <<предел в актуальной бесконечности>>. Эту интерпретацию — и её отличие от формального содержания теорем выше — мы развернём в процессной математике Части IV.

Следствие: конструкция действительных чисел без AC и Infinity. В Части IV настоящего тома действительные числа будут конструироваться через RealProcess — последовательности рациональных приближений. Эта конструкция не использует ни Аксиомы Бесконечности (которая постулирует существование завершённого бесконечного множества), ни Аксиомы Выбора (которая позволяет извлекать элементы из бесконечного семейства непредъявимым алгоритмом). Это прямое методологическое следствие $P4$: вся конструкция держится на процессах, не на завершённых объектах.

Все четыре принципа вместе

Все четыре принципа работают совместно: для любой системы $S$ на любом уровне $L$ действуют одновременно иерархия ($P1$), предшествование критерия ($P2$), интенсиональное тождество ($P3$) и конечная актуальность ($P4$). Формально это объединяющее утверждение имеет вид:⁴

Theorem four_principles_from_five_laws :
  (forall l : Level, ~ (l << l)) /\                  (* P1 *)
  (forall L (C : Criterion L), P2_valid L C) /\     (* P2 *)
  (forall L (S : System L),
    systems_intensionally_equal S S) /\              (* P3 *)
  (forall (R : nat -> Q) n, exists q : Q, R n = q). (* P4 *)

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

С завершением деривации принципов мы получаем последний шаг перед формулировкой E/R/R. Принципы $P1$–$P4$ суть необходимые условия системности, выводимые из законов логики. Структура, реализующая эти условия в их минимальной форме, — и есть E/R/R. К её формулировке мы переходим в следующем разделе.

E/R/R как онтология системы

Завершение деривационной цепи

Деривационная цепь, начатая с первого принципа $A=\exists$ и прошедшая через запись Distinction, законы $L1$–$L5$ и четыре принципа $P1$–$P4$, имеет ровно одно завершающее звено — структуру E/R/R. Архитектурно полная цепь имеет вид:

$$A=\exists \to \text{Distinction}\to L1\text{–}L5\to P1\text{–}P4\to E/R/R.$$

Каждое звено цепи — структурное условие, выводимое из предыдущих. Каждый шаг прослеживает необходимость, по которой устроена любая система, а не порождает её. Сама онтология системы — предельный результат этого прослеживания — есть E/R/R.

Здесь, однако, необходимо точно указать, что именно фиксирует формализация. Теорема complete_foundation из файла ERRFromDistinction.v⁵ доказывает следующее: из любой пропозиции строится Distinction; для всякой Distinction выполнены законы $L2$ и $L3$; всякая Distinction даёт E/R/R-структуру не менее чем с двумя ролями; и уровневая иерархия иррефлексивна. Это — ядро завершающего звена. Чего теорема не содержит — это отдельной формальной зависимости вида <<из $P1$–$P4$ следует E/R/R>>: файл ERRFromDistinction.v не импортирует PrinciplesFromLaws.v и работает с записью Distinction напрямую. Полный мост через $P1$–$P4$ — архитектурная интерпретация цепи, содержательно верная, но как единая теорема пока не записанная. В дальнейшем изложении мы говорим о цепи в архитектурном смысле, отмечая, где формализация уже её догнала, а где ещё нет.

Три аспекта системы

Структурное содержание. Всякая система с необходимостью имеет три аспекта:

• Elements (Элементы) — то, что есть в системе, её субстрат: конкретные носители, занимающие позиции.
• Roles (Роли) — то, зачем элементы значимы, какую функцию они выполняют в системе.
• Rules (Правила) — то, как организовано взаимодействие элементов, законы, удерживающие систему как систему.

Принципиально важно:

E/R/R — не три части системы, а три аспекта одного устройства.

Их нельзя отделить друг от друга. Элемент без роли — не элемент, а нечто аморфное; роль без элемента — пустая позиция, не имеющая носителя; правила без элементов и ролей — абстрактная схема, не относящаяся ни к чему конкретному. Все три аспекта работают одновременно или система не существует. В исходной формализации этот принцип зафиксирован прямо: «These are not three parts but three aspects of one act».⁶

Эпистемический порядок vs онтологический. Аббревиатура E/R/R перечисляет аспекты в эпистемическом порядке — от внешне наблюдаемого к глубинному. При анализе незнакомой системы естественно сначала увидеть её элементы (что-то, что доступно непосредственно), затем распознать роли (увидеть, что элементы имеют значимость, что-то делают), и лишь затем выявить правила (понять, по каким законам всё это работает).

Онтологически порядок обратный. Правила первичны: они задают, что значит быть в системе. Роли вторичны: они определены правилами как позиции, которые требуется заполнить. Элементы третичны: они подбираются под роли как их носители. Этот онтологический порядок (Rules $\to$ Roles $\to$ Elements) известен как generative order — порядок, в котором структура порождает себя. Он будет подробно разобран в «Асимметрия и generative order».

При этом аббревиатура E/R/R сохраняется за общепринятым эпистемическим порядком — по практическим соображениям: именно с элементов начинается анализ. Но в каждом конкретном случае структура работает в обратном направлении: правила $\to$ роли $\to$ элементы.

Формальное представление в Distinction. На уровне простейшей системы — акта различения — три аспекта получают конкретное содержание:

• Elements: положительная и отрицательная стороны (поля positive и negative записи Distinction).
• Roles: положение «выделенного» и положение «фона, относительно которого выделено» — две позиции, занимаемые сторонами.
• Rules: исключительность и исчерпанность (поля exclusive и exhaustive), удерживающие акт как именно различение.

Это — E/R/R-структура одной конкретной системы (акта различения). В § «Применение к Distinction»– «Применение к distinction_of» это представление будет разобрано формально.

Минимальность: два элемента, две роли, два правила

Структурное содержание. В простейшей системе — акте различения — каждый аспект E/R/R представлен ровно двумя составляющими. Это число не произвольно: оно выводится из уже установленной структуры записи Distinction и не может быть изменено без разрушения самого акта различения.

Деривация двух элементов. В Главе 2 ((см. соответствующую главу)) было показано, что запись Distinction имеет ровно четыре поля — positive, negative, exclusive, exhaustive — и ни одно из этих полей не может быть удалено без потери самой природы различения. Поля positive и negative имеют тип Prop — они выражают что именно различается. Это и есть Elements в простейшем акте: два содержательных полюса, между которыми проводится различение.

Различие одного полюса от себя — не различение, а тождество. Поэтому один элемент не образует акта различения. Следовательно, число элементов в простейшем акте не может быть меньше двух — и оно ровно два, поскольку запись Distinction имеет ровно два поля типа Prop.

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

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

Деривация двух правил. Поля exclusive и exhaustive выражают, как именно стороны соотносятся друг с другом: exclusive утверждает несовместность сторон; exhaustive — их совместную исчерпанность. Это два логически независимых правила: ни одно не сводится к другому, оба обязательны.

Что было бы при удалении одного из них? В (см. соответствующую главу) Главы 2 было показано: без exclusive стороны могут совпасть, и акт различения распадается в тождество; без exhaustive между сторонами появляется «третий путь», и разделение становится неполным. Следовательно, меньше двух правил недостаточно для удержания структуры различения. А больше двух правил в простейшем акте не нужны: исключительность и исчерпанность вместе уже фиксируют все законы различения — в чём, собственно, и состоит минимальность записи Distinction, доказанная в Главе 2.

Числовая фиксация в формализации. В Rocq двойственность зафиксирована числовыми инвариантами:⁷ для всякой $D:‘Distinction‘$:

$$‘er{r}_{e}lemen{t}_{c}ount‘(D)=2,‘er{r}_{r}ol{e}_{c}ount‘(D)=2,‘er{r}_{r}ul{e}_{c}ount‘(D)=2.$$

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

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

Что есть система

Структурное определение. После завершения деривационной цепи мы можем зафиксировать центральное понятие Теории Систем.

Система — это то, что имеет E/R/R-структуру.

Иначе говоря: системой называется всякое определённое целое, в котором работают три аспекта — Elements, Roles, Rules — в их минимальной двойственной форме или в надстройках над ней.

Это — не определение через нечто более простое. Невозможно было бы дать системе «внешнее» определение, поскольку любое такое определение само опиралось бы на структуру той же системы (содержит элементы, играющие роли, по правилам). Определение системы получается в самом конце деривации, не как новый постулат, а как конечный результат прослеживания цепи $A=\exists \to E/R/R$.

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

Следствие: универсальность. Поскольку E/R/R получено как завершение деривационной цепи, начатой с самого первого принципа, все определённые сущности — от элементарных частиц до математических структур — имеют E/R/R-структуру. Они системы или потому, что есть; не иметь E/R/R-структуру означало бы не быть определённым, не существовать как нечто конкретное.

С формулировкой E/R/R мы получаем основу для всего последующего: разбор конкретных систем (§«Применение к Distinction»– «Применение к distinction_of»), их хорошей сформированности («Самоприменение E/R/R», «Парадоксы как смешение E/R/R-категорий»), и места в иерархии («Иерархия уровней», «Мета-система: Абсолют»). Прежде чем переходить к этим разбираемым случаям, рассмотрим подробнее каждый из трёх аспектов в отдельности.

Три аспекта подробно

Порядок изложения

В «Три аспекта системы» было зафиксировано различие между эпистемическим порядком — аббревиатурой E/R/R, в которой аспекты перечислены от внешне наблюдаемого (Elements) к глубинному (Rules), — и онтологическим порядком (generative order), в котором правила первичны, роли вторичны, элементы третичны.

Подробное разворачивание трёх аспектов производится в онтологическом порядке: Rules $\to$ Roles $\to$ Elements. Это — порядок, в котором система разворачивается: сначала задаются правила, под них определяются роли, и лишь затем подбираются элементы.

Rules: законы организации

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

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

Двухслойность правил. В любой конкретной системе работает два слоя правил:

• Универсальный слой — законы логики $L1$–$L5$. Они работают всегда и везде: в любой системе, на любом уровне иерархии, для любой конфигурации.
• Конкретный слой — правила, специфичные для данной системы. Они определяют роли (какие позиции есть в этой системе) и задают подбор элементов (какие носители могут занимать какие позиции).

Подробный разбор двухслойности — в «Двухслойность Rules: универсальное и конкретное».

Механизм подбора. Особо отметим: правила конкретного слоя могут содержать механизм подбора элементов под роли — автоматический алгоритм, по которому из имеющихся потенциальных носителей выбираются те, что займут соответствующие позиции. Если такой механизм есть, актуализация системы производится системно, без внешнего вмешательства. Если механизма нет, по $L4$ требуется явное действие оператора — акт подбора, обоснованный структурой системы.⁸

Примеры. В группе универсальный слой правил — $L1$–$L5$; конкретный слой — аксиомы группы (ассоциативность, существование нейтрального элемента, существование обратных). Подбор элементов под роль <<обратный к данному>> в аддитивной группе $\mathbb{Z}/n\mathbb{Z}$ производится автоматически: обратный к $a$ есть $-a\mathrm{mod}n$ (для ненулевого представителя $a$ это $n-a$, для нуля — сам нуль). В формальной грамматике — $L1$–$L5$ плюс продукции грамматики. В физической системе — $L1$–$L5$ плюс уравнения движения и законы сохранения.

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

Roles: значимость позиций

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

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

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

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

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

Elements: актуализация потенциала

Структурное содержание. Elements (Элементы) — то, что актуально есть в системе: конкретные носители, занимающие заранее заданные роли. Элементы появляются в системе как результат подбора под уже-определённые роли — это завершающий шаг разворачивания системы.

Потенциальное и актуальное существование. Из изложения выше следует, что система имеет два модуса существования:

Главный системный критерий существования — Правила и Роли (потенциал); Элементы — актуализация.

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

Пример. Рассмотрим параметризованную схему $S_c$: <<множество натуральных чисел $n$ таких, что $n^2<c$>>, где $c$ — параметр. Правила схемы определены: условие $n^2<c$ задаёт роль <<элемент множества>> через явное арифметическое требование. При $c=10$ роли заполнены элементами $\{1,2,3\}$ — если считать натуральные с единицы⁹ — система $S_{10}$ актуализована тремя носителями. При $c=2$ — единственный элемент $\{1\}$, система $S_2$ актуализована минимально. При $c=1$ ролям нет носителей: система $S_1$ остаётся в потенциальном модусе — множество пусто как актуальный набор, но есть как структурно определённая возможность с явно заданным критерием.

Здесь важно избежать неточности. Было бы неверно сказать, что $S_{10}$, $S_2$, $S_1$ — <<одна и та же система с разным наполнением>>. По принципу $P3$ (интенсиональное тождество, «: интенсиональное тождество») тождество системы задаётся её критерием; а критерий $S_c$ включает значение параметра $c$. Разные $c$ — разные критерии, а значит разные системы в интенсиональном смысле. Точная формулировка такова: существует одна параметризованная схема $S_c$, и $S_{10}$, $S_2$, $S_1$ суть различные экземпляры этой схемы — интенсионально различные, ибо различны их критерии. Что у них общее — это схема (форма критерия, тип роли); что различно — конкретный критерий и потому сама система. Различие потенциального и актуального проходит внутри каждого экземпляра $S_c$: правила и роли задают его потенциал, носители — его актуализацию.

Связь с $L1$. Каждый актуализованный элемент в системе тождественен самому себе — это работа $L1$ применительно к носителям. Без тождества элементов невозможна была бы их устойчивая идентификация в разных контекстах. $L1$ работает в Elements как условие самой возможности обращаться к актуальным носителям как к определённым.

Множественность элементов. В простейшем акте различения — два элемента (положительная и отрицательная стороны). В сложных системах элементов больше: группа имеет элементы-носители, на которых задана групповая операция; формальный язык имеет элементы-символы алфавита; натуральные числа имеют элементы $1,2,3,\dots$. Во всех случаях элементы — актуальные носители ролей, существующие в дополнение к структурному потенциалу, заданному правилами и ролями.

Совместная работа трёх аспектов

Хотя три аспекта различимы — мы можем говорить отдельно о Rules, Roles, Elements — они не разделимы в работе системы. Элементы уже играют роли (определённые правилами); роли уже заполнены элементами (выбранными по правилам); правила уже работают на конкретных элементах и ролях. Три аспекта — три неотделимых стороны одного устройства, как было зафиксировано в «Три аспекта системы».

Связь с законами. Соответствие трёх аспектов и законов логики:

Аспект	Вопрос	Закон
Rules	Как организовано?	$L5$ (Порядок)
Roles	Зачем значимо?	$L4$ (ЗДО)
Elements	Что актуально есть?	$L1$ (Тождество)

При этом $L2$ (Непротиворечие) и $L3$ (Исключённое третье) работают во всех трёх аспектах: правила непротиворечиво применимы; роли непротиворечиво распределены; элементы непротиворечивы сами в себе и взаимно исключительны. Эти два закона не привязаны к одному аспекту — они работают как структурные условия согласованности всех трёх.

Следствие: единство E/R/R-разбора. При анализе любой системы три аспекта выявляются вместе. Хотя онтологически правила первичны, эпистемически удобно начинать с элементов (которые наблюдаемы) и двигаться к ролям и правилам. Систематический E/R/R-разбор — последовательное прохождение всех трёх вопросов — даёт полное описание онтологической структуры системы независимо от порядка, в котором эти вопросы задаются.

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

Двухслойность Rules: универсальное и конкретное

В «Rules: законы организации» было кратко обозначено, что Rules в любой системе работают двухслойно: универсальный слой законов $L1$–$L5$ и конкретный слой правил данной системы. Эта двухслойность — не методологическое удобство для классификации, а структурное устройство, без которого правила не могли бы работать ни в одной системе.

Универсальный слой Rules — законы $L1$–$L5$ — работает всегда и везде; конкретный слой определяет роли в данной системе и задаёт подбор элементов под эти роли.

Универсальный слой: законы $L1$–$L5$

Структурное содержание. Универсальный слой Rules — законы логики $L1$–$L5$. Они не привязаны к конкретной системе: работают в любой системе, на любом уровне иерархии, при любой конфигурации элементов и ролей. Это — условия самой возможности системности, выводимые из деривационной цепи и зафиксированные в Главе 3 как формальные теоремы Rocq.

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

• $L1$ обеспечивает, что элементы устойчиво идентифицируемы.
• $L2$ обеспечивает, что одно и то же не может одновременно быть и не быть в системе (для одного отношения).
• $L3$ обеспечивает, что между «есть в системе» и «нет в системе» нет третьего.
• $L4$ обеспечивает, что каждое утверждение о системе требует основания — структурного, а не произвольного.
• $L5$ обеспечивает, что система имеет иерархическое устройство: правила выше ролей, роли выше элементов.

Универсальность как структурное свойство. Универсальный слой работает до и независимо от того, какая конкретная система рассматривается. Когда мы определяем группу, грамматику или физическую систему, мы не добавляем $L1$–$L5$ как часть определения — эти законы уже работают в любой попытке такого определения. Само определение возможно только при их работе.

Конкретный слой: правила данной системы

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

• Определение ролей — какие позиции есть в этой конкретной системе, какие функции они выполняют.
• Подбор элементов — какие потенциальные носители могут занимать какие позиции, и (если есть) — как этот подбор производится.

Эти два аспекта неразделимы: правила, определяющие роли, неявно задают и тип объектов, которые могут эти роли играть. Например, правило «чётное натуральное число — такое $n$, что $n=2k$ для некоторого $k\in \mathbb{N}$» одновременно определяет роль «быть чётным числом» и указывает, какие элементы могут её играть (только те, что представимы в указанном виде — то есть $2,4,6,8,\dots$).

Формализация в Rocq. В репозитории ToS-Coq двухслойность зафиксирована через структуру типа System, в которой соединены универсальные требования и конкретные правила системы.¹⁰ Тип System L параметризован уровнем $L$ (универсальный слой работает через иерархию уровней) и содержит поле sys_criterion (конкретный критерий, специфичный для данной системы). Универсальный слой проявляется как требования к sys_criterion (его уровень должен быть строго ниже уровня системы, по $P1$); конкретный слой — как само содержание критерия.

Следствие: каждая система имеет свой профиль конкретного слоя. Группа, грамматика, физическая система — каждая имеет собственный набор конкретных правил. Универсальный слой одинаков для всех ($L1$–$L5$ работают одинаково); конкретные слои различны. Именно конкретный слой делает систему той самой системой, а не другой.

Подбор элементов: автоматический и операторный

Два типа подбора. В «Rules: законы организации» было введено различие двух типов подбора элементов под роли. Развернём его подробнее.

Автоматический подбор. Конкретный слой правил содержит алгоритмический механизм: для любой роли в системе указано, как выбрать элемент, который её займёт. В этом случае актуализация системы происходит без внешнего вмешательства — достаточно применить алгоритм. Пример: в аддитивной группе $\mathbb{Z}/n\mathbb{Z}$ роль <<обратный к $a$>> автоматически заполняется элементом $-a\mathrm{mod}n$ — механизм задан формулой.

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

Связь с потенциалом и актуализацией. Различие двух типов подбора имеет прямое следствие для модусов существования системы («Elements: актуализация потенциала»):

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

Совместная работа двух слоёв

Иерархическая структура. Универсальный и конкретный слои правил не «параллельны», а иерархичны. Универсальный слой работает над конкретным: законы $L1$–$L5$ суть условия, при которых конкретные правила вообще могут быть сформулированы и применены. Конкретные правила не могут противоречить универсальным — они работают в пределах того, что универсальные допускают.

Примеры двухслойности. Аддитивная группа $\mathbb{Z}/n\mathbb{Z}$. Универсальный слой: $L1$–$L5$. Конкретный слой: ассоциативность сложения по модулю $n$, существование нейтрального элемента ($0\mathrm{mod}n$), существование обратного для каждого элемента (обратный к $a$ есть $-a\mathrm{mod}n$). Подбор: автоматический (формулы явные). Заметим: всё сказанное относится к аддитивной структуре; в мультипликативной группе единиц $(\mathbb{Z}/n\mathbb{Z}{)}^{\times }$ нейтральный элемент — $1$, и обратный существует лишь для обратимых классов, а не для всякого элемента $\mathbb{Z}/n\mathbb{Z}$.

Формальная грамматика. Универсальный слой: $L1$–$L5$. Конкретный слой: алфавит терминалов, алфавит нетерминалов, стартовый символ, продукции. Подбор: автоматический (для каждой строки можно алгоритмически проверить, выводится ли она).

Множество чётных натуральных чисел. Универсальный слой: $L1$–$L5$. Конкретный слой: правило «$n$ чётно тогда и только тогда, когда $n=2k$ для некоторого $k\in \mathbb{N}$». Подбор: автоматический (для каждого натурального числа явный тест на чётность).

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

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

{ С двухслойностью Rules мы завершаем разбор онтологического устройства правил. Следующий раздел разворачивает асимметрию отношений между тремя аспектами E/R/R — generative order, которым правила задают роли, а роли — элементы. }

Асимметрия и generative order

В «Три аспекта системы» и «Порядок изложения» было различено два порядка: эпистемический (Elements $\to$ Roles $\to$ Rules) и онтологический (Rules $\to$ Roles $\to$ Elements). Настоящий раздел разворачивает онтологический порядок — generative order — как структурную асимметрию отношений между тремя аспектами E/R/R.

Generative order: Rules задают Roles; Roles ограничивают Elements. Обратной асимметрии нет: ни Elements не определяют Roles, ни Roles не задают Rules.

Три асимметричных отношения

Структурное содержание. Между тремя аспектами E/R/R работают три отношения, и каждое из них асимметрично: одна сторона определяет другую, но не наоборот.

Rules $\to$ Roles: правила задают роли. Правила системы определяют, какие позиции в ней есть. Из правил вытекает, какие роли требуются: правило «нейтральный элемент существует» задаёт роль «нейтральный элемент»; правило «существует обратный для каждого» задаёт роль «обратный к данному». Без правил роли были бы произвольны; с правилами они получают конкретное содержание.

Обратное неверно. Роли не задают правила. Можно представить себе «нейтральный элемент» вне контекста группы — но это уже не будет ролью в смысле ToS, поскольку нет правил, обосновывающих эту роль. Роли существуют только под правилами; обратное направление не работает.

Roles $\to$ Elements: роли ограничивают элементы. Роли, определённые правилами, ограничивают круг элементов, которые могут их играть. Не любой объект может занять любую позицию — только те, что удовлетворяют условиям роли. Правило «нейтральный элемент» вместе с ролью допускает только конкретный элемент в качестве носителя; в группе ${\mathbb{Z}}_n$ это число $1$ при умножении или $n$ при сложении (при индексации от единицы).

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

Третье отношение: Rules $\to$ Elements (через Roles). Прямое отношение от правил к элементам опосредовано ролями: правила сами по себе не определяют конкретных элементов, они определяют роли, которые затем заполняются элементами. Это — транзитивный аспект generative order: правила определяют роли, роли определяют элементы, поэтому правила (через роли) определяют элементы.

Generative order: онтологический порядок системы

Структурное содержание. Три асимметричных отношения вместе дают единый порядок развёртывания системы:

$$\text{Rules}\to \text{Roles}\to \text{Elements}.$$

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

Почему именно этот порядок. Generative order не произволен — он следует из работы законов логики на разных уровнях:

• $L5$ (закон порядка) задаёт иерархию: правила располагаются на уровне выше ролей, роли — на уровне выше элементов.
• $L4$ (закон достаточного основания) требует, чтобы каждая роль была обоснована — основанием служат правила; соответственно, роли могут быть определены только после правил.
• $L1$ (закон тождества) обеспечивает устойчивость элементов как носителей ролей — но эта устойчивость возможна только тогда, когда уже определены роли, для которых элементы являются носителями.

Generative order — структурное следствие работы $L1$, $L4$, $L5$ применительно к аспектам системы.

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

Связь с потенциалом и актуализацией

Структурное содержание. Generative order и различие потенциального/актуального модусов системы («Elements: актуализация потенциала») — две стороны одной структурной картины:

• Потенциал системы — то, что задано правилами и ролями. Это первые два звена generative order: Rules $\to$ Roles.
• Актуализация системы — подбор элементов под уже определённые роли. Это завершающее звено: Roles $\to$ Elements.

Generative order как развёртывание потенциала в актуальное. Когда мы говорим, что система разворачивается в порядке Rules $\to$ Roles $\to$ Elements, мы имеем в виду не временной процесс, а структурное отношение: потенциал предшествует актуализации, и актуализация следует из потенциала, а не наоборот. Конкретные элементы могут быть подобраны (или не быть — если ролям нет носителей), но самой возможности подбора нет без заранее заданных правил и ролей.

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

Эпистемический порядок как обратный

Структурное содержание. Generative order — порядок, в котором система есть (онтологически разворачивается). Эпистемический порядок — порядок, в котором система познаётся (распознаётся нами при анализе). Эти два порядка обратны друг другу:

Generative order (онтологически)	Эпистемический порядок
Rules задают Roles	Elements распознаются
Roles ограничивают Elements	Roles выявляются по Elements
Elements актуализуют систему	Rules выводятся по Roles

{

Почему два порядка обратны. Развёртывание системы идёт сверху вниз (Rules $\to$ Elements), потому что правила первичны. Распознавание системы идёт снизу вверх (Elements $\to$ Rules), потому что наблюдатель сначала видит элементы — они доступны непосредственно в опыте. Тот же феномен в естественных науках: устройство атома в реальности разворачивается из законов физики, но познаётся начиная с наблюдаемых явлений (спектров, рассеяния). }

Следствие: согласованность аббревиатуры E/R/R. Аббревиатура E/R/R — эпистемическая (Elements первыми, Rules последними), что согласуется с практикой анализа: при разборе незнакомой системы естественно начинать с элементов. Это практическое соглашение, а не онтологическое утверждение. Каждый раз, проводя E/R/R-разбор, мы движемся по эпистемическому порядку — но обнаруживаем систему, развёрнутую в generative order.

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

Иерархия уровней

В предыдущих разделах было показано, что E/R/R — три аспекта любой системы. В «Асимметрия и generative order» разворачивание системы было прослежено по generative order. Настоящий раздел разворачивает вертикальную структуру — иерархию уровней, в которой располагаются системы разной сложности.

Элементы системы уровня $n+1$ суть сами системы уровня $n$.

Принцип иерархии

Структурное содержание. Системы разной сложности не располагаются <<рядом друг с другом>> как равные — они образуют иерархию, в которой более сложная система имеет в качестве своих элементов системы, расположенные на более фундаментальных уровнях. Часто удобно рассматривать ближайший случай — когда элементы системы уровня $n+1$ суть системы уровня $n$, — и ниже мы будем им пользоваться как наглядным; но формальная идея шире: требуется лишь, чтобы элементы располагались ниже по уровню, не обязательно ровно на один шаг. Это — закон вертикальной структуры E/R/R.

Деривация из $L5$ и $P1$. Иерархия — не дополнительный постулат, а следствие уже-выведенного:

• По $L5$ (закон порядка), всякая операция располагается выше операнда: правила системы — над её элементами и ролями.
• По $P1$ (иерархия, «: иерархия»), уровень организуемого строго ниже уровня организатора: $\text{Level}(\text{организуемое})<\text{Level}(\text{организатор})$.

Применяя эти два принципа: элементы данной системы ($\text{Level}=n$) сами организованы — то есть имеют свою E/R/R-структуру. Значит, они и сами суть системы. Их собственный уровень строго ниже уровня организатора — они располагаются под ним в порядке $\ll$. В ближайшем, наглядном случае это уровень $n-1$; но формально требуется лишь отношение <<ниже по уровню>>, а не ровно один шаг вниз. Иерархия уровней — структурное следствие совместной работы $L5$ и $P1$.

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

Связь с типом Level

Формализация в Rocq. В Главе 3 ((см. соответствующую главу)) был кратко введён тип Level с оператором строгого порядка $\ll$ и функцией глубины level_depth.¹³ Иерархия уровней E/R/R-систем формализуется через этот тип:

• Каждая система $S$ располагается на определённом уровне — $\text{Level}(S)\in ‘Level‘$.
• Элементы системы $S$ располагаются на уровне строго ниже: $\text{Level}(e)\ll \text{Level}(S)$ для всякого элемента $e\in S$.
• Каждый конкретный уровень имеет конечную глубину относительно основания — это и фиксирует теорема L5_no_infinite_descent из Главы 3. Интерпретация этого факта как отсутствия неоснованного нисхождения естественна; но саму теорему о невозможности бесконечной нисходящей цепи уровней пришлось бы формулировать отдельно — теорема L5_no_infinite_descent доказывает более слабое утверждение о конечной глубине каждого уровня.

Следствие: уровни нумеруются. Поскольку каждый уровень имеет конечную глубину, ему можно сопоставить натуральное число — эту глубину, считая от основания. Это даёт нумерацию уровней: $L_1$ (уровень основания), $L_2$, $L_3$, и так далее, неограниченно вверх.

Многоуровневые системы: примеры

Рассмотрим несколько примеров, в которых иерархия уровней проявляется явно. Прежде — важная оговорка о терминах. В примерах ниже мы говорим о доменно-относительных ярусах: о первом, втором, третьем ярусе конкретной модели (арифметической, физической, языковой). Эти доменные ярусы не следует отождествлять с формальными конструкторами типа Level из TheoryOfSystems_Core_ERR.v, где $L_1$ обозначает не <<первый ярус некоторой предметной области>>, а Логику / основание, а $L_2,L_3,\dots$ — надстраиваемые над ней уровни. Доменный ярус — объяснительное понятие, относительное к выбранной модели; формальный Level — фиксированная структура с $L_1=\text{Logic}$. Чтобы различать их, в примерах мы пишем <<первый доменный ярус>>, <<второй доменный ярус>> и т.д., а обозначения $L_1,L_2$ оставляем за формальным Level.

Натуральные числа и их множества. Первый доменный ярус арифметической модели: натуральные числа $1,2,3,\dots$. Каждое натуральное число — система простейшего типа (минимальный акт различения, фиксирующий <<это число>>, а не другое).¹⁴ Второй доменный ярус: множества натуральных чисел. Например, множество чётных $\{2,4,6,\dots \}$ или множество простых $\{2,3,5,7,\dots \}$ — системы, элементы которых суть натуральные числа первого яруса. Третий доменный ярус: функции, действующие на множествах натуральных чисел (сложение, умножение, операции теории чисел); их элементы — системы второго яруса (множества).

Физический мир. Первый доменный ярус физической модели: элементарные частицы (электрон, кварки). Второй доменный ярус: атомы — системы, элементы которых суть элементарные частицы. Третий доменный ярус: молекулы — системы, элементы которых атомы. Четвёртый доменный ярус: макроскопические объекты — системы, элементы которых молекулы.

Формальный язык. Первый доменный ярус языковой модели: символы алфавита. Второй доменный ярус: слова — системы, элементы которых символы. Третий доменный ярус: выражения — системы, элементы которых слова. Четвёртый доменный ярус: формальные тексты — системы, элементы которых выражения.

Общая структура. В каждом примере действует один и тот же принцип: системы более высокого яруса имеют в качестве элементов системы яруса более фундаментального. Различаются лишь конкретные правила и конкретные элементы, но вертикальная структура одна и та же. Это — проявление онтологического характера иерархии: она работает не в одной предметной области, а во всех. Подчеркнём ещё раз: иерархия доменных ярусов в каждой модели — это применение структуры порядка, а формальный тип Level с $L_1=\text{Logic}$ — та структура, которая в этих применениях используется; отождествлять <<первый ярус арифметики>> с формальным $L_1$ не следует.

Иерархия как разворачивание E/R/R

Структурное содержание. Каждый уровень иерархии — это вновь разворачивание E/R/R, но уже на более высоком уровне. Правила, роли, элементы системы $L_2$ — сами имеют свою E/R/R-структуру, но на масштабе $L_2$. Аналогично для $L_3$, $L_4$ и далее.

Универсальный слой работает на всех уровнях. Законы $L1$–$L5$ — универсальный слой правил («Универсальный слой: законы –») — работают на каждом уровне одинаково. Различается лишь конкретный слой: на $L_2$ работают правила теории множеств, на $L_3$ — теории функций, на $L_4$ — более высоких теорий. Универсальные законы — общая структура; конкретные правила — то, что характеризует именно данный уровень.

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

Следствие: предельный акт различения. На самом нижнем уровне иерархии работает простейший акт различения — запись Distinction, разобранная в Главе 2. Элементы $L_1$ суть определённые (отличные от не-себя) объекты, и эта определённость обеспечивается работой $L1$–$L5$ в простейшем виде. Иерархия уровней начинается с акта различения и разворачивается вверх через повторное применение E/R/R на каждом следующем уровне.

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

Мета-система: Абсолют

В «Иерархия как разворачивание E/R/R» было отмечено: иерархия уровней систем не имеет внутренней верхней границы, но имеет предельную структуру — мета-систему, формируемую универсальными законами и самим фактом существования. Эта мета-система — Абсолют, разобранный в метафизике Тома I. Настоящий раздел показывает, что Абсолют имеет E/R/R-структуру — и тем замыкает онтологическую цепь между метафизическим устройством и формальной работой настоящего тома.

Прежде чем разворачивать этот разбор, необходимо точно обозначить его статус. Всё, что говорится ниже об Абсолюте, не является теоремой текущей Rocq-формализации. В Coq-файлах репозитория нет формального объекта Absolute, нет Логики и Источника как элементов некоторой мета-системы, нет теоремы вида <<$E/R/R\to \text{Absolute}$>>. Формализация, разобранная в предыдущих разделах, даёт E/R/R как структуру систем; настоящий же раздел есть метафизическое применение этой структуры — применение E/R/R к Абсолюту, связывающее настоящий том с метафизикой Тома I. Это содержательный, а не машинно-проверенный шаг. Поэтому, когда выше говорилось, что каждое звено деривационной цепи выводится из предыдущих, к звену <<E/R/R $\to$ Абсолют>> это не относится: оно принадлежит метафизической интерпретации, а не текущему формальному корпусу. Читатель должен удерживать это различение на протяжении всего раздела.

Что значит «мета-система»

Структурное содержание. Абсолют не есть «система среди систем» — его место не в иерархии $L_1,L_2,L_3,\dots$ рядом с другими уровнями. Абсолют есть мета-устройство: то, что задаёт саму возможность иерархии уровней, прежде чем в ней появляется какой-либо конкретный уровень. Этим он отличается от любой системы внутри иерархии: внутренняя система — одна из многих; мета-система — условие самой возможности существования любой из них.

Абсолют есть мета-система, формируемая Логикой и Источником как своими элементами.

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

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

E/R/R-структура Абсолюта

Структурное содержание. Абсолют как мета-система имеет E/R/R-структуру, разбираемую следующим образом:

Аспект E/R/R	В Абсолюте
Elements	Логика, Источник
Roles	Структура, Наполнение
Rules	$L1$–$L5$ + правила распределения ролей

Elements Абсолюта: Логика и Источник. На уровне Elements Абсолюта работают ровно два носителя:

Логика — структурный принцип, организующий; то, по которому работают законы $L1$–$L5$. Источник — наполнение, на которое направлено действие Логики; то, что Логика организует.

Roles Абсолюта: Структура и Наполнение. Логика и Источник не просто «есть» — они занимают определённые позиции в мета-устройстве:

Структура — роль, требующая исполнения. В Абсолюте эту роль играет Логика. Без чего-то, играющего роль структуры, существование было бы аморфным, не определённым. Наполнение — роль, также требующая исполнения. В Абсолюте её играет Источник. Без наполнения структура была бы пустой формой, не имеющей содержания.

Две обязательные роли. Минимальная двойственность E/R/R («Минимальность: два элемента, две роли, два правила») проявляется в Абсолюте через две обязательные роли. Это не произвольное распределение: обе роли необходимы по $L4$ (закон достаточного основания) для самого факта существования. Без структуры — нет формы; без наполнения — нет содержания. Обе роли — необходимые условия существования.¹⁵

Rules Абсолюта: универсальное и конкретное. На уровне Rules Абсолюта работают два слоя, как в любой системе («Двухслойность Rules: универсальное и конкретное»):

Универсальный слой — законы $L1$–$L5$. Они работают в Абсолюте как и в любой системе — удерживая его как определённое мета-устройство. Конкретный слой — правила, фиксирующие распределение ролей. Они задают, что роли Абсолюта суть Структура и Наполнение (а не какие-либо иные), и что Логика играет роль Структуры, а Источник — роль Наполнения.

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

Это — структурное исключение, согласующееся с primordial-статусом Абсолюта («Primordial-статус»). В обычной системе generative order (Rules $\to$ Roles $\to$ Elements) разворачивается последовательно: правила определяются, под них — роли, под роли подбираются элементы. В мета-системе все три аспекта даны одновременно: нет «момента до подбора», поскольку нет ничего, что было бы «до» мета-системы. Логика, Источник, их роли и правила, устанавливающие распределение ролей — единое мета-устройство, данное как условие существования вообще.

Следствие: законы логики работают на уровне Rules Абсолюта. Из E/R/R-разбора Абсолюта следует: законы $L1$–$L5$ — не внутри Абсолюта как часть его содержания, а на уровне Rules мета-устройства. Это согласуется с зафиксированной позицией ((см. соответствующую главу)): законы онтологически первичны — они работают на мета-уровне как условия самой возможности любого существования.

Primordial-статус

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

Деривация из $L4$. Абсолют primordial по следующему структурному соображению: для самого факта существования необходимо мета-устройство, в котором имеется Структура и Наполнение. По $L4$ это требование — не произвольное, а структурно необходимое: без двух обязательных ролей определённое существование было бы невозможно. Следовательно, мета-устройство, реализующее эти роли (то есть Абсолют), не может «появиться» позже какого-либо существования — оно есть условие существования вообще.

Следствие: невозможность вопроса «откуда Абсолют?». Спрашивать, откуда взялся Абсолют, или что было «до» Абсолюта — значит делать категориальную ошибку. Вопрос «откуда?» предполагает существование того, относительно чего ставится; но Абсолют есть само условие такого существования. Не существует «до Абсолюта», потому что не существует ничего, относительно чего можно было бы определить это «до».

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

Замыкание онтологической цепи

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

$$A=\exists \to \text{Distinction}\to L1\text{–}L5\to P1\text{–}P4\to E/R/R\to \text{Абсолют}.$$

Каждое звено цепи — структурное условие, выводимое из предыдущих. Завершающее звено — Абсолют как мета-система, реализующая E/R/R-структуру на мета-уровне.

Связь Тома I и настоящего тома. В Томе I Абсолют разбирается из позиции метафизики — как первоначальное мета-устройство, делающее возможным какое-либо существование. В настоящем томе Абсолют появляется как предельная структура E/R/R — мета-система, к которой применимы те же категории Elements, Roles, Rules, что и к обычным системам, но с учётом её primordial-статуса: подбор элементов под роли, работающий в обычных системах, в мета-системе не действует — Логика и Источник даны одновременно со своими ролями. Это не два разных Абсолюта: это одна структура, разобранная с двух сторон — метафизической и формальной.

Следствие: формальный аппарат E/R/R универсален. Из работы E/R/R на мета-уровне (в Абсолюте) и на каждом конкретном уровне ($L_1,L_2,L_3,\dots$) следует: E/R/R-структура — не ограниченный инструмент, применимый только к определённому классу систем, а универсальная онтологическая структура. Она работает везде, где работает определённое существование — от простейшего акта различения до мета-системы существования как такового. При этом в мета-системе generative order реализуется в предельной форме: не как последовательность разворачивания, а как одновременная данность всех трёх аспектов.

Следствие: онтологическая первичность подтверждена. Зафиксированная в Главе 3 онтологическая первичность законов $L1$–$L5$ получает дополнительное подтверждение: эти законы работают на уровне Rules самой мета-системы, не внутри какой-либо конкретной системы. Они не «вводятся» в формальную теорию — они уже есть в самой структуре мета-устройства. Их вывод в Rocq как теорем (Глава 3) — методологическое прослеживание, не онтологическое основание.

С разбором Абсолюта мы получаем полное представление об онтологической структуре E/R/R — от простейшего акта различения через иерархию уровней к мета-системе. В следующем разделе мы проверим состоятельность самой E/R/R-структуры через её самоприменение: разберём структуру E/R/R как систему через её собственный аппарат.

Самоприменение E/R/R

В предыдущих разделах E/R/R-структура была разобрана как онтология любой системы — от простейшего акта различения через иерархию уровней до мета-системы Абсолюта. Возникает естественный вопрос проверки: сама E/R/R-структура — хорошо ли она сформирована как система? Иначе говоря, если применить E/R/R-разбор к E/R/R как к системе, получится ли согласованный результат, или возникнут структурные противоречия?

Этот вопрос — проверка состоятельности структуры. Параллель с работой Главы 3: в (см. соответствующую главу) было показано, что $L4$ самообоснован в формальной системе Rocq — закон достаточного основания обосновывает сам себя. Аналогичная проверка требуется для E/R/R: если структура внутренне противоречива при самоприменении, она не годится как универсальная онтология систем.

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

Структурное содержание. Применить E/R/R к E/R/R — значит рассмотреть саму E/R/R-структуру как систему и провести её E/R/R-разбор. Конкретно: какие Elements в самой E/R/R-структуре? Какие Roles они играют? Какие Rules работают?

Принципиальная разница с Абсолютом. В «Мета-система: Абсолют» Абсолют был разобран как мета-система — с особенностью: его элементы не подбираются под роли, а даны как primordial. E/R/R — не Абсолют. Это онтологическая структура, прослеживаемая в любой системе (включая Абсолют), но сама не являющаяся мета-системой. При самоприменении E/R/R работает в обычном режиме — с подбором элементов под роли, как в любой системе уровня иерархии.

Замечание: самоприменение формализовано. { Это самоприменение теперь закреплено и машинно. В файле PrinciplesToERR.v E/R/R-триада записана как объект ERRSystem (err_meta_system), и теорема err_self_well_formed доказывает, что она проходит тот самый критерий хорошей сформированности из ERRWellFormedness.v¹⁶ — E/R/R удовлетворяет собственному критерию. Существенно, чем именно: теорема self_application_not_self_membership разделяет два смысла <<E/R/R применяется к себе>>. Это самоприменение (стратифицированное самоописание, уровнем ниже), а не самочленство ($x\in x$, при котором $\mathrm{level}(S)<\mathrm{level}(S)$), запрещаемое $P1$; и потому оно $P1$-совместимо, а не исключение из неё. Самосогласованность E/R/R доказана отдельной Rocq-теоремой, без аксиом; содержательный разбор ниже разворачивает то, что эта теорема фиксирует.}

E/R/R применена к E/R/R: разбор

Elements. В самой E/R/R-структуре есть три различимых аспекта: Elements, Roles, Rules. Эти три аспекта — сами Elements в E/R/R-разборе E/R/R-структуры. То есть на уровне Elements самоприменения мы имеем:

• Элемент $E$ — категория «Elements» (как аспект структуры).
• Элемент $R_1$ — категория «Roles» (как аспект).
• Элемент $R_2$ — категория «Rules» (как аспект).

Каждый из этих трёх — определённый, различимый от двух других. По $L1$, каждая категория тождественна себе: Elements — именно Elements, не что-либо иное; аналогично для Roles и Rules.

Roles. На уровне Roles самоприменения работают функции, которые играют три категории в системе. Каждая категория выполняет определённую функцию:

• Категория Elements играет роль «носителя субстрата системы» — то, через что в системе есть что-то.
• Категория Roles играет роль «носителя функциональных позиций» — то, через что элементы получают значимость.
• Категория Rules играет роль «носителя организующих законов» — то, через что система удерживается как система.

По $L4$, каждое ролевое назначение обосновано: категория Elements играет роль субстрата потому что в любой системе требуется субстрат, и эту функцию принимает на себя именно категория «что есть»; аналогично для Roles и Rules.

Rules. На уровне Rules самоприменения работают два слоя («Двухслойность Rules: универсальное и конкретное»):

Универсальный слой — законы $L1$–$L5$, которые работают и здесь, как в любой системе. Конкретный слой — правила самой E/R/R-структуры:

• Правило «три категории — ровно три, не больше и не меньше» (по минимальности E/R/R, «Минимальность: два элемента, две роли, два правила»).
• Правило «категории различимы между собой» (отсюда смешение категорий E/R/R недопустимо — что разворачивается в «Парадоксы как смешение E/R/R-категорий»).
• Правило «работают в generative order: Rules задают Roles, Roles ограничивают Elements» («Асимметрия и generative order»).

Замечание о подборе элементов. В самоприменении подбор элементов под роли работает в предельной форме: сами категории E/R/R играют определённые роли. Это не «подбор из произвольного множества кандидатов», а единственно возможное ролевое распределение — категория «Elements» не может играть роль «носителя организующих законов», поскольку организация — функция Rules, не Elements. Распределение ролей в самоприменении задано самой структурой.

Проверка well-formedness

Критерий хорошей сформированности. В файле ERRWellFormedness.v (детально — в «Парадоксы как смешение E/R/R-категорий») зафиксирован критерий: система хорошо сформирована, если каждый её компонент относится ровно к одной E/R/R-категории и нет самореференции через категории.¹⁷

Проверка для самой E/R/R. Применим критерий к самоприменению E/R/R:

Однозначность категорий. Каждая из трёх категорий — Elements, Roles, Rules — относится ровно к одной E/R/R-категории в самоприменении (как Element в нашем разборе). Однозначность соблюдена.

Отсутствие самореференции. Категория Rules не выступает элементом самой себя; категория Elements не выступает правилом для самой себя; категория Roles не выступает элементом самой себя. Содержательно это согласуется с $P1$ (иерархия): самоотношение через уровни не возникает. Самореферентного отношения через категории в этом разборе не обнаруживается.

Следствие: самоприменение не обнаруживает нарушения. Сформулируем вывод осторожно, в соответствии со статусом разбора. В текущей версии ToS самосогласованность E/R/R — не машинно-проверенная теорема, а содержательная проверка по критерию, формализованному в ERRWellFormedness.v для известных парадоксальных систем. Поэтому корректная формулировка такова: самоприменение E/R/R не обнаруживает структурного нарушения по тем же признакам (самореференция, смешение категорий), по которым формально диагностируются парадоксальные системы. Это содержательное свидетельство в пользу того, что E/R/R годится как универсальная онтология систем, — но именно содержательное свидетельство, а не доказанная в Rocq теорема о самосогласованности.

Параллель с самообоснованием $L4$

Структурное содержание. Самосогласованность E/R/R — структурное явление, параллельное самообоснованию $L4$, зафиксированному в Главе 3 ((см. соответствующую главу)). В обоих случаях формальный аппарат ToS может быть применён к самому себе, и в обоих случаях результат — согласованность, не противоречие.

Параллель. ;; $L4$ применён к себе. Закон достаточного основания утверждает, что всякое существование имеет основание. Применяя $L4$ к самому $L4$: основанием $L4$ является структурная несовместность противоречия (поле exclusive в записи Distinction). Закон обосновывает сам себя без обращения к чему-либо внешнему.

E/R/R применена к себе. Структура E/R/R утверждает, что всякая система разбираема в три аспекта. Применяя E/R/R к самой E/R/R: структура разбираема в три категории (Elements, Roles, Rules) без самореференции и без смешения категорий. Структура обосновывает свою применимость к самой себе.

Следствие: самосогласованность как структурное свойство ToS. Из самообоснования $L4$ и самосогласованности E/R/R следует, что формальный аппарат ToS обладает важным методологическим свойством: его центральные структуры (закон достаточного основания и онтология E/R/R) не зависят от чего-либо внешнего для своей применимости. Они работают через себя — что согласуется с зафиксированной онтологической первичностью законов логики и E/R/R-структуры.

С проверкой состоятельности E/R/R через самоприменение мы получаем основание перейти к её применениям — сначала к простейшей системе, записи Distinction, а затем к универсальной конструкции distinction_of.

Применение к Distinction

С разработанным аппаратом E/R/R и проверенной самосогласованностью структуры можно перейти к её рабочему применению — разбору конкретных формальных структур, уже введённых в настоящей работе. Первое такое применение — к записи Distinction, простейшей формальной системе, введённой в Главе 2 и разработанной в Главе 3.

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

Постановка

{

Что разбираем. Запись Distinction с четырьмя полями positive, negative, exclusive, exhaustive, формализующая акт различения. Структурный разбор четырёх полей был проведён в (см. соответствующую главу) Главы 2; формальный вывод законов из этой записи — в Главе 3. Здесь мы расставляем содержание акта различения в три E/R/R-категории и проверяем, что результат хорошо сформирован. }

Уровень системы. В содержательной интерпретации иерархии уровней Distinction удобно понимать как систему уровня основания: запись не содержит в качестве элементов других систем, она напрямую фиксирует акт различения. Как и в случае distinction_of («Применение к distinction_of»), это — интерпретация в терминах иерархии, а не буквальная типизация Distinction в Level: формально Distinction есть Record, не объект System L.

Порядок разбора. Согласно онтологическому порядку («Порядок изложения»), разбор производится в направлении Rules $\to$ Roles $\to$ Elements: сначала устанавливаются правила, затем — роли, ими определённые, и лишь затем — элементы, играющие эти роли.

E/R/R-разбор Distinction

Rules: универсальные законы и поля exclusive, exhaustive. На уровне Rules в Distinction работают два слоя («Двухслойность Rules: универсальное и конкретное»):

Универсальный слой — законы $L1$–$L5$. Они работают в Distinction как теоремы, выведенные в Главе 3.

Конкретный слой — два структурных поля самой записи, формализующие правила работы акта различения:

• Поле exclusive ($\neg (‘positive‘\wedge ‘negative‘)$) — правило, фиксирующее, что положительная и отрицательная стороны несовместны.
• Поле exhaustive ($‘positive‘\vee ‘negative‘$) — правило, фиксирующее, что между сторонами нет третьего.

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

Roles: положительная сторона и отрицательная сторона. Правила работы акта различения определяют две позиции, которые должны быть заполнены:

• Роль положительной стороны — позиция выделенного: того, что в акте различения предъявляется как определённое содержание. В записи Distinction эту роль задаёт поле positive.
• Роль отрицательной стороны — позиция фона: того, относительно чего предъявление обретает определённость. Эту роль задаёт поле negative.

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

Elements: положительная и отрицательная стороны. На уровне Elements в акте различения работают две стороны различения. Для конкретного экземпляра $D:‘Distinction‘$ это значения positive $D$ и negative $D$ — ровно так устроен err_elements в ERRFromDistinction.v. Когда запись применяется через универсальную конструкцию distinction_of $(A)$ ((см. соответствующую главу) Главы 2), эти значения суть пропозиция $A$ и её отрицание $\neg A$:

• Пропозиция $A$ — положительная сторона, элемент, занимающий роль выделенного.
• Пропозиция $\neg A$ — отрицательная сторона, элемент, занимающий роль фона.

По $L1$, каждый из этих элементов тождественен себе: $A=A$, $\neg A=\neg A$. Множественность — ровно два элемента, как было показано в «Минимальность: два элемента, две роли, два правила»: один элемент не образует различения, а два — ровно столько, сколько нужно.

Два уровня чтения: экземпляр и схема. В этом разборе необходимо явно различить два уровня, иначе E/R/R-разметка Distinction вступит в противоречие с формализацией.

{ Уровень экземпляра. Для конкретного $D:‘Distinction‘$ элементы — это значения positive $D$ и negative $D$. Именно так устроена формализация: файл ERRFromDistinction.v определяет список элементов как

err_elements D := [ positive D; negative D ],

то есть положительная и отрицательная стороны экземпляра суть Elements E/R/R-разбора. На уровне экземпляра расстановка такова: Elements суть positive $D$ и negative $D$; Roles — <<выделенное>> и <<фон>>; Rules — exclusive и exhaustive. }

Уровень схемы записи. На уровне самой record-схемы Distinction как типа имена полей positive и negative можно прочитать иначе — как ролевые слоты: <<положительная сторона>> и <<отрицательная сторона>>, две позиции, которые конкретный экземпляр заполняет. Это чтение полезно содержательно: оно показывает, что схема задаёт потенциал акта различения. Но его нужно понимать именно как мета-уровневое прочтение record-схемы, а не как буквальную E/R/R-разметку, совпадающую с ERRFromDistinction.v. В формализации Elements — это значения positive $D$ и negative $D$ экземпляра, а не содержимое <<внутри>> ролевых слотов схемы.

Иными словами: расстановка <<Elements $=$ значения полей>> относится к экземпляру $D$ и буквально совпадает с кодом; прочтение <<positive/negative $=$ ролевые слоты>> относится к схеме Distinction и есть содержательная мета-интерпретация. Оба прочтения законны, но смешивать их нельзя.

Соответствие полей записи и E/R/R-категорий. Итоговая расстановка — с явным указанием обоих уровней чтения:

Поле	Уровень экземпляра $D$	Уровень схемы
positive	Element: значение positive $D$	ролевой слот
negative	Element: значение negative $D$	ролевой слот
exclusive	Rule: несовместность сторон	Rule
exhaustive	Rule: исчерпанность сторон	Rule

Левый столбец — буквальная E/R/R-разметка экземпляра, совпадающая с кодом файла ERRFromDistinction.v: positive $D$ и negative $D$ суть Elements. Правый столбец — мета-уровневое прочтение схемы, в котором positive и negative видятся ролевыми слотами. Роли E/R/R-разбора (<<выделенное>> и <<фон>>) на уровне экземпляра суть позиции, которые занимают эти два элемента; на уровне схемы они и есть сами слоты.

Проверка well-formedness

Критерий. По критерию хорошей сформированности («Проверка well-formedness», «Парадоксы как смешение E/R/R-категорий»): однозначность категорий и отсутствие самореференции через категории.

Проверка для Distinction. Однозначность категорий. На уровне экземпляра $D$: positive $D$ и negative $D$ — элементы, поля exclusive и exhaustive — правила, роли <<выделенное>>/<<фон>> — позиции, которые элементы занимают. Каждый компонент однозначно относится к одной E/R/R-категории; в формализации ERRWellFormedness.v эта однозначность встроена в само представление — категория компонента задана функцией, так что двух категорий у одного компонента быть не может.

Отсутствие самореференции. Поле exclusive есть правило о соотношении ролей positive и negative, не о самом себе. Поле exhaustive аналогично. По $P1$ такая самореференция через уровни структурно невозможна. Элементы $A$ и $\neg A$ играют свои роли, не ссылаясь на самих себя в качестве правил или ролей.

Следствие: Distinction хорошо сформирована. { Простейшая формальная структура настоящего тома удовлетворяет критерию E/R/R-разбора — и это теперь не только содержательно. В файле PrinciplesToERR.v Distinction записана как объект ERRSystem (distinction_meta_system), и теорема distinction_err_well_formed машинно подтверждает, что она проходит критерий is_well_formed; а every_distinction_err_well_formed распространяет это на всякий такой разбор. Содержательное обоснование её правомерности как формальной модели акта различения подкреплено отдельной Rocq-теоремой.}

Что даёт разбор

Структурное содержание. E/R/R-разбор Distinction показывает следующее:

• Сама запись Distinction как тип в Rocq фиксирует потенциал акта различения: правила и роли заданы, элементы — ещё нет. Запись — структурный шаблон, не конкретный акт.
• Конкретный акт различения — актуализация, при которой роли positive и negative заполняются конкретными пропозициями $A$ и $\neg A$.
• Различие потенциального и актуального модусов существования системы («Elements: актуализация потенциала») проявляется здесь с особой ясностью: тип Distinction — потенциал; экземпляр mkDistinction $A$ $\neg A$ … — актуализация.

Следствие: методология работает. Применение E/R/R к простейшей формальной структуре даёт согласованный результат: каждое поле находит своё место в E/R/R-категориях, конкретные элементы актуализуют структуру, проверка well-formedness проходит. Это — первое рабочее подтверждение применимости методологии к конкретным формальным объектам настоящего тома.

Следствие: основа для применения к производным конструкциям. { Distinction — базовая запись, на которой построена универсальная конструкция distinction_of (разобранная в (см. соответствующую главу) Главы 2). Поскольку Distinction хорошо сформирована, конструкция distinction_of наследует E/R/R-согласованность — что мы разбираем в следующем разделе. }

Применение к distinction_of

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

E/R/R-разбор distinction_of даёт качественно новое: эта конструкция не есть отдельный акт различения — она есть механизм производства актов различения для произвольных пропозиций. Это первая в настоящей работе система-производитель, а не просто система-носитель.

Постановка

Что разбираем. Конструкция distinction_of $(P)$, которая для любой пропозиции $P:‘Prop‘$ строит экземпляр записи Distinction со следующими значениями полей: positive $=P$, negative $=\neg P$, поле exclusive получает конструктивное доказательство несовместности $P$ и $\neg P$, поле exhaustive получает доказательство $P\vee \neg P$ из аксиомы classic (как обсуждалось в (см. соответствующую главу) Главы 3).

Уровень: содержательная интерпретация. { В содержательной E/R/R-интерпретации distinction_of удобно понимать как конструкцию более высокого уровня, чем Distinction: она принимает пропозицию и строит экземпляр Distinction, и по принципу иерархии конструкция-производитель стоит над тем, что она производит. Это — полезное объяснительное прочтение. Но нужно сразу оговорить его статус относительно формализации. В текущей формализации Distinction есть Record, а distinction_of — Definition-функция, строящая экземпляр из пропозиции $P$; ни то ни другое не оформлено как объект типа System L с конкретным уровнем. Когда ниже мы говорим, что distinction_of <<принадлежит уровню $L_2$>>, а Distinction <<есть запись уровня $L_1$>>, — это интерпретация функции-конструктора в терминах иерархии, а не буквальная типизация в типе Level, имеющаяся в коде. Содержательно интерпретация верна и полезна; формально же типизация distinction_of и Distinction в Level пока не проведена. }

Порядок разбора. Согласно онтологическому порядку, разбор производится в направлении Rules $\to$ Roles $\to$ Elements.

E/R/R-разбор distinction_of

Rules: универсальные законы и правила конструкции. На уровне Rules в distinction_of работают два слоя:

Универсальный слой — законы $L1$–$L5$, работающие на уровне $L_2$. В частности, $P1$ (иерархия) обеспечивает, что distinction_of как функция стоит на уровне выше своих значений; $L4$ обеспечивает обоснованность всех полей строящегося экземпляра.

Конкретный слой — правила, специфичные для конструкции:

• Правило применения mkDistinction: для построения экземпляра Distinction конструктор требует четыре аргумента — две пропозиции и два доказательства.
• Правило конструктивного доказательства exclusive: для произвольной $P$ доказательство $\neg (P\wedge \neg P)$ строится конструктивно (это — $L2$ для $P$, не требующее аксиом).
• Правило обращения к аксиоме classic: для получения exhaustive $=P\vee \neg P$ используется classic, поскольку для произвольной пропозиции исчерпанность конструктивно не доказуема ((см. соответствующую главу) Главы 3).

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

• Роль входа — позиция, занимаемая параметром, для которого строится экземпляр. В distinction_of $(P)$ эту позицию занимает пропозиция $P$.
• Роль выхода — позиция, занимаемая построенным результатом. Эту позицию занимает построенный экземпляр Distinction.

По $L4$, обе роли обоснованы: вход необходим, поскольку конструкция универсальна и должна работать для произвольной пропозиции; выход — поскольку именно построенный экземпляр есть результат применения конструкции. Без входа не было бы предмета для построения; без выхода — результата построения.

Замечание: внутренние роли построенного экземпляра. Помимо ролей входа и выхода, внутри построенного экземпляра Distinction работают те же роли, что были разобраны в «E/R/R-разбор Distinction»: положительная сторона и отрицательная сторона. Эти роли — наследие записи Distinction, работающее на уровне $L_1$ внутри результата уровня $L_2$.

Elements: пропозиция $P$ и построенный экземпляр. На уровне Elements в distinction_of работают:

• Пропозиция $P$ — актуальный носитель роли входа. Это — произвольная пропозиция типа Prop, передаваемая конструкции.
• Построенный экземпляр Distinction $(P,\neg P,\dots )$ — актуальный носитель роли выхода. Это — конкретный объект записи Distinction, в котором роли заполнены пропозициями $P$ и $\neg P$.

По $L1$, каждый из этих элементов тождественен себе: данная пропозиция $P$ остаётся той же пропозицией; построенный экземпляр остаётся тем же экземпляром.

Соответствие компонент и E/R/R-категорий.

Компонент	Что фиксирует	E/R/R-категория
mkDistinction	Применение конструктора	Rule (конкр. слой)
Constructive exclusive	Правило для $L2$	Rule (конкр. слой)
Use of classic	Правило для $L3$	Rule (конкр. слой)
Позиция входа	Роль параметра	Role
Позиция выхода	Роль результата	Role
Пропозиция $P$	Актуальный вход	Element
Экземпляр Distinction	Актуальный выход	Element

Проверка well-formedness

Однозначность категорий. Каждый компонент конструкции относится ровно к одной E/R/R-категории. Правила (mkDistinction, конструктивное доказательство, обращение к classic) — именно правила, не роли и не элементы. Позиции входа и выхода — роли, не правила. Пропозиция $P$ и построенный экземпляр — элементы, актуализующие эти роли.

Отсутствие самореференции. Конструкция distinction_of не ссылается на самой себя в качестве своего параметра — она принимает произвольную пропозицию, не распространяет себя на саму себя. По $P1$ такая самореференция через категории структурно невозможна: конструкция стоит на уровне $L_2$, её значения — на уровне $L_1$, и переход обратно невозможен.

Следствие: distinction_of хорошо сформирована. Универсальная конструкция, наследующая E/R/R-согласованность от Distinction («Проверка well-formedness»), сама удовлетворяет критерию хорошей сформированности.

Что даёт разбор

Структурное содержание. E/R/R-разбор distinction_of показывает следующее:

• Конструкция-производитель имеет E/R/R-структуру более сложную, чем простая запись: появляются новые роли (вход и выход), специфичные для механизмов производства.
• Иерархия уровней работает явно: distinction_of на $L_2$, её значения — на $L_1$, и переход $L_2\to L_1$ есть актуализация (применение конструкции к конкретной пропозиции).
• Двухслойность Rules проявляется: конкретный слой содержит как конструктивные правила (применение mkDistinction, конструктивное доказательство exclusive), так и правила обращения к аксиоме (classic для exhaustive).

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

Следствие: подготовка к диагностике парадоксов. В «Проверка well-formedness» мы убедились, что distinction_of не приводит к самореференции. Но что если бы мы попытались построить конструкцию самореферентную — например, такую, которая строит Distinction для пропозиции, утверждающей что-либо о самой конструкции? Здесь начинается работа E/R/R как диагностического инструмента — предмет следующего раздела.

Парадоксы как смешение E/R/R-категорий

В §«Применение к Distinction»–«Применение к distinction_of» методология E/R/R работала как конструктивный инструмент — мы разбирали хорошо построенные структуры и убеждались, что они хорошо сформированы. Настоящий раздел переворачивает направление: E/R/R применяется как диагностический инструмент к структурам, в которых что-то идёт не так — к классическим парадоксам.

Центральное наблюдение: парадоксы — не глубокие тайны, открывающие пределы разума, а диагностические сигналы того, что в построении нарушено E/R/R-устройство. При корректной диагностике парадокс не решается — он растворяется: становится видно, в каком именно месте конструкция нарушает категориальное устройство, и сам вопрос, который ставит парадокс, оказывается некорректно поставленным.

Парадоксы — это смешение E/R/R-категорий: один и тот же объект пытается одновременно играть две различные категориальные роли.

Диагностическая функция E/R/R

{

Растворение, не решение. Принципиальное различие между двумя подходами к парадоксам — решением и растворением. Решить парадокс — ответить на вопрос, который он ставит: «истинна ли лгущая фраза?», «содержит ли множество Рассела само себя?». Растворить парадокс — показать, что сам вопрос некорректно поставлен, не имеет осмысленного содержания, поскольку конструкция, лежащая в его основе, нарушает структуру. }

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

E/R/R как универсальный диагностический инструмент. Поскольку всякая корректная система имеет E/R/R-структуру, любая конструкция, претендующая на статус системы, должна разбираться через три категории — Elements, Roles, Rules — однозначно и без самореференции. Парадоксы — именно те конструкции, для которых такой разбор невозможен: одна и та же сущность пытается одновременно занимать места разных категорий. Это — структурное нарушение, которое формализуется в Rocq и проверяется машинно.¹⁸

Место структурных парадоксов в общей классификации

В более широкой работе по диагностике парадоксов¹⁹ парадоксы классифицируются по типу нарушения:

• Структурные парадоксы — нарушают вертикальное устройство, смешивая E/R/R-категории; самореференция в самой конструкции. Сюда относятся парадоксы Рассела, Лжеца, Грелинга, Кантора, Бурали-Форти, Берри, Ричарда, Карри, Ябло и другие.
• Дефектные парадоксы — содержат изъян в посылках (концептуальная неопределённость, скрытое противоречие, ложная посылка, категориальная ошибка). К ним относятся, в частности, парадокс Сорита, парадокс корабля Тесея, парадоксы Зенона и парадоксы бесконечности (Гильберта, Галилея, Банаха–Тарского).
• Не-парадоксы — контр-интуитивные, но корректные результаты, не содержащие противоречия (Монти Холл, парадокс дней рождения, парадокс Симпсона).

В настоящем разделе мы подробно разбираем структурные парадоксы — те, что разрешаются непосредственно через E/R/R-диагностику. Дефектные парадоксы и не-парадоксы требуют иных инструментов, выходящих за рамки настоящей работы.

Парадокс Рассела: Element = Rule

Конструкция. Рассмотрим множество $R$ всех множеств, не содержащих самих себя. Спрашивается: содержит ли $R$ само себя? Если $R\in R$, то по определению $R\notin R$; если $R\notin R$, то по определению $R\in R$. Противоречие.

E/R/R-диагноз. В конструкции Рассела одна и та же сущность — множество $R$ — занимает две категории одновременно:

• Как Element: $R$ выступает кандидатом на собственное членство; вопрос «$R\in R$?» предполагает $R$ как элемент.
• Как Rule: $R$ определяется правилом «не содержит себя» и сам играет роль критерия, по которому проверяется его собственная принадлежность.

Иными словами: Element = Rule. Объект пытается быть одновременно тем, что классифицируется, и тем, что классифицирует.

Нарушение $P1$. В «: иерархия» было показано, что $P1$ (иерархия, $S\notin S$) выводится из $L1+L5$. Применительно к парадоксу Рассела: множество не может быть собственным элементом, поскольку организатор и организуемое располагаются на разных уровнях. Конструкция $R\in R$ требует $\text{Level}(R)<\text{Level}(R)$, что нарушает иррефлексивность $L5$.

{

Формальное растворение. В репозитории конструкция Рассела формализована как russell_system в ERRWellFormedness.v и проверена на хорошую сформированность — результат false. Это устанавливают машинно две теоремы в двух файлах: лемма russell_ill_formed в самом ERRWellFormedness.v (прямо о russell_system) и лемма russell_is_ill_formed в ParadoxDiagnosis.v (через отображение paradox_system, сопоставляющее типу парадокса его E/R/R-систему).²⁰ }

Историческое решение и его место в E/R/R-картине. Классическое решение — теория типов Рассела — разносит множества и элементы по разным типам, делая самопринадлежность синтаксически невыразимой. Аксиома регулярности в ZFC формулирует то же требование через запрет $\in$-циклов. Оба решения — частные случаи общего $P1$: организатор и организуемое — разные уровни.

Парадокс Лжеца: Element применяет Rule к себе

Конструкция. Высказывание $L$: «Это высказывание ложно».²¹ Если $L$ истинно — то $L$ ложно; если $L$ ложно — то $L$ истинно. Противоречие.

E/R/R-диагноз. Высказывание $L$ занимает две позиции:

• Как Element: $L$ есть само высказывание, на которое направлена оценка истинности.
• Как Rule: $L$ применяет операцию оценки истинности к самому себе — содержит в себе саму эту операцию.

Это — особый случай: Element применяет Rule к самому себе. Самореферентное применение оценки приводит к тому, что высказывание должно существовать до собственной оценки (как объект) и одновременно содержать эту оценку (как часть себя).

Нарушение $L5$. По $L5$, операции располагаются на уровне выше тех, к чему применяются. Оценка истинности — операция, работающая над высказыванием как над объектом. Включение оценки в само высказывание совмещает уровни операции и операнда, что структурно невозможно.

Формальное растворение. Конструкция Лжеца формализована как liar_system; теорема liar_is_ill_formed устанавливает её ill-formed-статус.

Связь с иерархией Тарского. Тарский разделил язык-объект и метаязык: оценка истинности высказываний языка-объекта производится в метаязыке, на уровне выше. Это — частный случай иерархии уровней. Соотношение с нашим подходом нужно сформулировать точно. У Тарского строится открытая иерархия языков и метаязыков, неограниченно продолжающаяся вверх. В ToS иерархия уровней Level устроена схоже в одном отношении и иначе — в другом: каждый конкретный уровень имеет конечную глубину относительно основания (это и есть содержание $L5$ и теоремы L5_no_infinite_descent), но сама иерархия не имеет внутренней верхней границы — она продолжается вверх неограниченно через конструктор следующего уровня. То есть отличие не в том, что <<наша иерархия конечна, а тарская бесконечна>>: верно, что каждый уровень достижим за конечное число шагов от основания, и при этом уровней неограниченно много.

Парадокс Грелинга: Rule = Element

Конструкция. Слово называется гетерологическим, если оно не описывает себя (например, «длинный» — короткое слово, не описывает себя). Гетерологично ли слово «гетерологический»? Если да — то по определению оно не описывает себя, то есть не гетерологично; если нет — то описывает себя, значит гетерологично.

{

E/R/R-диагноз. Слово «гетерологический» занимает две позиции: }

• Как Rule: оно есть свойство (правило применимости предиката), работающее на словах.
• Как Element: при тесте на самоприменимость оно само рассматривается как слово, к которому правило применяется.

Здесь Rule = Element. Правило пытается быть собственным операндом.

Нарушение иерархии. Свойство (предикат) и объект, к которому оно применяется, — разные уровни ($L5$). Свойство «гетерологический» применяется на уровне второго порядка — к самим словам как объектам уровня первого порядка. Применение свойства к себе требует свойства одновременно быть на двух уровнях, что невозможно по $P1$.

Формальное растворение. grelling_system ill-formed; теорема grelling_is_ill_formed.

Историческая параллель. Стратификация типов Рассела — предикаты на словах располагаются на уровне выше слов; применение предиката к самому предикату как к слову блокируется синтаксически.

Парадоксы Кантора и Бурали-Форти

Парадокс Кантора. Множество всех множеств $U$. Должно содержать все множества, включая само себя, что даёт $U\in U$.

E/R/R-диагноз: $U$ занимает две позиции — как System (целая система всех множеств) и как Element (член самой себя). Это — System = Element самой себя. Нарушение $P1$ непосредственно.

Парадокс Бурали-Форти. Множество всех порядковых чисел. Его порядковый тип — порядковое число, большее всех порядковых, что противоречит его собственному определению как множества всех.

E/R/R-диагноз: тотальность всех порядковых $\Omega$ занимает две позиции — как Totality (само множество) и как Element (входящее в эту тотальность). Структурно та же ошибка: Totality = Element самой себя.

{

Формальное растворение. Обе конструкции структурно эквивалентны конструкции Рассела — самопринадлежности тотальности. В репозитории они представлены через russell_system (Кантор) и grelling_system (Бурали-Форти) как конкретизации общего паттерна самопринадлежности.²² }

Историческое решение. В ZFC отказ от универсального множества и переход к собственным классам (NBG, MK) формализуют именно тот запрет, который выражает $P1$: тотальности не могут быть собственными элементами.

Унифицированная диагностика

Главная теорема. Все пять разобранных парадоксов структурно ill-formed. В Rocq это зафиксировано единой теоремой:

Theorem all_paradoxes_ill_formed : forall p : ParadoxType,
  is_well_formed (paradox_system p) = false.

где ParadoxType перечисляет пять парадоксов, а paradox_system сопоставляет каждому из них формальную конструкцию.²³

Унифицированная таблица. Все пять структурных парадоксов сводятся в единую таблицу через тип нарушения E/R/R-категорий:

Парадокс	E/R/R-нарушение	Истор. решение
Рассел	Element = Rule	Теория типов
Лжец	Element применяет Rule к себе	Иерархия Тарского
Грелинг	Rule = Element	Стратификация типов
Кантор	System = Element самой себя	Нет универс. множества
Бурали-Форти	Totality = Element самой себя	Собственные классы

{

Контрапозитив. Если система хорошо сформирована, она не может совпадать ни с одной из парадоксальных конструкций. Это зафиксировано теоремой well_formed_paradox_free: хорошая сформированность исключает парадоксальность. }

Связь с принципами $P1$–$P4$. Принципы, разобранные в «Четыре принципа», работают как структурные блокировки парадоксов:

• $P1$ (иерархия) блокирует парадоксы Рассела, Кантора, Бурали-Форти — запрещая самопринадлежность.
• $P2$ (предшествование критерия) блокирует Лжеца — требуя, чтобы оценка истинности была определена до применения к высказыванию.
• $P3$ (интенсиональное тождество) различает «пустые» системы с разными критериями — в отличие от ZFC, где есть единственное пустое множество.
• $P4$ (конечная актуальность) растворяет парадоксы бесконечности (Гильберт, Галилей, Банах–Тарский), которые в классификации относятся к дефектным: они возникают из трактовки бесконечности как завершённого объекта.

Контр-примеры: хорошо сформированные системы

Диагностическая функция E/R/R работает в обоих направлениях. Не только парадоксы получают точный диагноз — хорошо сформированные системы проверяются как корректные.

Натуральные числа. Структура натуральных чисел разбирается через E/R/R следующим образом:

• Elements: конкретные натуральные числа $1,2,3,\dots$ как носители.
• Roles: позиция «единица» (начало) и позиция «преемник» (для каждого числа).
• Rules: универсальный слой ($L1$–$L5$) и конкретный слой (правила построения — единица и преемник).

Категории однозначны, самореференции нет.²⁴ Натуральные числа — хорошо сформированная система.

Шахматы. Игра в шахматы также разбирается через E/R/R:

• Elements: конкретные фигуры на доске и клетки доски.
• Roles: типы фигур (король, ферзь, слон и так далее), типы клеток, понятия позиции и хода.
• Rules: универсальный слой и конкретный слой (правила ходов, условия победы).

Каждая фигура — именно элемент, не правило; каждое правило — именно правило, не фигура. Категории не смешиваются; самореференции нет. Шахматы — хорошо сформированная система.²⁵

Следствие: критерий работает в обе стороны. E/R/R-диагностика отличает парадоксы от хорошо сформированных систем точно и формально. Парадоксы выявляются как ill-formed автоматически (Rocq компилирует и проверяет); хорошо сформированные системы — от арифметики до игр — проходят проверку. Это — систематический критерий, не зависящий от частных особенностей рассматриваемой структуры.

С разбором парадоксов как диагностической работы E/R/R мы завершаем содержательное разворачивание главы. Развёрнутая структура — запись Distinction, законы $L1$–$L5$, принципы $P1$–$P4$, E/R/R-устройство и иерархия уровней — становится основой для последующих глав, в которых формальный аппарат получит дополнительные технические уточнения и будет применён к более тонким вопросам метаматематики.

---

---

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

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

Навигация: ← Глава 3. Вывод законов логики из Distinction · Глава 5. Со-определение A и ¬ A →

Footnotes

1. Формализация четырёх принципов и их деривация от законов содержится в файле PrinciplesFromLaws.v репозитория ToS-Coq; файл опирается на Distinction.v, LawsFromDistinction.v и TheoryOfSystems_Core_ERR.v. ↩

2. Соответствующие теоремы файла — P1_concrete_L1_L2, P1_level_step, P1_asymmetry. ↩

3. Этот результат зафиксирован в теореме P1_blocks_russell. Подробное обсуждение связи с парадоксами — в «Парадоксы как смешение E/R/R-категорий». ↩

4. Соответствующая теорема в файле — four_principles_from_five_laws. Также присутствует теорема derivation_chain, явно указывающая закон-источник для каждого принципа: $P1$ от $L1+L5$; $P2$ от $L5$; $P3$ от $L1+L4$; $P4$ от $L5$. ↩

5. Файл ERRFromDistinction.v репозитория ToS-Coq. ↩

6. Прямая цитата из комментариев файла ERRFromDistinction.v. ↩

7. Соответствующие функции файла ERRFromDistinction.v — err_element_count, err_role_count, err_rule_count. Также присутствуют теоремы distinction_has_two_elements, distinction_has_two_roles, minimum_two_roles, доказывающие эти равенства. ↩

8. Случай, когда требуется акт оператора при отсутствии алгоритмического механизма подбора, тесно связан с Аксиомой Выбора в классической теории множеств. Подробное обсуждение — в Главе 6, где разбираются обе фундаментальные аксиомы репозитория ToS-Coq (classic и L4_witness) и их соотношение с принципом $P4$. ↩

9. Здесь мы для наглядности считаем натуральные числа начиная с $1$. Если работать с nat в Rocq, где натуральные начинаются с $0$, то уже $0^2<1$, и носитель при малых $c$ непуст; пример тогда удобнее брать с $c=0$, где условие $n^2<0$ не выполнено ни для какого $n$. ↩

10. Формальный аппарат — в файле FormationRules.v, опирающемся на тип System, поле sys_criterion (конкретный критерий системы), отношение HasType (типизация системы в контексте). Ключевые леммы — sys_form (правило формации системы), p1_check (проверка иерархии), l4_role_principle (проверка обоснованности ролей), wf4_check (общая проверка хорошей сформированности). ↩

11. Связь с Аксиомой Выбора в классической теории множеств: ситуация, когда из семейства непустых множеств требуется выбрать по элементу из каждого, не имея алгоритма для такого выбора. В ToS обе ситуации формально разделены: автоматический подбор реализуется через конструктивные конструкции Rocq, операторный — через аксиому L4_witness. Подробное обсуждение — в Главе 6. ↩

12. «Нетривиальная» — в смысле: не вырожденная в простейший акт различения. Простейший акт различения — предельный случай иерархии, в котором уровни не разворачиваются дальше; см. «Иерархия как разворачивание E/R/R». ↩

13. Подробное обсуждение Level как самостоятельной структуры — в Главе 6. Здесь нам достаточно его роли в формализации иерархии. ↩

14. Формально: индуктивное определение натуральных чисел через единицу и операцию прибавления единицы есть простейшая E/R/R-структура с двумя элементами на каждом шаге — <<уже построенное>> и <<следующее>>. ↩

15. Эта структура согласована с метафизическим выводом Тома I, где двойственность Структура/Наполнение возникает как $L4$ для $A=\exists$: для самого факта существования необходимо мета-устройство, в котором имеются обе роли. ↩

16. Подробное обсуждение критерия — в «Парадоксы как смешение E/R/R-категорий». ↩

17. Точные формулировки no_self_reference и rules_above_elements разбираются в «Парадоксы как смешение E/R/R-категорий». ↩

18. Формальный аппарат — в файлах ERRWellFormedness.v (критерий хорошей сформированности) и ParadoxDiagnosis.v (унифицированный разбор пяти парадоксов). Главная теорема all_paradoxes_ill_formed устанавливает, что все классические парадоксы — структурно ill-formed. ↩

19. Полная классификация $46$ классических парадоксов на три класса (структурные, дефектные, не-парадоксы) и подробный метод доменного анализа — в отдельной работе автора по диагностике парадоксов через архитектуру рассуждения. В настоящем разделе мы ограничиваемся структурными парадоксами, поскольку именно они напрямую разбираются через E/R/R-диагностику. ↩

20. В PrinciplesFromLaws.v («: иерархия») есть также отдельная теорема P1_blocks_russell, фиксирующая, что $P1$ блокирует конструкцию Рассела. ↩

21. Формально: $L\iff \neg L$. ↩

22. Теоремы cantor_is_ill_formed и buraliforti_is_ill_formed в файле ParadoxDiagnosis.v устанавливают ill-formed-статус обеих конструкций — через отображение paradox_system, в котором Кантору сопоставлена russell_system, а Бурали-Форти — grelling_system. ↩

23. Полный синтез — в теореме paradox_diagnosis_synthesis, объединяющей: (1) ill-formed-статус всех парадоксов; (2) контрапозитив well_formed_paradox_free; (3) точную классификацию нарушений для каждого парадокса. ↩

24. Это зафиксировано в ERRWellFormedness.v теоремой nat_well_formed: формальное представление натуральных чисел как ERRSystem проходит проверку is_well_formed. ↩

25. Теорема chess_well_formed. ↩