Глава 6. Аксиоматический минимум и механизм статуса

Слои формальной работы

Установка главы

Глава 5 завершилась наблюдением: формальная работа в ToS живёт на двух уровнях — на уровне Elements, где применяются операции к готовым определённостям, и на уровне Roles и Rules, где задаётся устройство, внутри которого определённости получают свои позиции. Эта двух-уровне-вая картина имеет конкретное техническое следствие, которое настоящая глава развёртывает: за работающим формальным аппаратом стоит небольшая, ясно обозримая совокупность утверждений, объявленных в репозитории как Axiom — то есть как утверждения, не имеющие доказательства внутри системы типов CIC.

Прежде чем разбирать каждое такое утверждение по отдельности, важно точно установить, чем оно в ToS является и чем не является. Это уточнение принципиально, потому что без него обсуждение техники легко принимается за обсуждение постулатов.

Что аксиомы ToS не есть. Аксиомы, объявленные в файле ToS_Axioms.v репозитория, не есть выбор автора. Они не есть «то, что мы решили принять вместо чего-то другого». Они не суть постулаты, конкурирующие с постулатами иных теорий — такими как аксиомы $\mathrm{ZFC}$ или аксиомы $\mathrm{NBG}$ — по принципу «эта система выбирает одни аксиомы, та — другие, выбор есть дело удобства или вкуса».

Что аксиомы ToS есть. Они — технические свидетельства того, что некоторые структурные факты, в ToS выводимые из устройства акта различения, в системе типов CIC не могут быть формально доказаны внутри неё. Они отмечают места, в которых онтологически первичные законы встречаются с конкретными особенностями реализующей платформы — и где для формальной проверки соответствующих утверждений требуется явное объявление в Coq.

Это — не философский нюанс, а точная техническая характеристика. Закон Исключённого Третьего ($L3$) онтологически следует из структуры акта различения и из законов $L1$, $L2$, разобранных в Главе 3. Но CIC, как формальная теория, по умолчанию конструктивна: в ней $L3$ не выводится как теорема для произвольной пропозиции $P$. Поэтому, чтобы работать в Coq с $L3$ в его классической форме, в репозитории объявлена аксиома classic. Это не выбор ToS принять $L3$ дополнительно; это регистрация в коде того, что онтологически выводимый $L3$ требует в CIC явного объявления. Содержательное обоснование $L3$ остаётся выводом из акта различения, а не постулатом.

Тот же характер имеет аксиома L4_witness, связанная с законом $L4$ (достаточное основание / самообоснование). Содержательно $L4$ выводится из устройства акта различения вместе с остальными законами; технически экстракция свидетеля из чистого экзистенциала в CIC не выводима без явного объявления; объявление и есть аксиома L4_witness.

Формально classic и L4_witness — настоящие аксиомы: в системе Rocq это утверждения, принимаемые проверяющей системой без доказательства, и L4_witness прямо объявлен через Axiom. Онтологически, однако, они не являются основаниями ToS: на месте каждой такой аксиомы стоит онтологически первичный закон ($L3$, $L4$), выводимый из устройства акта различения, а Axiom в коде есть способ зарегистрировать этот закон в среде CIC, которая иначе его не имеет. Кратко: формально — аксиоматический статус в CIC; онтологически — деривационный статус в ToS. Эту терминологическую пару мы будем держать на протяжении главы.

Три слоя формальной работы

С учётом сделанных уточнений формальная работа в репозитории ToS-Coq естественно расчленяется на три слоя.

Слой A: платформа CIC. Первый слой — то, что в Rocq доступно по факту реализации CIC как системы типов. Сюда входят:

• Индуктивные типы. Способ задавать новые типы через перечисление их конструкторов (как nat := O | S nat). Это — не аксиома, а правило формирования, встроенное в язык типов; принципы индукции (nat_ind и аналоги) автоматически выводятся для каждого объявленного индуктивного типа.
• Универсная иерархия. Тип Prop, тип Type${}_0$, Type${}_1$, и так далее — структурная иерархия, которая не позволяет типу содержать тип своего же уровня. Это — встроенное в CIC структурное соответствие принципу $P1$ (Глава 4); парадокс Рассела блокируется здесь ещё до того, как может быть записан.
• $\beta$-редукция, рекурсия, унификация. Вычислительная часть CIC: правила, по которым термы упрощаются, как проверяются равенства, как разворачиваются определения. Эти правила работают автоматически, без специальных аксиом.
• Тип Prop как универс пропозиций. В CIC тип Prop выделен особо: его обитатели — пропозиции (а не данные), и для них принят принцип пропозициональной иррелевантности доказательств в экстракциях, но не внутри самой теории. Это — структурное соглашение платформы, не отдельная аксиома.

Существенно, что выбор CIC как платформы реализации не случаен. CIC структурно поддерживает позицию ToS: иерархия универсов поддерживает $P1$, индуктивные типы поддерживают потенциальную (но не завершённую) бесконечность — что согласовано с $P4$ (Глава 4). Это — то, что позволяет в ToS-репозитории работать с минимальным числом явных объявлений: значительная часть содержательных требований ToS уже структурно встроена в CIC.

Слой B: технические свидетельства $L3$ и $L4$ в CIC. Второй слой — два утверждения, объявленные в файле ToS_Axioms.v репозитория¹ как Axiom. Их перечисление:

• classic — утверждение, что для всякой пропозиции $P$ верно $P\vee \neg P$. Содержательно — закон $L3$, выводимый в ToS из устройства акта различения (Глава 3, § 3.4). Технически — объявление, необходимое для работы с $L3$ в среде CIC, которая по умолчанию его не имеет.
• L4_witness — утверждение, что из существования $\exists x.P(x)$ можно извлечь конкретный элемент $x$ вместе с доказательством $P(x)$. Содержательно — формальный аппарат самообоснования по закону $L4$ (Глава 3, § 3.5). Технически — объявление, необходимое для конструктивного извлечения свидетеля в CIC.

Этот слой обсуждается подробно в § 6.2 (classic) и § 6.3 (L4_witness) настоящей главы. Сейчас существенно одно: сверх платформы CIC других Axiom-объявлений в ToS-Coq нет.

Слой C: определения и теоремы ToS. Третий слой — всё остальное содержание репозитория: запись Distinction, конструкция distinction_of, лемма co_constitution, $E/R/R$-структура (Глава 4), теоремы $L1$–$L5$ (Глава 3), теоремы $P1$–$P4$ (Глава 4), и работа последующих частей настоящего тома. Это — определения и доказанные утверждения; они не вводят новых аксиом, а работают на двух нижних слоях.

Всё содержание ToS-репозитория, выходящее за пределы платформы CIC, сводится логически к двум законам, требующим аксиоматической регистрации, — $L3$ и $L4$. Эти регистрации не суть постулаты-основания; они суть технические метки, отмечающие места встречи онтологически первичных законов с конкретной системой типов CIC. (Технически $L3$ в текущем репозитории зарегистрирован не в одном месте — см. § 6.2; это предмет синхронизации, не расширения аксиоматики.)

Терминологическое уточнение: $L4${L4} и L4_level

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

В книге $L4$ — это Закон Достаточного Основания, четвёртый из законов логики, разобранный в Главе 3 (§ 3.5). Содержательно: всякое утверждение требует основания, обеспечивающего его статус; в формальной части это закон самообоснования экземпляра Distinction через предъявление свидетеля.

В репозитории встречается также техническое обозначение L4_level в одном из основных файлов кода². Это — четвёртый уровень иерархии типов Level := L1 | LS Level, определяемый как LS (LS (LS L1)) — то есть как третий шаг наследования поверх базового уровня $L_1$. Этот объект относится к структуре $P1$-иерархии, не к закону логики.

Чтобы избежать смешения, в книге сохраняется следующее различение:

• $L4$ (заглавная жирная цифра с предшествующим L) — закон логики, четвёртый из пяти законов.
• L4_level (целиком в моноширинном начертании) — технический объект Coq, четвёртый уровень иерархии типов.

При первом появлении технического имени в книге всегда указывается явно, что речь о коде, а не о законе. Аксиома, разбираемая в § 6.3 ниже, — L4_witness — относится к закону $L4$, не к уровню L4_level; её имя содержит «L4» именно по связи с законом.

Аксиома, теорема, производный принцип

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

Аксиома в CIC — утверждение, объявленное директивой Axiom и принимаемое тайп-чекером без доказательства. Утверждение из аксиомы доступно во всех файлах, импортирующих модуль, в котором аксиома объявлена. С точки зрения проверителя кода аксиома есть запрос «прими это на веру». Содержательное обоснование аксиомы — отдельный вопрос; в ToS, как уже сказано, обе аксиомы имеют точное содержательное основание (выводимость $L3$ и $L4$ из устройства акта различения), при том что внутри CIC они объявлены как Axiom.

Теорема в CIC — утверждение, выводимое из ранее введённых определений, аксиом и других теорем через явное доказательство (тактиками или термами). Доказанная теорема автоматически проверяется тайп-чекером.

Производный принцип — утверждение, формально являющееся теоремой, но содержательно играющее роль, аналогичную аксиоме, и систематически применяемое в дальнейшей работе. В ToS такими производными являются, например, L3_informative и L4_definite в ToS_Axioms.v: они не объявлены как аксиомы, а доказаны из classic и L4_witness, но систематически используются в последующем коде.

Различение аксиомы, теоремы и производного принципа — единственная техническая категориальная разметка, нужная для оставшейся работы настоящей главы. С этими уточнениями переходим к разбору первой из двух аксиом — classic, технического свидетельства закона $L3$ в CIC.

classic: техническое свидетельство $L3$ в CIC

Объявление и источник

Утверждение, объявленное в файле ToS_Axioms.v как classic, имеет сигнатуру:

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

В словесном переводе: для всякой пропозиции $P$ верно либо $P$, либо $\neg P$. Это и есть классический Закон Исключённого Третьего.

В репозитории ToS classic не объявляется заново. В строке файла ToS_Axioms.v:

Require Export Coq.Logic.Classical_Prop.

{

импортируется и реэкспортируется стандартный модуль Classical_Prop библиотеки Rocq, в котором classic уже объявлен как Axiom. После этой строки утверждение classic доступно во всех файлах, которые импортируют ToS_Axioms. }

То, что classic берётся из стандартной библиотеки, не есть случайное обстоятельство: автор ToS-репозитория не изобретает свой вариант Закона Исключённого Третьего, а пользуется тем, что в платформе Rocq уже зафиксировано — сам факт, что для работы с классической логикой в CIC требуется явное объявление, существует в Rocq независимо от ToS.

Необходимо, впрочем, точное замечание о текущем состоянии репозитория. Логически в проекте два предполагаемых аксиоматических объявления — $L3$ и $L4$. Технически же $L3$ зарегистрирован не в одном месте: помимо реэкспорта из ToS_Axioms.v, в некоторых ранних foundation-файлах — в частности, в Distinction.v — $L3$ объявлен локально, прямой строкой Axiom classic : forall P : Prop, P \/ ~ P, с сопровождающим комментарием <<1 axiom (classic = L3)>>. Содержательно это тот же самый $L3$; но технически это отдельное локальное Axiom-объявление, не сведённое к центральному ToS_Axioms.v. Поэтому тезис <<всё сверх платформы CIC помещается в два объявления>> следует понимать логически (два закона — $L3$ и $L4$), а не как утверждение, что в коде ровно две физические строки Axiom. Это — место, которое в репозитории стоит синхронизировать: убрать локальное Axiom classic из Distinction.v и заменить его импортом ToS_Axioms, приведя проект к одному центру аксиом.

Почему CIC по умолчанию не имеет $L3$

Чтобы понять, почему classic приходится объявлять как Axiom (а не выводить как теорему), нужно ясно представлять конструктивный характер CIC.

В CIC доказательство пропозиции $P$ есть построение объекта типа $P$. Для пропозиции $P\vee Q$ построение есть указание, какая из двух сторон выбирается, и предъявление доказательства этой стороны: либо доказательство $P$, помещённое в левую ветвь, либо доказательство $Q$, помещённое в правую ветвь. В частном случае $P\vee \neg P$ правая ветвь есть доказательство $\neg P$, то есть функция $P\to \perp$.

Применительно к $P\vee \neg P$ это означает следующее. Чтобы конструктивно доказать $P\vee \neg P$ для произвольной пропозиции $P$, нужно для каждой такой $P$ либо построить доказательство $P$, либо построить функцию из $P$ в $\perp$. Но если $P$ — произвольная пропозиция, у нас нет общего способа сделать ни то, ни другое: какой именно $P$ нам предстоит обрабатывать, до получения конкретной $P$ неизвестно. Для всех $P$ одновременно построить указание левой или правой стороны конструктивно нельзя.

Пример структурной неразрешимости. Рассмотрим следующий класс пропозиций. Пусть $p$ — натуральное число, кодирующее программу (например, в смысле универсальной машины Тьюринга или эквивалентной модели), и пусть $x$ — натуральное число на входе этой программы. Пропозиция $H(p,x)$ — «программа $p$ останавливается на входе $x$» — это конкретное утверждение для каждой пары $(p,x)$.

Для отдельных конкретных $(p,x)$ значение $H(p,x)$ может быть известно: для одних программ остановка очевидна, для других — доказуемо невозможна. Однако общего алгоритма, разрешающего $H(p,x)$ для произвольной пары, не существует — это классический результат Тьюринга (проблема остановки структурно неразрешима). Это не утверждение о пределах наших нынешних знаний; это доказанный структурный факт об отсутствии общего разрешителя.

Соответственно, для произвольной пары $(p,x)$ конструктивно предъявить ни доказательство $H(p,x)$, ни доказательство $\neg H(p,x)$ в общем случае нельзя — не по эпистемической причине («мы пока не знаем»), а по структурной (общего конструктивного способа не существует). Тем не менее по $L3$ для каждой конкретной пары ровно одно из двух имеет место. Именно эта ситуация — когда $L3$ структурно верен, а конструктивно не выводим — и есть то, ради чего classic объявлен в ToS-репозитории.

Что CIC даёт без classic. CIC не запрещает $L3$ — она просто не выводит его как общую теорему. Если для конкретной пропозиции $P$ известно доказательство $P$ или доказательство $\neg P$, конструктивная система это принимает; если для $P$ доказана разрешимость (существование алгоритма, который для каждого случая отвечает, верно $P$ или нет) — это тоже не требует classic. classic становится нужен именно тогда, когда работа ведётся с произвольной пропозицией, для которой ни доказательство, ни отрицание, ни разрешимость заранее не известны.

Методологическое замечание. Объявление classic обеспечивает работу с $L3$ для произвольных пропозиций, но это не означает, что в ToS любое утверждение существования следует обосновывать через classic. Если речь идёт о существовании математического объекта — числа, функции, структуры, — предпочтительный путь не в том, чтобы перебирать кандидатов в надежде найти один, а в том, чтобы предъявить формулу построения, то есть процесс, который этот объект производит. Процесс на $N$ работает потенциально — по $P4$ $N$ есть индуктивное правило, разворачиваемое по шагам, а не завершённое множество; и существование объекта, заданного процессом, есть свойство процесса, не результат удачного перебора.

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

В CIC Закон Исключённого Третьего не запрещён. Он не выводится как общая теорема. Объявление classic как Axiom — это формальный способ ввести его в систему, сохранив при этом строгий контроль над тем, где именно он используется.

$L3$ как структурный закон акта различения

Тот факт, что CIC не выводит $L3$ как общую теорему, ничего не говорит о содержательном статусе $L3$. Это — ограничение формальной системы, не утверждение о структуре акта различения.

Содержательное обоснование $L3$ — в Главе 3, § 3.4. Кратко напомню структуру вывода. Акт различения по своей структуре тотален: когда $A$ выделяется от $\neg A$, всё, что не есть $A$, по этому самому акту относится к $\neg A$. Третьей области, не относящейся ни к $A$, ни к $\neg A$, в самом акте различения не оставлено. Если такая область возникает, это значит, что различение не было актом различения по $A$ — то есть произошло иное различение, или различение не состоялось.

В записи Distinction эта тотальность зафиксирована полем exhaustive : positive \\/ negative — которое требует доказательства, что одна из сторон имеет место. Это поле и есть формальное выражение $L3$ внутри Distinction; и именно оно требует classic при построении distinction_of P для произвольной пропозиции $P$.

Содержательный путь:

• тотальность акта различения;
• $L3$ как закон;
• поле exhaustive в записи Distinction;
• classic как Axiom в ToS_Axioms.v, потому что CIC по умолчанию $L3$ не выводит.

Технический путь:

• CIC конструктивна;
• $L3$ требует объявления;
• classic объявлен как Axiom;
• работа с Distinction становится возможной для произвольных пропозиций.

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

Производные принципы из classic

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

Двойное отрицание (NNPP_from_L3). Утверждение $\neg \neg P\to P$ — так называемое двойное отрицание — классически верно, но конструктивно не выводимо. В ToS-репозитории оно доказано:

Lemma NNPP_from_L3 : forall P : Prop, ~~P -> P.
Proof. intros P Hnn. destruct (classic P); [assumption | contradiction]. Qed.

Доказательство применяет classic к $P$, разбирает оба случая ($P$ верно — тогда $P$ есть искомое; $\neg P$ верно — тогда из $\neg \neg P$ и $\neg P$ получаем противоречие) и в каждом случае завершает доказательство.

Вычислительная версия (L3_informative). В CIC есть различие между пропозициональной дизъюнкцией $P\vee Q$ (тип Prop) и информативной дизъюнкцией $\{P\}+\{Q\}$ (тип Set или Type). Первая утверждает существование одного из случаев, вторая позволяет вычислительно различить, какой из случаев имеет место.

В ToS-репозитории доказано:

Lemma L3_informative : forall P : Prop, {P} + {~P}.

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

Здесь важно избежать неточности. L3_informative не требуется для конструкции distinction_of: как видно из файла Distinction.v, distinction_of $(P)$ живёт в Prop и для поля exhaustive использует только classic $P:P\vee \neg P$ — пропозициональную дизъюнкцию, а не информативную $\{P\}+\{\neg P\}$. L3_informative нужен в других местах — там, где требуется вычислительно различить ветвь, то есть совершить переход из пропозициональной дизъюнкции в информативную (из Prop в Type). Именно для такого перехода и нужны обе аксиомы; distinction_of такого перехода не делает.

Зафиксировав classic как первое из двух объявлений Axiom в ToS и его содержательную связь с законом $L3$, переходим к разбору второго объявления — L4_witness, технического свидетельства закона $L4$ в CIC.

L4_witness: техническое свидетельство $L4$ в CIC

Объявление

Второе из двух Axiom-объявлений ToS, разобранное в файле ToS_Axioms.v, имеет следующую сигнатуру:

Axiom L4_witness : forall (A : Type) (P : A -> Prop),
  (exists x, P x) -> {x : A | P x}.

В словесном переводе: для всякого типа $A$ и предиката $P:A\to Prop$, если существует элемент $x:A$, удовлетворяющий $P$, то этот элемент можно извлечь вместе с доказательством $P(x)$.

В отличие от classic, которая реэкспортируется из стандартной библиотеки Rocq, L4_witness объявляется в репозитории ToS-Coq непосредственно. В стандартной библиотеке Rocq имеются аналогичные конструкции, но в ToS-репозитории все они запрещены к импорту⁴. Причина запрета будет понятна по ходу настоящего раздела и подробно разобрана в § 6.4.

От exists к sig: что делает аксиома

Чтобы точно понять, что утверждает L4_witness, нужно ясно представлять различие двух родственных конструкций CIC — exists и sig.

Пропозициональное существование (exists). { Запись exists x, P x имеет тип Prop. Это — пропозиция, утверждающая, что какой-то $x$, удовлетворяющий $P$, есть. Здесь нужна точность. Доказательство exists x, P x в CIC обычно строится через конструктор ex_intro и содержит конкретный свидетель $x_0$. Но поскольку это доказательство живёт в Prop, на него действует ограничение элиминации: извлечь $x_0$ как вычислительное значение типа Type в общем случае нельзя. Поэтому неверно сказать, что пропозиция exists x, P x <<не несёт свидетеля>> — точнее сказать, что свидетель в её доказательстве есть, но в общем случае недоступен как вычислительное значение. Именно эта недоступность, а не отсутствие свидетеля, и составляет барьер. }

Информативное существование (sig). Запись $\{x:A\mid Px\}$ — сокращение для sig P — имеет тип Type. Это — пара из элемента $x_0:A$ и доказательства $P(x_0)$. Такая конструкция, в отличие от пропозициональной, даёт доступ к свидетелю: имея объект типа $\{x:A\mid Px\}$, можно вычислительно извлечь его первую компоненту и работать с ней дальше.

Барьер между Prop и Type. В CIC между этими двумя конструкциями есть структурный барьер. Имея доказательство exists x, P x (то есть объект типа Prop), в общем случае нельзя конструктивно построить из него объект типа $\{x:A\mid Px\}$ (типа Type). Барьер этот связан со singleton elimination — правилом CIC, которое в основном запрещает использовать пропозициональные объекты для построения информативных, чтобы сохранить независимость пропозиционального уровня от вычислительного.

Аксиома L4_witness в точности преодолевает этот барьер — она утверждает, что переход от пропозициональной формы $\exists x.P(x)$ к информативной форме $\{x:A\mid Px\}$ всегда возможен. Это и есть техническое содержание аксиомы.

Содержательное основание: определённость существования

Почему L4_witness соответствует именно закону $L4$ — требует точного содержательного разбора, поскольку технически это утверждение об извлечении свидетеля, а содержательно $L4$ (Глава 3, § 3.5) есть Закон Достаточного Основания. Связь этих двух формулировок такова.

Существование = определённость. В позиции ToS существование никогда не есть «бытие как туман». Существовать — значит быть отделённым от того, чего нет, то есть быть определённым. Это — содержание Тома I и содержание развёрнутого в Главе 3 закона $L4$. Когда мы утверждаем «существует $x$, удовлетворяющий $P$», мы утверждаем не расплывчатую возможность чего-то такого, а наличие определённого $x$, отличимого от всего остального.

Применительно к экзистенциалу $\exists x.P(x)$ это означает следующее: если этот экзистенциал верен, существующий $x$ есть какой-то конкретный $x$, не «облако возможностей». Тот факт, что в пропозициональной записи имя этого $x$ не показано, есть особенность записи, не структуры существования. Структурно $x$ определён; формально L4_witness даёт способ к этой определённости обратиться.

Самообоснование как смысл $L4$. В Главе 3 (§ 3.5) Закон Достаточного Основания был сформулирован через идею самообоснования: всякий акт различения предъявляет в себе основание собственной осуществимости — свидетеля, относительно которого различение состоялось. Для $\exists x.P(x)$ таким свидетелем является сам $x_0$, удовлетворяющий $P$: наличие $x_0$ и есть основание истинности экзистенциала.

Аксиома L4_witness в формальной части переводит это содержательное наблюдение в конструктивную форму: «есть основание — значит, есть к нему доступ». Если бы между экзистенциалом и его свидетелем стоял непреодолимый барьер, было бы возможно положение вещей, в котором утверждается существование без возможности обратиться к существующему. Такое положение противоречит позиции ToS, и L4_witness его формально исключает.

Извлечение свидетеля по L4_witness не есть акт выбора из множества возможных вариантов. Это — признание того, что существование всегда определённо. Свидетель не выбирается; он предъявляется как основание самого факта существования.

Различение с Аксиомой Выбора

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

Чем работает L4_witness. Берётся один экзистенциал $\exists x.P(x)$, и из него извлекается один свидетель. Никакого «выбора между альтернативами» здесь нет: для данного $P$ свидетель уже определён (структурно), и аксиома лишь даёт к нему конструктивный доступ. Это — локальная операция, относящаяся к одному конкретному экзистенциалу.

Чем работает Аксиома Выбора. Берётся семейство экзистенциалов $\{\exists x.P(i,x)\mid i\in I\}$, индексированное некоторым множеством $I$, и утверждается существование функции выбора $f:I\to A$, которая для каждого индекса $i$ предъявляет соответствующий свидетель. Это — глобальная операция, требующая согласованного выбора по всем индексам сразу, при том что для разных $i$ свидетели независимы.

Где различие. L4_witness говорит: «каждое отдельное существование определённо». Аксиома Выбора в её сет-теоретическом смысле говорит: «можно согласованно выбрать свидетелей для произвольно большого семейства существований одновременно». Первое — утверждение об определённости каждого существования по отдельности; второе — утверждение о возможности их одновременного сбора в функцию. Различие здесь структурное, категориальное: L4_witness извлекает свидетеля из одного экзистенциала, тогда как сет-теоретическая Аксиома Выбора утверждает функцию выбора для завершённого семейства множеств.

Техническая оговорка: choice-подобная сила. Здесь, однако, необходима честная техническая оговорка, без которой различение прозвучало бы сильнее, чем оно есть. Было бы неверно утверждать, что L4_witness <<не позволяет вывести Аксиому Выбора>> вообще. L4_witness объявлен как полиморфный принцип по Type:

$$‘L{4}_{w}itness‘:\forall (A:‘Type‘)(P:A\to Prop),(\exists x,Px)\to \{x:A\mid Px\}.$$

Из такой формы, если семейство существований дано как функция $\forall i:I,\exists x:A_i,P_{i}x$, выборочная функция строится: достаточно применить L4_witness под лямбдой по $i$ и взять первую проекцию. То есть как типо-теоретический принцип перехода из exists в sig L4_witness обладает choice-подобной силой — по существу это принцип неопределённой дескрипции (indefinite description).

Поэтому корректная формулировка такова. L4_witness не есть Аксиома Выбора в сет-теоретическом смысле выбора из завершённого семейства множеств — и именно эта, сет-теоретическая AC запрещается принципом $P4$ как завершённая бесконечность (§ 6.5). Но как полиморфный типо-теоретический принцип L4_witness имеет choice-подобную силу: при наличии семейства доказательств существования он позволяет определить функцию, выбирающую свидетеля в каждом индексе. В книге эти две вещи необходимо различать: не сет-теоретическую AC, несовместимую с $P4$, и типо-теоретическую силу L4_witness как принципа дескрипции. Что отделяет ToS от теорий с сет-теоретической AC — это не отсутствие choice-подобной силы на уровне типов, а отказ от завершённого семейства одновременных выборов.

Полный разбор иерархии классических аксиом и места L4_witness в ней — в § 6.4.

Производный принцип: L4_definite

Из L4_witness в репозитории выводится производный принцип L4_definite, относящийся к единственным экзистенциалам:

Lemma L4_definite : forall (A : Type) (P : A -> Prop),
  (exists! x, P x) -> {x : A | P x}.

Здесь $\exists !x.P(x)$ — стандартная запись «существует единственный $x$, удовлетворяющий $P$». Утверждение L4_definite извлекает этот единственный $x$ как информативное значение типа $\{x:A\mid Px\}$.

Содержательно L4_definite есть строго более слабая версия L4_witness: она требует не просто существования, а существования и единственности. Доказательство в репозитории сводит её к L4_witness тривиально — из $\exists !x.P(x)$ выделяется $\exists x.P(x)$, и применяется L4_witness.

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

Зафиксировав L4_witness как второе из двух Axiom-объявлений ToS, его содержательную связь с законом $L4$ и его принципиальное отличие от Аксиомы Выбора, переходим к точному формальному разбору иерархии классических аксиом, в которой L4_witness занимает строго определённое место.

Деривационная природа позиции ToS

Постулат и вывод

Перед тем как переходить к разбору структурных несовместимостей ToS с классическими аксиомами (§ 6.5), полезно зафиксировать саму природу позиции ToS относительно постулатов — природу, которая существенно отличается от природы классических аксиоматических оснований и которая определяет, как вообще следует понимать сравнение ToS с такими основаниями.

Постулативная позиция. В классических аксиоматических основаниях математики — от $\mathrm{ZFC}$ до $\mathrm{NBG}$ и далее — основной приём состоит в следующем. Выбирается набор утверждений — аксиом — и объявляется принятым. Этот набор фиксирует, что в системе считается истинным «по определению»; всё остальное содержание выводится из аксиом. Сами аксиомы при этом обосновываются вне системы — аргументами математического удобства, согласованности с интуицией, исторической традицией, объяснительной силой. Внутри системы аксиомы истинны просто потому, что они приняты.

В этой позиции принять одно или другое есть в существенном смысле выбор автора аксиоматизации. $\mathrm{ZFC}$ выбирает Аксиому Выбора; конструктивные системы её не выбирают; разные учёные могут предложить разные наборы, и спор о том, какой набор «правильнее», ведётся вне формальной системы — средствами содержательного убеждения.

Деривационная позиция. ToS работает на иной основе. Здесь не выбирается набор аксиом для последующего вывода всего остального. Здесь выводится всё — из единственного исходного факта: акт различения возможен, и его структура наблюдается. Из этой структуры выводятся пять Законов ($L1$–$L5$, Глава 3); из них — четыре Принципа ($P1$–$P4$, Глава 4); из них — $E/R/R$-разбор, конструкция Distinction, последующие части тома.

Технические объявления в ToS_Axioms.v — classic и L4_witness — не являются постулатами ToS. ToS как теория строит своё содержание не на наборе постулатов; её отправная точка — один структурный факт — акт различения возможен, — и из этого факта выводятся Законы $L1$–$L5$, Принципы $P1$–$P4$ и весь последующий аппарат. Что касается classic и L4_witness в репозитории — это, как уже было проговорено в § 6.1 и § 6.3, объявления, имеющие формально-аксиоматический статус в CIC и онтологически-деривационный статус в ToS: формально они — аксиомы платформы, онтологически — регистрация уже выведенных Законов $L3$ и $L4$.

Отправная точка ToS — один структурный факт: акт различения. Всё содержание ToS выводится из устройства этого факта. Объявления classic и L4_witness имеют формально-аксиоматический статус в CIC, но онтологически-деривационный статус в ToS: они регистрируют в коде уже выведенные Законы, а не служат основанием теории. Поэтому сравнение ToS с $\mathrm{ZFC}$ <<по тому, чьи аксиомы лучше>> некорректно: эти системы устроены по-разному — $\mathrm{ZFC}$ постулирует, ToS прослеживает деривацию из одного структурного факта.

Почему сравнение ToS с ZFC по силе аксиом некорректно

Естественно возникает вопрос о сравнении ToS с другими формальными системами. В классической proof-theory принято характеризовать систему дедуктивной силой её аксиом — тем, насколько обширное множество теорем из неё выводимо. Чем больше принято, тем сильнее система; чем меньше — тем слабее. По этой шкале $\mathrm{ZFC}$ сильнее систем без Аксиомы Выбора, а конструктивные системы без $L3$ — слабее $\mathrm{ZFC}$.

Возникает соблазн поместить ToS на эту шкалу. Соблазн обманчив, и понимание, почему он обманчив, даёт точное понимание позиции ToS.

Что значит «занять место на шкале силы». Поместить теорию на шкалу силы означает рассматривать её как набор постулатов, который сравнивается с другими наборами постулатов по объёму выводимого. Это применимо к $\mathrm{ZFC}$, к $\mathrm{NBG}$, к конструктивным системам — к системам, которые являются наборами постулатов и предлагают себя именно в этом качестве.

Почему ToS не является таким набором. ToS не предлагает себя как набор постулатов. Технические объявления classic и L4_witness в репозитории не характеризуют позицию ToS как «такую-то выбранную аксиоматизацию». Они отмечают точки, в которых уже выведенные в ToS Законы требуют технической регистрации в CIC — и не более.

Аксиомы $\mathrm{ZFC}$ обосновываются содержательно: предлагаются как удачное оформление интуитивных понятий множества и принадлежности. Технические объявления ToS обосновываются выводом: Закон Исключённого Третьего выводится из тотальности акта различения, Закон Достаточного Основания — из самообоснования различения. У этих двух способов обоснования различная природа.

Что было бы сравнением «по существу». По существу сравнивать ToS с $\mathrm{ZFC}$ означало бы спрашивать: выводит ли $\mathrm{ZFC}$ свои аксиомы из чего-либо, что в ToS выводит свои Законы? Ответ — $\mathrm{ZFC}$ не выводит свои аксиомы. Они приняты. Сравнение по дедуктивной силе сохраняет смысл при сопоставлении двух наборов постулатов; для ToS, в которой никакого «набора постулатов» нет, такое сравнение оказывается переводом с одного языка — деривационного — на чужой — постулативный.

Сравнение ToS с $\mathrm{ZFC}$ по «силе» возможно технически, но теряет смысл методологически. Можно подсчитать, что classic плюс L4_witness дедуктивно слабее, чем $\mathrm{ZFC}$ с её Аксиомой Выбора. Но этот подсчёт никак не отражает того, что в ToS classic и L4_witness не суть аксиоматика, выбранная в качестве альтернативы аксиомам $\mathrm{ZFC}$. Они суть технические свидетельства уже выведенных в ToS Законов, регистрирующие эти Законы в CIC; собственная аксиоматика как основание ToS не имеет.

Что значит «сила» в позиции ToS

Если сравнение по объёму принятого ToS не применимо, возникает встречный вопрос: чем характеризуется сила позиции ToS? Что делает её работающей формальной системой, а не просто менее постулативной версией классики?

Ответ — в точности вывода. Сила ToS не в объёме принятого, а в плотности деривационной связи между исходным фактом и каждым последующим утверждением. Каждый Закон логики выводится из структуры акта различения через шаги, разобранные в Главе 3. Каждый Принцип — из Законов через шаги, разобранные в Главе 4. Запись Distinction — из требований к фиксации акта различения. co_constitution — из совместного определения сторон. И так далее.

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

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

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

Конструкции ToS и их соотношение с классическими объектами

Установка раздела

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

Однако в современной математической практике используется ряд классических конструкций — Аксиома Выбора, Аксиома Бесконечности, завершённые бесконечные множества, импредикативные определения — которые принимаются в основаниях вроде $\mathrm{ZFC}$ и заметно формируют облик современной математики. Поскольку ToS претендует на работающий формальный аппарат, естественно спросить: что из этой классики обнаруживается в ToS, а что — нет?

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

Конструкции, выведенные в ToS

Перечислю основные конструкции, получаемые в ToS как следствия устройства акта различения — без обращения к классической аксиоматике.

Процессная бесконечность. Из принципа $P4$ (Глава 4) следует, что бесконечность в ToS есть процесс, не объект. Натуральные числа задаются как индуктивный тип $N:=O\mid SN$: каждое отдельное число конечно и получено конечным числом применений конструктора $S$; для всякого уже полученного числа существует следующее. Бесконечность работает потенциально — как возможность разворачивания, не как готовая совокупность всех чисел сразу.⁵

Механизм выбора через $L5$. Закон $L5$ (Глава 3, § 3.6) задаёт онтологический приоритет: иерархически старшее имеет преимущество перед младшим. В формальном аппарате это превращается в механизм выбора по онтологическому старшинству, соблюдающий иерархию: для непустого конечного списка $L5$ определяет, какой элемент имеет статус «первого». Извлечение элемента из непустого списка — операция, заложенная в саму конструкцию: $L5$ не выбирает между равноправными альтернативами, а реализует онтологический порядок, заложенный в структуре.⁶

Стратификация уровней. Принцип $P1$ (Глава 4) задаёт иерархию уровней: $L1$, LS L1, LS (LS L1) и так далее. Объекты различены по уровням; объект уровня $L$ не может содержать объекты того же уровня. Эта стратификация встроена в систему типов CIC через универсную иерархию ($Prop$, $‘Type{‘}_0$, $‘Type{‘}_1$, $\dots$); содержательно она выражает структурное следствие акта различения — невозможность самовключения, разобранную в Главе 4.

$E/R/R$-структура. Из устройства различения, развёрнутого в Главе 4, выводится разделение ролей и правил формирования: всякая система имеет уровень элементов (Elements), уровень ролей (Roles) и уровень правил (Rules). Это разделение работает и в формальной части как структурный принцип организации: { ролям соответствуют типы, правилам — зависимости между типами, элементам — значения.} Подробный разбор $E/R/R$-механизма для случая выбора — в § 6.6 ниже.

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

Этот способ задания не есть выбор реализации; он есть прямое следствие $P4$: всё актуально предъявленное конечно, и любое определение объекта работает через эту актуальную конечность.

Перечисленные конструкции — процессная бесконечность, $L5$-механизм, стратификация уровней, $E/R/R$, индуктивные определения — получены в ToS из устройства акта различения. Они существуют самостоятельно, не как ответ на классические аксиомы, а как следствия вывода. Дальнейший разбор — что из классической математики оказывается воспроизводимым в этих конструкциях, а что нет — есть наблюдение результата, не пересмотр самих конструкций.

Что из классических объектов воспроизводится

Часть классических конструкций находит в ToS полный или близкий аналог.

Натуральные числа. Классическое понятие «множества натуральных чисел» отчасти воспроизводится: каждое отдельное число доступно в ToS как элемент индуктивного типа $N$; вся арифметика первого порядка работает. Что не воспроизводится — понимание $N$ как готовой совокупности всех натуральных чисел; об этом ниже.

Конечная арифметика и комбинаторика. Все конечные операции — сложение, умножение, факториал, конечные суммы, конечные произведения — работают полностью. Файл P4_Eliminates_Infinity.v содержит конкретные примеры: factorial(5) = 120, конечные частичные суммы и т. п.

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

Индукция как принцип доказательства. Принцип индукции по натуральным числам nat_ind автоматически выводится для индуктивного типа $N$ — это стандартная особенность CIC. Доказательства по индукции работают в ToS точно так же, как в классической арифметике: для базы и шага — и затем утверждение распространяется на все натуральные числа.

Конструктивные конкретные ординалы. Принцип, в обратной математике называемый «Арифметической Трансфинитной Рекурсией» (${\mathrm{ATR}}_0$), мотивирует в ToS конструкцию трансфинитной итерации через Fixpoint-определения на индуктивном типе ординалов Ord := OZero | OSucc Ord | OLim (nat -> Ord). Здесь нужна точность. Файл репозитория⁷ показывает, что определённые схемы трансфинитной итерации могут быть реализованы как структурная рекурсия по индуктивному типу ординалов, принимаемая средствами CIC без отдельной аксиомы. Это — $P4$-версия мотива ${\mathrm{ATR}}_0$, а не доказательство того, что вся классическая система ${\mathrm{ATR}}_0$ из обратной математики целиком сведена к определению: такого доказательства файл не содержит и на него не претендует. Сказанное точно: трансфинитная итерация по конкретному индуктивному типу ординалов конструктивна; полная эквивалентность с ${\mathrm{ATR}}_0$ — вопрос, выходящий за рамки этого файла.

Квантификация над функциями второго порядка. В обратной математике принцип ${\Pi }_1^1$-Comprehension утверждает существование множеств, выделяемых ${\Pi }_1^1$-формулами (квантификация над функциями $N\to N$). В ToS вводится $P4$-ограниченная, вычислимая версия такой квантификации: функция рассматривается как процесс-программа, кодируемая натуральным числом, и <<квантификация над всеми функциями>> заменяется квантификацией над кодами программ⁸. Это даёт арифметический аналог соответствующих рассуждений, но не является буквальным воспроизведением классической ${\Pi }_1^1$-Comprehension над всеми функциями $N\to N$: утверждение, что всякая функция $N\to N$ есть программа, файлом не доказывается — редукция встроена в определение $P4$-квантификации. Точная формула: ToS заменяет квантификацию над всеми функциями её $P4$-вычислимой версией, и в этой версии ${\Pi }_1^1$-мотив становится арифметическим.

Что из классических объектов не воспроизводится

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

Завершённая бесконечность как готовый объект. В классической математике постулируется существование некоторого бесконечного множества целиком — как объекта, доступного для оперирования: «множество всех натуральных чисел существует». Это постулирование оформлено в $\mathrm{ZFC}$ Аксиомой Бесконечности.

В ToS бесконечность есть процесс. Утверждение «все натуральные числа существуют как готовый объект» означало бы наличие предиката, истинного для всех $n:N$ одновременно актуально — то есть актуальную бесконечную тотальность предъявленного. Это вступает в противоречие с $P4$. Здесь, однако, нужна точность относительно формы, в которой противоречие доказано. Файл репозитория⁹ доказывает противоречие при наличии трёх посылок: завершённого бесконечного множества (CompletedInfSet), $P4$-ограниченности актуальности на каждой стадии (P4_stage_bounded) и моста (bridge), переводящего членство в завершённом множестве в актуальную предъявленность на стадии 0. То есть формальная теорема такова: завершённая бесконечность противоречит $P4$ при наличии моста, связывающего членство с актуальностью на стадии. Философская интерпретация ToS шире — завершённая бесконечность как готовый объект отвергается принципиально; но Rocq-теорема имеет именно условную форму, и приписывать коду безусловный запрет <<любой completed infinity>> не следует.

Аксиома Выбора в полной формулировке. Аксиома Выбора утверждает существование функции выбора $f:I\to A$ для произвольно большого индексного семейства экзистенциалов. Если $I$ потенциально бесконечно, такая функция как объект означает одновременное удержание бесконечно многих значений — то есть завершённую бесконечность. По уже разобранной причине это в ToS не строится: наличие функции выбора $f:N\to N$ производит граф $\{(n,f(n))\mid n\in N\}$ — завершённый бесконечный объект, несовместимый с $P4$.¹⁰

Работа, для которой в классической математике требуется Аксиома Выбора, в ToS выполняется $L5$-механизмом — но только для конечных семейств. Случай бесконечных семейств не имеет в ToS аналога по принципиальной причине: одновременный выбор по бесконечно многим независимым местам структурно несовместим с процессной природой бесконечности.

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

В ToS обе предпосылки отсутствуют. Первая блокирована $P1$: иерархия уровней (Глава 4) не допускает самовключения, объект уровня $L$ не может содержать объекты того же уровня. Вторая блокирована $P4$: завершённой тотальности всех объектов в ToS не существует.

Парадокс Рассела в ToS не есть «избегнутый парадокс» — его попросту невозможно сформулировать. Конструкция, на которой он строится, не имеет места в системе.¹¹

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

Стандартная библиотека Rocq: какие модули не используются

В стандартной библиотеке Rocq содержится ряд модулей, реализующих классические конструкции, оказавшиеся невозможными в ToS:

• Coq.Logic.ClassicalDescription — определение объекта через свойство, с опорой на Аксиому Выбора.
• Coq.Logic.ClassicalEpsilon — гильбертовский $ϵ$-оператор, выбирающий произвольного свидетеля, с опорой на Аксиому Выбора.
• Coq.Logic.IndefiniteDescription — неопределённое описание, ещё одна форма выбора.

В ToS-репозитории эти модули не импортируются. Это не есть запрет в смысле волевого акта — это естественное следствие того, что данные модули привносят в CIC то, чего в ToS нет (Аксиома Выбора и её варианты). Если бы они были импортированы, в репозитории появилась бы конструкция, не имеющая основания в выводе из акта различения. В комментарии файла ToS_Axioms.v соответствующие модули явно отмечены как не используемые — эта отметка есть техническое напоминание, не дополнительное правило.

Зафиксировав соотношение конструкций ToS с классическим материалом — что из классики воспроизводимо, что нет и почему именно так, — переходим к подробному разбору центрального аппарата, выполняющего в ToS работу Аксиомы Выбора без её принятия. Этот аппарат — механизм передачи статуса через структуру $E/R/R$ — разворачивается в § 6.6.

Статус, роль, передача: механизм через $E/R/R$

Установка раздела

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

Существенно: то, что разбирается ниже, не есть «ослабленная Аксиома Выбора» или «локальная её версия». Это — другая конструкция, получающаяся непосредственно из устройства $E/R/R$ и Законов $L1$–$L5$. Она работает не через выбор между альтернативами, а через присвоение статуса в структурированном процессе.

Постановка: элемент, число, статус

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

С онтологической стороны существенно различение трёх вещей, без которого дальнейший разбор был бы неточен.

Позиция, элемент, число. В разворачивающемся процессе различаются три вещи. Позиция — место в разворачивании: первое, второе, третье и так далее. Элемент — то, что эту позицию занимает, входя в процесс. Число — значение элемента. Это — не одно и то же: элемент не есть позиция, он её занимает; и элемент не есть число, он его несёт как своё значение. Когда говорится «второй элемент есть число $3$», имеется в виду: элемент, занявший вторую позицию, несёт значение — число $3$.

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

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

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

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

Правила

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

Правило 1: превосходит ли число текущего элемента действующий максимум? Вопрос требует основания для положительного ответа. Таким основанием служит строгое превосходство: если число текущего элемента строго больше действующего максимума, основание есть. Это — $L4$ (Закон Достаточного Основания): строгое превосходство и есть достаточное основание для того, чтобы текущему элементу был присвоен статус максимума, а прежний носитель этого статуса его потерял.

Если строгого превосходства нет, Правило 1 положительного ответа не даёт, и процесс переходит к Правилу 2.

Правило 2: равно ли число текущего элемента действующему максимуму? Если число текущего элемента равно действующему максимуму, текущий элемент получает статус повторного максимума. Если же число меньше действующего максимума, текущий элемент статуса максимума или повторного максимума не получает.

Два правила исчерпывают возможные исходы шага. Правило 1 отвечает на вопрос о передаче статуса максимума и опирается на $L4$. Правило 2 отвечает на вопрос о повторе максимума. Случай, когда число текущего элемента меньше действующего максимума, — это просто отсутствие положительного ответа на оба правила; статус действующего максимума при этом не меняется, и менять его не требует никакого отдельного закона — нет основания для изменения.

Роли: базовые и статусные

Роли в ToS разделяются на два класса, и для разбираемого механизма это различение существенно.

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

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

• Максимум — статус, присваиваемый по положительному ответу на Правило 1. На каждой стадии процесса этот статус несёт ровно один элемент — тот, число которого на текущий момент строго превзошло числа всех прежних. При срабатывании Правила 1 статус передаётся: прежний носитель его теряет, новый получает.
• Повторный максимум — статус, присваиваемый по положительному ответу на Правило 2. Повторных максимумов в процессе может быть несколько — по одному на каждый шаг, на котором сработало Правило 2. Они образуют список — но список этот не дан заранее как готовый объект: он создаётся и пополняется в ходе процесса, по одной позиции на каждое срабатывание Правила 2. На любой стадии список повторных максимумов существует актуально ровно в том объёме, в каком процесс уже прошёл — в полном согласии с $P4$: это процесс, не завершённый объект.

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

Где $L4$ и где $L5$

Прежде чем разбирать пример, зафиксируем точно, какой Закон где работает.

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

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

Именно $L5$ делает возможным само устройство процесса. Без порядка разворачивания не было бы «действующего» максимума, с которым сравнивается число «текущего» элемента; не было бы «очередной позиции» в списке повторных максимумов. Список повторных максимумов пополняется упорядоченно — каждый новый повторный максимум занимает следующую позицию — именно потому, что $L5$ как Закон Порядка производит порядок, в котором процесс разворачивается.

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

Полный разбор на примере

Применим аппарат к конкретной последовательности значений: $1,3,2,5,4,5,7,7$.

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

Шаг 1: первый элемент, число $1$. Первый акт разворачивания. В процесс входит первый элемент, заполняя базовую роль; значение этого элемента — число $1$. Действующего максимума до сих пор не было, и сравнивать не с чем: первый элемент принимает статус максимума как стартовый. Действующий максимум: $1$. Список повторных максимумов: пуст.

Шаг 2: второй элемент, число $3$. В процесс входит второй элемент; его значение — число $3$. Правило 1: $3>1$ — строгое превосходство. $L4$ даёт основание. Статус максимума передаётся второму элементу. Действующий максимум: $3$. Список повторных: пуст.

Шаг 3: третий элемент, число $2$. Значение третьего элемента — $2$. Правило 1: $2>3$? Нет. Правило 2: $2=3$? Нет. Ни одно правило не дало положительного ответа. Третий элемент заполняет базовую роль (потому он и в процессе), но статусной роли не получает. Действующий максимум остаётся $3$ — основания для изменения нет. Список повторных: пуст.

Шаг 4: четвёртый элемент, число $5$. Правило 1: $5>3$. $L4$ даёт основание. Статус максимума — у четвёртого элемента. Действующий максимум: $5$. Список повторных: пуст.

Шаг 5: пятый элемент, число $4$. Правило 1: $4>5$? Нет. Правило 2: $4=5$? Нет. Пятый элемент статусной роли не получает. Действующий максимум остаётся $5$. Список повторных: пуст.

Шаг 6: шестой элемент, число $5$. Это — ключевой шаг примера. Значение шестого элемента — $5$. Существенно: это другой элемент, нежели четвёртый, хотя значение у них одно. Правило 1: $5>5$? Нет — $L4$ требует строгого превосходства, равенство его не даёт. Правило 2: $5=5$? Да. Шестой элемент получает статусную роль повторного максимума. Действующий максимум остаётся прежним: $5$ (значение четвёртого элемента). Список повторных максимумов — то есть повторов действующего максимума — пополняется: в нём появляется первая позиция, и её занимает шестой элемент.

Шаг 7: седьмой элемент, число $7$. Правило 1: $7>5$. $L4$ даёт основание. Статус максимума — у седьмого элемента. Действующий максимум: $7$. При смене действующего максимума список повторных, относившийся к прежнему максимуму $5$, более не действует: повторы значения $5$ не суть повторы нового действующего максимума. Список повторных максимумов снова пуст — повторов значения $7$ ещё не было.

Шаг 8: восьмой элемент, число $7$. Значение восьмого элемента — $7$; это другой элемент, нежели седьмой. Правило 1: $7>7$? Нет. Правило 2: $7=7$? Да. Восьмой элемент получает статусную роль повторного максимума. Действующий максимум остаётся $7$. Список повторных максимумов (для действующего максимума $7$) пополняется: первую позицию занимает восьмой элемент.

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

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

Это — прямое проявление $P4$: нет «итогового состояния системы» как готового объекта, существующего помимо процесса. Есть состояние на каждой стадии — какой элемент несёт статус максимума, какие элементы несут статус повторного максимума, — и это состояние меняется от шага к шагу. Механизм статуса позволяет проследить эти изменения шаг за шагом, и сама прослеживаемость есть следствие процессного, а не объектного устройства ToS.

В процессе не было ни одного акта выбора между равноправными вариантами. На каждом шаге задавались два правила; ответ на них — по $L4$ для Правила 1 — определял исход однозначно. $L5$ не участвовал в отдельных шагах как операция — он производил сам порядок прохождения, благодаря которому на каждом шаге был определён «действующий» максимум, «текущий» элемент и «очередная» позиция в списке повторных.

Почему это не Аксиома Выбора

Постановка задачи может напомнить классическую: «дано непустое множество, выберите элемент». В этой постановке Аксиома Выбора утверждает возможность выбора по произвольному принципу. В разобранном выше механизме статуса нет ни «множества», ни «выбора» в этом смысле.

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

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

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

Формальная регистрация механизма

Здесь необходима точность относительно того, что в репозитории формализовано, а что — пока нет.

В репозитории формализован более простой механизм, чем полный механизм статуса, разобранный в § 6.6. А именно: разрешение непустого списка по порядку — лемма l5_res_rule в файле src/FormationRules.v¹³ — и выбор первого элемента — функция L5_choose в файле src/foundation/P4_Eliminates_AC.v. Эти конструкции формализуют, что при наличии порядка над элементами и непустого списка процесс, разворачиваемый по $L5$, всегда приходит к определённому результату.

Полный механизм статуса, описанный в § 6.6, — с состоянием вида <<действующий максимум плюс список повторных максимумов>>, с шаг-функцией, со сбросом повторов при смене максимума — в текущем репозитории отдельным файлом-автоматом не формализован. Его пока следует понимать как содержательную схему: точное описание того, как устроен процесс присвоения статуса, которое может быть формализовано отдельным файлом конечного автомата (с записью состояния, шаг-функцией и теоремами о единственности статуса максимума на каждой стадии и о сбросе повторов). Разобранная по шагам последовательность $1,3,2,5,4,5,7,7$ — точная иллюстрация этой схемы; но машинно-проверенной регистрацией всего механизма она пока не подкреплена.

Замечание о двух файлах: AC_is_L5 и запрет AC. Отдельно отметим место, требующее аккуратности — и, по-видимому, синхронизации в самом репозитории. Файл P4_Eliminates_AC.v содержит теорему AC_is_L5 (и равную ей P4_eliminates_AC):

$$\forall (\ast family\ast :\mathbb{N}\to ‘listnat‘),(\forall i,\ast family\ast i\ne [])\to \exists f,\forall i,fi\in \ast family\ast i,$$

то есть выбор по $\mathbb{N}$-индексированному семейству непустых списков — индекс $i$ пробегает весь $\mathbb{N}$, без конечного ограничения. Файл же P4ProhibitsAC.v определяет AC_on_nat с той же сигнатурой ($\mathbb{N}\to ‘listnat‘$) и доказывает, что она влечёт завершённую бесконечность и потому несовместима с $P4$. Получается видимое напряжение: одна теорема подаёт $\mathbb{N}$-индексированный выбор как конструктивный <<$L5$>>, другая — как запрещённый $P4$. Конструктивно бесспорна лишь конечная версия — finite_choice с явным конечным индексом $n<N$, и она действительно есть в обоих файлах. Корректная позиция для книги такова: конечный выбор (по списку, по конечному индексу) — конструктивен и совместим с $P4$; процессный выбор по стадиям совместим с $P4$ лишь будучи представлен как стадийная функция, а не как завершённый граф; а $\mathbb{N}$-индексированная теорема AC_is_L5 в её текущей форме — место, которое в репозитории стоит развести с P4ProhibitsAC.v (ограничив AC_is_L5 конечным индексом либо явно пометив её как утверждение о стадийной, а не завершённой функции). До такой синхронизации книга не должна подавать конфликт $P4$ и AC как уже полностью формально разведённый.

Зафиксировав механизм статуса через $E/R/R$ как конструкцию, выполняющую в ToS работу Аксиомы Выбора без её принятия, перейдём к заключительным разделам главы — разбору того, что в CIC встроено структурно и не требует объявлений (§ 6.7), и разбору различия онтологических Законов и технических аксиом (§ 6.8).

Что в CIC встроено структурно

Установка: третий слой

В § 6.1 формальная работа ToS была расчленена на три слоя: платформа CIC (слой A), два технических объявления classic и L4_witness (слой B), определения и теоремы ToS (слой C). Разделы § 6.2–6.6 разобрали слой B и часть слоя C. Настоящий раздел возвращается к слою A — к платформе.

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

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

Универсная иерархия и $P1$

Первое, что встроено в CIC структурно, — иерархия универсов.

В CIC всякий тип сам имеет тип. Тип Prop (универс пропозиций) и тип Set имеют тип Type${}_0$; Type${}_0$ имеет тип Type${}_1$; и так далее — вверх по бесконечной (в потенциальном смысле) иерархии. Существенное свойство этой иерархии: универс не содержит сам себя. Не существует типа, который был бы обитателем самого себя; Type${}_n$ всегда обитает в строго более высоком Type${}_{n+1}$.

Это устройство есть структурное соответствие принципу $P1$ (Глава 4): иерархия уровней, в которой объект не может содержать объект своего же уровня или себя самого. CIC реализует $P1$ не как объявленную аксиому, а как встроенное правило формирования типов: попытка записать тип, обитающий в себе, не проходит проверку типов — такое выражение в CIC просто не является правильно сформированным.

Следствие: парадокс Рассела невыразим. Как уже отмечалось в § 6.5, парадокс Рассела в ToS невозможно даже сформулировать. Теперь видно, на каком уровне это блокируется. «Множество всех множеств, не содержащих себя» требует объекта, способного содержать объекты своего уровня (включая, возможно, себя). В CIC такой объект нельзя записать: универсная иерархия не даёт выразить «множество всех множеств» как объект, обитающий на одном уровне со своими элементами. Парадокс блокируется не аксиомой и не проверкой постфактум — он блокируется тем, что соответствующее выражение не является правильно сформированным типом.

В репозитории иерархия уровней ToS¹⁴ строится поверх универсной иерархии CIC: формальная иерархия типов ToS опирается на ту, что в CIC уже есть.

Индуктивные типы и $P4$

Второе встроенное свойство — механизм индуктивных типов.

В CIC новый тип может быть задан перечислением его конструкторов. Стандартный пример — натуральные числа: nat задаётся двумя конструкторами — O (ноль) и S (переход к следующему). Всякий обитатель nat есть результат конечного числа применений конструкторов: O, S O, S (S O) и так далее. Бесконечного обитателя — полученного бесконечным числом применений S — в nat нет.

Это устройство есть структурное соответствие принципу $P4$ (Глава 4): актуально предъявленное конечно, бесконечность работает потенциально. Индуктивный тип nat даёт ровно это: каждое отдельное число конечно (получено конечным числом шагов), и при этом для всякого числа есть следующее (конструктор S применим всегда). Здесь нужна точность. nat в CIC является индуктивным типом и потому объектом языка — по нему можно квантифицировать (forall n : nat, …); неверно было бы сказать, что <<в CIC нет типа всех натуральных чисел>>. Тип nat есть. Вопрос в том, как ToS читает этот тип: не как завершённое множество в сет-теоретическом смысле — как собранную целиком тотальность, — а как правило порождения, по которому каждый обитатель получается конечным числом применений конструктора. CIC не вынуждает читать nat как завершённую бесконечную совокупность; ToS пользуется этой свободой и читает его процессно. Различие здесь не в наличии или отсутствии типа nat, а в его интерпретации.

Принцип индукции выводится автоматически. Для каждого объявленного индуктивного типа CIC автоматически строит соответствующий принцип индукции — для nat это nat_ind. Этот принцип не объявляется как аксиома: он есть прямое следствие того, как устроен индуктивный тип. Доказательства по индукции в ToS опираются на эти автоматически построенные принципы, не на отдельные объявления.

Вычисление как встроенное правило

Третье встроенное свойство — вычислительная семантика CIC.

Термы CIC не статичны: они вычисляются. Применение функции к аргументу упрощается ($\beta$-редукция); определения разворачиваются; выражения над конструкторами вычисляются до результата. Равенство двух термов в CIC проверяется в том числе вычислением: если два выражения сводятся к одному и тому же, они равны по определению, без всякого доказательства.

Эта вычислительная часть — не аксиома и не объявление. Она есть встроенное правило системы типов: CIC по построению есть не только язык записи утверждений, но и язык вычислений. Когда в ToS проверяется, что factorial 5 равно 120, это проверяется вычислением — система разворачивает определение факториала и считает; никакой аксиомы для этого не требуется.

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

Почему созвучие платформы не есть доказательство позиции

Разобранные встроенные свойства CIC — универсная иерархия, индуктивные типы, вычислительная семантика — структурно созвучны принципам ToS: $P1$, $P4$, процессной онтологии. Возникает искушение усилить это наблюдение до утверждения: «CIC доказывает позицию ToS» или «CIC подтверждает истинность ToS». Такое усиление было бы методологической ошибкой, и важно понять, почему.

CIC есть среда реализации. Тот факт, что ToS реализуема в CIC без насилия над платформой — что принципы ToS ложатся на устройство CIC естественно, а не вопреки ему, — есть свидетельство реализуемости ToS, не истинности её исходного структурного факта. Истинность позиции ToS обосновывается выводом из акта различения (Главы 1–4), не созвучием с какой-либо платформой.

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

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

Этот итог подводит к последнему содержательному вопросу главы. Если classic и L4_witness — технические объявления, а не онтологические основания; если встроенные свойства CIC — среда реализации, а не аксиомы ToS; то в чём именно состоит онтологический статус Законов $L1$–$L5$, и чем он отличается от статуса всего технического? Этому различению — онтологических Законов и технических аксиом — посвящён заключительный раздел главы.

Онтологические Законы и технические аксиомы

Два рода присутствующего в формальной работе

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

Онтологические Законы. Первый род — Законы $L1$–$L5$ (Глава 3) и Принципы $P1$–$P4$ (Глава 4). Они выведены из устройства акта различения. Их обоснование — деривация: каждый из них получен цепочкой шагов из единственного структурного факта. Они не зависят от того, на какой платформе ведётся формальная работа: Закон Тождества или Закон Достаточного Основания есть то, что он есть, безотносительно к тому, реализуется ли ToS в CIC, в иной системе типов или вообще без формализации.

Технические аксиомы. Второй род — объявления classic и L4_witness в файле ToS_Axioms.v. Они не выведены внутри CIC — они объявлены директивой Axiom. Их наличие обусловлено конкретным обстоятельством: CIC по умолчанию конструктивна и не выводит $L3$ и аппарат извлечения свидетеля как теоремы. Технические аксиомы суть регистрация в коде уже выведенных Законов $L3$ и $L4$ — регистрация, необходимая именно потому, что платформа CIC устроена определённым образом.

Онтологический Закон и техническая аксиома — разные роды. Закон выведен из акта различения и от платформы не зависит. Техническая аксиома есть объявление, обусловленное устройством конкретной платформы. На месте classic и L4_witness стоят онтологически первичные Законы $L3$ и $L4$; сами эти объявления — лишь форма, в которой Законы регистрируются в CIC.

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

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

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

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

Применение критерия. Закон $L3$ (Исключённого Третьего) инвариантен: он выведен из тотальности акта различения (Глава 3) и остаётся тем же, в какой бы системе ни велась формализация. Объявление classic зависит от платформы: оно существует потому, что CIC конструктивна. В системе типов, где Исключённое Третье встроено, объявление classic было бы не нужно — а Закон $L3$ остался бы ровно тем же.

Аналогично: $L4$ (Достаточного Основания) инвариантен; объявление L4_witness зависит от того, что CIC не выводит извлечение свидетеля конструктивно.

Мысленный эксперимент: смена платформы

Критерий инвариантности проясняется мысленным экспериментом.

Представим, что ToS формализуется не в CIC, а в некоторой иной системе типов — такой, в которой Исключённое Третье встроено (то есть $P\vee \neg P$ выводится как теорема для любой пропозиции). В такой системе объявление classic не понадобилось бы: то, что оно регистрирует, платформа давала бы сама.

Что изменилось бы в ToS при таком переносе? Из технического слоя — одно объявление исчезло бы (classic стало бы не нужно). Из онтологического слоя — ничего. Закон $L3$ как был выведен из тотальности акта различения, так и остался бы выведенным. Тотальность акта различения от смены платформы не зависит; вывод $L3$ из неё — тоже.

Этот экспериментальный сдвиг обнаруживает границу точно. То, что при смене платформы может исчезнуть или измениться, — технический слой. То, что при смене платформы остаётся неизменным, — онтологический слой. Законы $L1$–$L5$ и Принципы $P1$–$P4$ принадлежат второму; classic и L4_witness — первому.

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

Почему различение необходимо

Без ясного различения двух родов позиция ToS прочитывается неверно — причём двумя противоположными способами.

Первая ошибка: принять технические аксиомы за основание. Если classic и L4_witness принять за «настоящие основания ToS», возникает картина ToS как ещё одной постулативной теории: «вот система, она выбрала такие-то две аксиомы». Эта картина ложна. Формально classic и L4_witness — настоящие аксиомы CIC; но онтологически они не основания ToS, а технические объявления, регистрирующие два Закона в платформе. Онтологическое основание ToS — вывод из акта различения, и оно имеет деривационный, а не аксиоматический статус.

Вторая ошибка: принять Законы за «просто аксиомы». Противоположная ошибка — счесть Законы $L1$–$L5$ «просто аксиомами среди прочих», набором постулатов, который ToS выбрала вместо постулатов $\mathrm{ZFC}$. Эта картина тоже ложна. Законы не выбраны и не постулированы; они выведены. Назвать их аксиомами — значит стереть деривационную природу ToS, разобранную в § 6.4.

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

«Аксиоматический минимум» — точное прочтение

Настоящая глава называется «Аксиоматический минимум и механизм статуса». Проделанный разбор позволяет прочитать это название точно.

«Аксиоматический минимум» не означает «минимальный набор оснований ToS». Формально аксиомы у ToS есть — два объявления в CIC; но онтологическим основанием они не являются: основание — вывод из акта различения, имеющий деривационный статус, а не статус постулата.

«Аксиоматический минимум» означает: минимальный объём технических объявлений, необходимых для того, чтобы провести ToS через формальную проверку в CIC. Этот объём — два объявления, classic и L4_witness. Они минимальны не в смысле «мы выбрали взять поменьше», а в смысле «CIC по своему устройству требует именно стольких, и не больше»: всё прочее, что нужно ToS, либо встроено в платформу (§ 6.7), либо выводится (Законы, Принципы, определения, теоремы).

Аксиоматический минимум ToS — это не минимум того, на чём ToS стоит, а минимум того, что ToS объявляет в конкретной платформе. ToS стоит на выводе из акта различения; ToS объявляет в CIC две технические аксиомы. Первое — основание, неизменное; второе — реализационный минимум, зависящий от платформы. Глава о том, как мало второго требуется, когда первое устроено как вывод.

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

Незавершённость: математика и квантовая

суперпозиция{Незавершённость: математика и квантовая суперпозиция}

Незавершённость как сквозной мотив главы

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

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

Незавершённость внутри математики

Стоит проговорить отчётливо: незавершённость, о которой идёт речь, — свойство самой математики в её устройстве по ToS, не временное состояние знания.

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

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

Незавершённость в ToS — не предел, у которого математика останавливается. Это устройство, по которому она работает. Определённость — числа, статуса, результата — возникает в процессе, и помимо процесса её нет. Готовая тотальность не есть цель, не достигнутая математикой; она есть конструкция, которой в процессной онтологии не отведено места.

Определённость как акт: от математики к физике

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

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

Это — тот же структурный мотив, что и в процессной онтологии ToS¹⁵: определённость есть результат акта, а не свойство, лежащее готовым до акта. В $P4$ бесконечность не предсуществует как готовый объект — она разворачивается. В механизме статуса (§ 6.6) статус не предсуществует процессу — он присваивается на шаге. В квантовом измерении определённое значение не предсуществует измерению — оно регистрируется в нём.

И всё это — в основе своей — мотив акта различения, с которого ToS начинается: определённость возникает в акте различения, не до него. То, что не различено, не есть «определённое, но скрытое»; оно есть неопределённое, и определённость наступает с актом.

Вывод физики: предмет следующего тома

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

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

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

Завершение главы

Глава 6 завершила формальное измерение Части I: разобран аппарат — Законы, Принципы, $E/R/R$-структура, технические основания реализации в Rocq, механизм статуса. Этот аппарат построен и формально проверен.

Остаётся, однако, ещё один слой Части I — не формальный, а онтологический. На протяжении Глав 1–6 неоднократно обнаруживались позиционные решения, которые ToS принимает молча, самим устройством своего аппарата: бесконечность как процесс, а не объект; список как первичная структура, а множество как производный режим работы с ним; определённость как результат акта различения. Эти решения работали в Главах 1–6, но не были собраны и явно объявлены как онтологические позиции тома.

Этому посвящена Глава 7 — заключительная глава Части I. Она онтологическая: она выносит наружу сквозные мотивы, к которым том будет возвращаться на протяжении всех последующих частей, и объявляет их явно. После Главы 7 Часть I — «Перво-различие и законы логики» — будет завершена в обоих своих измерениях, формальном и онтологическом, и развёрнутый аппарат будет готов к применению в конкретных областях математики: к числовым системам, к структуре континуума, к основаниям анализа.

---

---

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

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

Навигация: ← Глава 5. Со-определение A и ¬ A · Глава 7. Онтологическое ядро: сквозные мотивы →

Footnotes

1. Соответствующий файл — src/ToS_Axioms.v в репозитории theory-of-systems-coq. ↩

2. Соответствующий файл — src/TheoryOfSystems_Core_ERR.v в репозитории. ↩

3. Точнее, через строку Require Export Coq.Logic.Classical_Prop в файле ToS_Axioms.v: classic объявлен как Axiom в стандартной библиотеке Rocq и реэкспортируется оттуда. ↩

4. Имеются в виду модули Coq.Logic.ClassicalDescription, Coq.Logic.ClassicalEpsilon и Coq.Logic.IndefiniteDescription, перечисленные в комментарии файла ToS_Axioms.v как запрещённые к импорту. ↩

5. Формальная проверка этого устройства — в файле src/foundation/P4_Eliminates_Infinity.v репозитория theory-of-systems-coq. ↩

6. Формализация механизма — функция L5_choose в файле src/foundation/P4ProhibitsAC.v и теорема AC_is_L5 в файле src/foundation/P4_Eliminates_AC.v. ↩

7. Файл src/foundation/P4_Eliminates_ATR.v. Теорема P4_eliminates_ATR0 в нём фиксирует базовое и шаговое уравнения итерации (iterate_pred на OZero и на OSucc). ↩

8. Файл src/foundation/P4_Eliminates_Pi11.v. В нём Program := nat, а eval_program объявлен как Parameter; теорема P4_eliminates_Pi11 устанавливает эквивалентность $P4$-определённой квантификации P4_forall_functions с квантификацией по nat. ↩

9. Файл src/foundation/P4CompletedInfinity.v, тип CompletedInfSet. Теорема completed_inf_contradicts_P4. ↩

10. Формальное доказательство несовместимости — в файле src/foundation/P4ProhibitsAC.v. ↩

11. Формальная проверка — в файле src/foundation/P4ProhibitsImpredicative.v, теорема P4_dissolves_russell. ↩

12. Соответствующий тип Observable в файле src/CoinductiveSystems.v репозитория. Подробное обсуждение коиндуктивных систем — в последующих частях настоящего тома. ↩

13. l5_res_rule: для непустого списка с разрешимым полным порядком функция l5_resolve_gen возвращает значение определённого вида (Some v). ↩

14. Тип Level и отношение level_lt в файле src/TheoryOfSystems_Core_ERR.v; формальная иерархия ToS строится поверх универсной иерархии CIC. ↩

15. Процессная природа бесконечности зафиксирована в файле src/foundation/ProcessP4Synthesis.v репозитория — в формулировке «бесконечность есть процесс, не объект» и в конструкции порождающего процесса. ↩

16. В частности, файл src/foundation/UnistochasticFromGraph.v: формализованы матрицы над $Q$, ортогональность, поэлементный квадрат (gamma_of), двойная стохастичность, унистохастичность, конкретные примеры $2\times 2$ и $3\times 3$, теорема unistochastic_implies_DS. ↩