Глава 1. Первоначало: A = ∃

Проблема начала

Регресс обоснования

Любое математическое утверждение требует обоснования. Утверждая, что $\sqrt{2}$ — иррациональное число, мы опираемся на доказательство; доказательство опирается на свойства целых чисел; свойства целых чисел — на свойства натуральных; натуральные строятся как индуктивный тип со своими правилами образования. Цепочка обоснований уходит вглубь, и естественный вопрос таков: где она заканчивается? Заканчивается ли она вообще?

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

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

В терминологии Методологического введения регресс обоснования есть прямое требование Закона Достаточного Основания (ЗДО). ЗДО говорит: всякое утверждение требует основания. Бесконечный регресс этому требованию не удовлетворяет, потому что не предъявляет актуального основания для отдельно взятого утверждения; он лишь обещает основание в бесконечности. ЗДО требует, чтобы основание было доступно в конкретной точке цепочки, не отложено в недостижимое. Таким образом, проблема начала — не результат произвольного решения, что «надо где-то остановиться», а следствие самой работы Логики на структуре обоснования.

Три классические стратегии остановки

История оснований математики предложила три различных ответа на проблему начала. Каждый ответ принимает структурную необходимость остановки, но по-разному истолковывает её природу.

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

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

Стратегия Брауэра: фундаментальная интуиция. Брауэр и его последователи в интуиционизме отвергли как самоочевидные истины Евклида, так и формальные конвенции Гильберта. Для Брауэра математика — это ментальная деятельность субъекта, разворачивающаяся во времени. Первичное начало — фундаментальная интуиция: способность сознания различать «один шаг» и «следующий шаг», порождая последовательность. Из этой интуиции выводится натуральный ряд; из натурального ряда — вся конструктивная математика. Природа начала у Брауэра — феноменологическая: оно укоренено в структуре сознания, не во внешней реальности и не в выборе.

Что общего и что различно

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

Различие проявляется в том, как каждая стратегия отвечает на вопрос «а почему именно эти начала?». Евклид отвечает: «потому что они самоочевидны» — но самоочевидность апеллирует к интуиции, которую сам формализм не может проверить. Гильберт отвечает: «потому что мы их выбрали» — но выбор кажется произвольным, и Гёдель в 1931 году показал, что даже непротиворечивость выбора не может быть установлена изнутри самой системы.² Брауэр отвечает: «потому что они укоренены в структуре сознания» — но феноменологический анализ сознания сам не является математическим методом.

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

Апория первой посылки

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

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

Эту апорию можно записать в форме структурного утверждения:

$$\begin{array}{rl}& \text{Остановка регресса требует объяснения,}\\ & \text{которое само не может быть регрессивным.}\end{array}$$

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

Положение Тома II относительно проблемы начала

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

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

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

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

В § 1.2 мы рассмотрим этот первичный факт содержательно: что он утверждает, почему он не пуст, как он самосвидетельствует. В § 1.3 мы покажем, что прямая попытка формализовать его средствами Rocq наталкивается на структурную границу — и эта граница онтологически содержательна, она говорит нечто важное о соотношении формальной системы и того, на чём она стоит. В § 1.4 мы перейдём к первому формализуемому — акту различения, который окажется первым объектом, который Том II может записать в Rocq и с которого начинается собственно математическая работа тома.

Корректное обращение с границей между пред-формальным и формализуемым — центральная методологическая позиция Тома II, к которой мы будем возвращаться многократно: в Части IV (при обсуждении принципа $P4$ — бесконечности как свойства процессов, а не завершённых объектов), в Части X (при обсуждении множеств как режима рассмотрения), в Главе 14.8 (при обсуждении принципиальной открытости категории $\mathbf{ToS}$). Каждый раз структура работы будет одной и той же: признать границу, не пытаться формализовать то, что лежит за ней, и двинуться к ближайшему формализуемому объекту по эту сторону границы.

Положение $A=\exists$: содержательное обсуждение

Формула и её прочтение

Установив в § 1.1, что Том II опирается на онтологическое разрешение проблемы начала, данное в Томе I, мы можем теперь предъявить сам первичный факт, на котором стоит математическая работа.

Этот факт записывается формулой

$$A=\exists ,$$

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

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

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

Не онтологический аргумент Ансельма. Ансельм Кентерберийский в Proslogion (XI век) предложил вывод существования Бога из самого понятия Бога как «то, больше чего нельзя помыслить»: то, что существует в реальности, больше того, что существует только в уме; следовательно, если Бог — то, больше чего нельзя помыслить, то Бог существует в реальности.³ Формула $A=\exists$ ничего подобного не утверждает. Здесь не идёт речь о выводе существования из понятия; речь о признании существования как исходной данности. $A$ — не «нечто, чьё определение требует существования», а просто нечто, о существовании которого мы можем говорить, потому что оно уже есть.

Не парменидовское $\tau \acute{o}\acute{\epsilon }\sigma \tau \iota \nu$ как онтологический тезис. Парменид в поэме О природе утверждает: «есть — есть; не есть — нет»⁴. Формулу $A=\exists$ можно прочитать как родственную этому утверждению, но между ними есть существенное различие. Парменид делает онтологический тезис о характере бытия: бытие едино, неподвижно, не имеет частей, противоположно становлению. Формула $A=\exists$ ничего о характере существующего не говорит. Она фиксирует лишь тот факт, что существование имеет место — без определения того, каково существующее или сколько его. Это минимальное утверждение, на котором сходятся самые различные онтологические позиции. Парменид, Гераклит, Аристотель, Спиноза, Лейбниц — все согласились бы с $A=\exists$, разойдясь в дальнейшем описании характера существующего.

Почему не пустое утверждение

Естественный вопрос математика, столкнувшегося с формулой $A=\exists$: что в ней содержательно? Если $A$ — произвольное «нечто», и утверждается лишь, что оно «существует», то не пуста ли эта формула? Не сводится ли она к тавтологии «существующее существует»?

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

$$\neg (A=\exists )\text{т. е.}\text{«ничто не существует»}.$$

Это утверждение, однако, имеет структурное затруднение. Само его произнесение требует:

• Существования того, кто его произносит (отрицателя).
• Существования самого отрицательного утверждения (как мыслительного или речевого акта).
• Существования контекста, в котором отрицание имеет определённое содержание (различие между «существует» и «не существует» должно быть установлено).

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

Запишем это структурно. Пусть $E$ — утверждение «нечто существует», а $\neg E$ — его отрицание. Схематически — не как формулу уже заданного объектного языка, а как мета-уровневое указание на структуру самоопровержения — это можно записать так:

$$\neg E⟹\neg (\text{утверждение}\neg E\text{существует}),$$

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

Здесь и становится видно, в чём содержательность $A=\exists$.

• Структурно $A=\exists$ не пуста, потому что её отрицание структурно невозможно. Утверждение, чьё отрицание невозможно не от слабости отрицателя, а от внутренней структуры отрицания, несёт содержание — содержание неустранимости некоторого «есть».
• $A=\exists$ противопоставлено абсолютному ничто — тому состоянию, которое Парменид называл «не есть» и которое неизрекаемо: о нём нельзя ни мыслить, ни говорить, не впадая в противоречие. Содержание $A=\exists$ — именно отрицание абсолютного ничто как структурно недопустимого.
• $A=\exists$ предпосылка теории. Если ничто не существует, нет ни рассуждения, ни рассуждающего, ни объекта рассуждения. Самó наличие настоящей теории — математической работы Тома II, читателя, физического текста, на котором написаны эти слова — есть свидетельство того, что $A=\exists$ выполнено. Работа, не предполагающая первичного факта существования, не могла бы вестись.

Самосвидетельствование как работа Логики

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

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

Применительно к $A=\exists$ это означает следующее. Парадокс отрицания, который мы рассмотрели в предыдущем подразделе, не есть нечто внешнее по отношению к Логике. Он есть прямое проявление работы Логики на самом первичном уровне — работы Закона Достаточного Основания.

Развернём это утверждение. ЗДО говорит: всякое утверждение требует основания. Применим ЗДО к утверждению «$A=\exists$»: каково основание этого утверждения? И применим ЗДО к его отрицанию «$\neg (A=\exists )$»: каково основание отрицания? Для $A=\exists$ основанием служит сам факт существования (в том числе существования рассуждения, утверждения, и рассуждающего); для $\neg (A=\exists )$ основание не может быть предъявлено, потому что любая попытка его предъявить уже использует то, что отрицается. Утверждение, для которого невозможно основание, ЗДО запрещает. Поэтому $\neg (A=\exists )$ запрещено самой работой Логики, а $A=\exists$ — утверждено той же самой работой.

Это даёт следующий важный поворот. То, что выглядело как «парадокс» — самопротиворечивость отрицания существования, — есть не парадокс в смысле проблемы, требующей разрешения, а нормальная работа Логики на её первичной структуре. ЗДО, применённый к самому первичному уровню, даёт $A=\exists$ как единственное утверждение, имеющее основание, и $\neg (A=\exists )$ как утверждение, для которого основание структурно невозможно.

В этом смысле $A=\exists$ есть не первое положение, поставленное Томом I, а первое, что Логика устанавливает о самой себе, когда обращается к вопросу о существовании. Самосвидетельствование $A=\exists$ есть ЗДО в работе.

Содержательное наполнение через философскую традицию

Формула $A=\exists$ и её самосвидетельствующий статус — не изобретение настоящей серии. Это положение принадлежит большой философской традиции, и Том II может опереться на эту традицию как на сходящиеся независимые свидетельства структурного факта.

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

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

Аристотель. В Метафизике IV книги Аристотель формулирует Закон Непротиворечия — первый принцип всего сущего и всякого рассуждения⁷. Его аргумент в IV.4 показывает, что отрицатель Закона Непротиворечия не может ничего сказать без того, чтобы воспользоваться им⁸. Структура аргумента — та же, что и у нашего обсуждения самосвидетельствования $A=\exists$: сам акт отрицания использует то, что отрицается. Аристотель применяет эту структуру к Закону Непротиворечия; Том I применяет её на более глубоком уровне — к самому факту существования.

Декарт и Августин. Раннее новое время даёт известную формулировку самосвидетельствования в контексте сомнения. Декарт в Размышлениях приходит к точке, в которой радикальное сомнение наталкивается на собственный предел: даже допустив, что я обманут во всём, я не могу сомневаться в том, что я сомневаюсь, а значит — в том, что я существую как сомневающийся⁹. Августин за двенадцать веков до Декарта формулирует это же открытие в форме si fallor, sum — «если я заблуждаюсь, я существую»¹⁰.

Структурно $cogito$ Декарта и $sifallor$ Августина суть применения $A=\exists$ к конкретному случаю — к существованию мыслящего. Они показывают, что неустранимость существования проявляется и на индивидуальном уровне: индивид не может отрицать своё существование, не впадая в противоречие, точно так же, как Логика не может отрицать существование вообще. Том II не пользуется cogito как самостоятельным основанием (это уже шаг к субъективности, которая в метафизике Тома I имеет специфическое место), но признаёт его как сходящееся свидетельство того же структурного факта.

Хайдеггер. Хайдеггер в Бытии и времени (1927) и последующих работах вводит онтологическое различие между бытием (Sein) и сущим (Seiendes)¹¹. Сущее — это любое конкретное «нечто»: вещь, факт, событие. Бытие — это то, что нечто есть, сам факт бытия чего-либо, не сводимый ни к одному конкретному сущему.

Формула $A=\exists$ ближе именно ко второму — к бытию в хайдеггеровском смысле. $A$ оставляется в неопределённости (любое нечто); $\exists$ фиксирует сам факт бытия. Это согласуется с хайдеггеровской программой возврата к вопросу о бытии, и Том I по метафизике во многом следует этой программе. Том II, опираясь на онтологию Тома I, наследует это различение, не разворачивая его в полной хайдеггеровской глубине.

Витгенштейн. Логико-философский трактат в § 6.44 даёт формулировку, особенно близкую к содержанию $A=\exists$: «Не то, как мир есть, является мистическим, а то, что он есть»¹². Витгенштейн отделяет как мира (предметом которого занимается наука) от что мира (предметом которого занимается — по его мнению — мистическое созерцание; философия же должна молчать). Том II не следует за Витгенштейном в его выводе о молчании; но фиксирует то же различение: $A=\exists$ утверждает именно что мира, не как.

Эта сходимость свидетельств — Парменид, Аристотель, Декарт, Августин, Хайдеггер, Витгенштейн, — столь различных по эпохам, языкам и методологическим установкам, к одному и тому же структурному факту свидетельствует о его неустранимости. $A=\exists$ — не изобретение нашей серии и не положение, на котором настаивает только Том I по метафизике. Это структурное обнаружение, которому философская традиция возвращается на каждом большом этапе своего развития, пере-формулируя на языке своего времени.

$A=\exists$ и математическая работа

Естественное возражение, к которому мы должны быть готовы: «всё это философия. Какое отношение $A=\exists$ имеет к собственно математической работе Тома II?»

Прямое и существенное.

Математика, какой мы её знаем, уже опирается на $A=\exists$ на самом базовом уровне — в работе экзистенциального квантора $\exists$. Когда мы пишем

$$\exists x\in N.x>0,$$

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

В терминах теории типов CIC, на которой построен Rocq и работает наш формальный аппарат, здесь нужно различать два уровня. Тип может быть сформирован — то есть быть корректным объектом языка, построенным по правилам образования типов; это ещё не означает, что он населён. Населённость типа означает наличие терма этого типа — объекта, имеющего данный тип. В соответствии Карри–Ховарда, для пропозиций населённость соответствует наличию доказательства. Эти два уровня не совпадают: тип может быть безупречно сформирован и при этом пуст — таков, например, тип False в Prop, корректный объект языка, не имеющий ни одного обитателя.

Базовый случай населённого типа: тип $N$ натуральных чисел населён, потому что у него есть конструкторы — $0$, $S(0)$, $S(S(0))$ и так далее. Каждый конструктор производит конкретный терм типа $N$, и тем самым подтверждает, что тип $N$ не пуст — что натуральные числа есть.

Поэтому формальная населённость типа не тождественна первофакту $A=\exists$. Населённость есть уже внутренний режим существования — существование терма внутри работающей типовой системы. Сам же первофакт лежит ниже: он есть условие того, что вообще возможны язык, типы, термы, правила образования — и само различие между сформированным и населённым, между населённым и пустым. Всмотримся: населённость типа $N$ опирается на то, что конструкторы $0$, $S$ сами есть, даны в типовой системе. И сам факт того, что они даны — что их можно записать, упомянуть, применить, — есть проявление того же первичного факта $A=\exists$. Если бы ничто не существовало, не существовали бы и конструкторы; если бы не существовали конструкторы, не было бы типа $N$; если бы не было типа $N$, не было бы и математики чисел.

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

Так же на каждом уровне математики. Группа существует как структура, потому что её элементы есть и групповая операция есть. Топологическое пространство существует, потому что точки и открытые множества есть. Категория существует, потому что её объекты и морфизмы есть. На каждом уровне $A=\exists$ работает как условие самой возможности говорить о математических объектах этого уровня.

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

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

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

Граница формализации

Естественная попытка

Установив в § 1.2 первичный факт $A=\exists$ как содержательное основание Тома II, мы сталкиваемся с естественным вопросом, который должен задать любой математик, привыкший работать в строго формальной системе: как записать этот факт в Rocq?

Иными словами: если $A=\exists$ есть утверждение, на котором стоит математическая работа, — то не должна ли первая строка нашего репозитория быть именно его записью? Не должно ли быть, скажем, определения

Axiom A_exists : True.

или иной аксиомы такого рода, фиксирующей $A=\exists$ как формальное утверждение, на которое все дальнейшие теоремы могут ссылаться?

Этот ход кажется естественным. Он соответствует обычной практике математической формализации: если есть утверждение, на которое теория опирается без доказательства — запишем его как аксиому. Гильбертова программа оснований, разобранная нами в § 1.1.2, требует именно этого — определить формальную систему как набор аксиом и правил вывода. Если $A=\exists$ — основание Тома II, у него должно быть место в формальной системе Rocq, на которой Том II записан.

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

Что делает запись Axiom A_exists : True

Рассмотрим внимательно, что именно происходит, если мы добавляем в систему запись

Axiom A_exists : True.

Чтобы это понять, нужно вспомнить, что есть True в CIC, на которой построен Rocq.

True — индуктивный тип с единственным конструктором:

Inductive True : Prop :=
  | I : True.

Тип True населён — у него есть обитатель I. Это означает: утверждение True в Rocq уже доказуемо без каких-либо аксиом, потому что обитатель I даёт прямое свидетельство. В любой точке любого доказательства можно написать exact I и завершить любой подгол вида True.

Что добавляет аксиома Axiom A_exists : True к системе CIC? Технически: имя A_exists, ссылающееся на свидетеля типа True. Что нового она сообщает системе? Ничего. У типа True уже был свидетель I; добавление имени для того же самого (или эквивалентного) свидетеля не расширяет ни множества теорем, ни возможностей системы.

Это — первый ход обнаружения границы. Попытка формализовать $A=\exists$ через тривиальный тип True вырождается. Запись либо не сообщает ничего нового (если она формально эквивалентна тому, что уже есть в системе), либо вводит имя без содержания (если она претендует на нечто, чего в True нет, но формально с тем же типом).

Попытка через Inhabited

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

В Rocq и в стандартной библиотеке Coq.Logic.Inhabited есть типовой класс, утверждающий, что некоторый тип населён, то есть имеет по крайней мере одного обитателя:

Class Inhabited (X : Type) : Prop :=
  inhabited_witness : X.

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

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

Axiom A_exists_inhabited :
  exists (X : Type), Inhabited X.

или, эквивалентно,

Axiom A_exists_inhabited :
  exists (X : Type) (x : X), True.

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

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

Содержательно. В системе CIC у нас уже есть, например, тип unit с единственным обитателем tt, или тип nat с обитателями 0, 1, 2, … — и так далее. Утверждение «существует тип, имеющий обитателя» уже доказуемо в CIC, без каких-либо аксиом:

Theorem some_type_inhabited :
  exists (X : Type) (x : X), True.
Proof.
  exists unit. exists tt. exact I.
Qed.

Объявление этого утверждения как аксиомы — избыточно: оно и так доказуемо. Если же мы попытаемся объявить аксиомой именно «существование чего-то до конкретных типов» (не предъявляя unit или nat как свидетеля), нам потребуется нечто, что является типом, но при этом не есть какой-либо из уже определённых типов. Такого объекта в CIC нет.

Структурно. Чтобы доказать Inhabited X для какого-либо X, нужен конкретный обитатель. Иначе доказательство невозможно. Но если для подтверждения существования X нужен его обитатель, а обитатели — это объекты, которые уже есть в системе типов, то мы вернулись к тому же вопросу: откуда в системе типов есть эти объекты? Ответ: они появляются через работу самой системы типов, опирающейся на CIC, опирающейся, в свою очередь, на то, что существование есть.

Это — та же циркулярность, что и в первой попытке, но более явная. Чтобы формализовать $A=\exists$ через Inhabited, нужно предъявить тип с обитателем. Но предъявление типа с обитателем уже использует то, что типы и обитатели есть. Формализация $A=\exists$ требует $A=\exists$ как условия её самой возможности.

Структура границы

Двух попыток — через True и через Inhabited — достаточно, чтобы увидеть структуру обнаружения. Можно попробовать ещё несколько вариантов — через ex в стандартной библиотеке, через типовые классы более общего вида, через высшие сорта типов, — но во всех случаях обнаружится одна и та же структура:

• Либо запись формально эквивалентна тому, что уже есть в CIC без всякой аксиомы, и её добавление избыточно.
• Либо запись требует для своего доказательства предъявления конкретного существующего объекта, и это предъявление является именно тем, что мы пытались сформулировать как аксиому.

В обоих случаях $A=\exists$ не записывается как самостоятельное утверждение формальной системы. Не потому, что мы не нашли правильной формулировки. А потому, что сама формальная система уже работает на основании $A=\exists$, и попытка записать это основание изнутри системы натыкается на структурную циркулярность: основание не является объектом системы, оно есть условие самой возможности системы.

Запишем эту структуру формально. Пусть $S$ — формальная система с языком $L(S)$ — множеством корректно построенных формул, которые $S$ способна выразить. Утверждение $\varphi$ записывается в системе $S$, если $\varphi \in L(S)$.

Утверждение.

Внутри уже заданной формальной системы $S$ всякая формула, претендующая выразить $A=\exists$ как основание самой системы, попадает в одну из двух ситуаций:

1. она становится обычной внутренней формулой или аксиомой системы $S$ — и тем самым уже предполагает язык, правила и объекты $S$;
2. она вырождается в тривиальную населённость или доказуемость того, что в $S$ уже имеется.

Следовательно, $A=\exists$ не может быть внутренним основанием системы $S$ в том же смысле, в каком обычная аксиома есть внутреннее основание теории. Оно может быть лишь пред-формальным условием возможности самой формализации.

Это утверждение мы не доказываем формально — такого доказательства, в строгом смысле, не существует, потому что речь идёт о метатеоретическом наблюдении, не о теореме внутри одной системы. Мы обнаруживаем его через анализ конкретных попыток (как было сделано в подразделах «Что делает запись Axiom A_exists : True» и «Попытка через Inhabited») и через структурное рассуждение о статусе формальных систем как технических реализаций уже-работающей Логики (см. Методологическое введение, раздел о Логике как структуре бытия).

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

$A=\exists$ — не объект, формализуемый внутри формальной системы; это условие самой возможности формальной системы.

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

В терминах метафизики Тома I: Логика не записывается в формальной системе, потому что формальная система есть техническая реализация Логики, не сама Логика; $A=\exists$ не записывается в формальной системе, потому что формальная система работает на основании факта существования, не определяя его.

Связь с теоремами о неполноте

Здесь следует сделать одно важное прояснение, особенно для читателя, знакомого с результатами Гёделя. Положение «Структура границы» не есть теорема Гёделя о неполноте, но оно структурно родственно тому, что Гёдель показал.

Первая теорема Гёделя¹³ устанавливает: в любой формальной системе $S$, способной выразить арифметику и непротиворечивой, существуют истинные утверждения о натуральных числах, которые не доказуемы в $S$. Эти утверждения принадлежат языку $L(S)$ — то есть они выразимы в $S$, — но их доказательство выходит за рамки $S$.

Положение «Структура границы» другое. Оно говорит не о недоказуемости формулы в системе, а о том, что $A=\exists$ не может быть внутренним основанием системы. Всякая формула, претендующая выразить $A=\exists$ как основание $S$, либо становится рядовой внутренней формулой $S$ (и тем самым уже предполагает систему), либо вырождается в тривиальность. Граница здесь лежит не между выразимым и доказуемым, а между тем, что система высказывает внутри себя, и тем, что есть условие её собственной возможности.

Различие можно изобразить так:

• Гёдель: внутри формальной системы есть выразимые, но недоказуемые формулы. Граница — между выразимым и доказуемым.
• Том II: для $A=\exists$ граница лежит раньше — между выразимым формальной системой и тем, что является условием возможности этой формальной системы. Граница — между выразимым и предпосылкой выразимости.

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

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

Возражения и ответы

Естественные возражения к положению «Структура границы» стоит явно проговорить.

Возражение 1. «Возможно, мы просто не нашли правильной формализации. Должна быть более удачная запись, в которой $A=\exists$ выразимо без циркулярности.»

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

Кроме того, аргумент в подразделе «Структура границы» был структурный, не привязанный к конкретной записи: чтобы выразить $A=\exists$ в $L(S)$, нужно либо использовать обитателей системы (но их существование — это и есть то, что мы пытаемся записать), либо ввести запись, формально эквивалентную уже-имеющимся истинам системы (тогда запись ничего не сообщает). Никакая «новая удачная запись» эту структурную дилемму не обходит.

Возражение 2. «Программа Гильберта же работает — мы постулируем аксиомы и развиваем теорию. Почему здесь это не работает?»

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

Это легко увидеть. Аксиома Пеано «существует $0\in N$» — не аксиоматизация существования; это предъявление конкретного объекта $0$ в качестве элемента типа $N$, при том что и $0$, и $N$ есть как объекты языка. Аксиома работает на уровне свойств $N$, а не на уровне наличия $N$. Том II не отрицает программу Гильберта на её собственном уровне; он указывает, что ниже аксиоматического уровня лежит условие самой возможности этих аксиом, и это условие имеет иной статус.

Возражение 3. «В ZFC есть аксиома существования пустого множества: $\exists x.\forall y.y\notin x$. Это прямая аксиоматизация существования. Почему она работает там, но не работает здесь?»

Ответ. Аксиома пустого множества в ZFC аксиоматизирует существование конкретного множества с определённым свойством (быть пустым). Она работает внутри уже-принятого языка предикатов первого порядка. Все его языковые элементы есть — они предполагаются до аксиомы. Прежде чем записать аксиому пустого множества, ZFC уже работает на основании того, что (а) есть язык предикатов, (б) есть формулы этого языка, (в) есть переменные и квантор существования, (г) есть отношение принадлежности $\in$, (д) есть режим рассуждения о множествах как объектах теории.

Сам символ $\varnothing$ появляется уже после этого — как обозначение объекта, существование и единственность которого устанавливаются внутри теории; примитивным символом языка он не является. Все перечисленные пункты — проявления $A=\exists$ на уровне ниже аксиомы. Аксиома пустого множества аксиоматизирует существование одного конкретного множества; она не аксиоматизирует существование вообще. Том II не критикует ZFC за это — ZFC не претендует на аксиоматизацию существования вообще, и работает в своих рамках корректно. Мы лишь указываем, что вопрос о существовании вообще, в отличие от существования пустого множества, имеет иной статус и не подлежит аксиоматизации в обычном смысле.

Возражение 4. «Тогда философия — не математика. Может, в самом начале не нужно вводить никакой формы $A=\exists$, а просто начать с конкретных аксиом, как делает обычная математика?»

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

Во-первых, обычная математика, не задаваясь вопросом о $A=\exists$, неявно принимает его на каждом шаге. Том II делает это явным — не для того, чтобы изменить обычную работу, а для того, чтобы предъявить основание, которое всё равно работает.

Во-вторых, и это важнее: следующая глава (Глава 2) разворачивает первый формализуемый объект — акт различения. Этот объект неявно опирается на $A=\exists$, как и любая формальная конструкция. Но в Главе 3 акт различения станет основанием для вывода законов логики как теорем Rocq. Чтобы эта структура работала — чтобы было ясно, на чём стоит сам акт различения, в каком отношении он находится к Логике (которая, как мы знаем из Методологического введения, онтологически первична), — $A=\exists$ должно быть зафиксировано прежде формализации. Иначе акт различения предстал бы как «первоначало» в формальном смысле — что неверно онтологически: он есть первое формализуемое, а не первое вообще.

Различение первого вообще ($A=\exists$, пред-формальное) и первого формализуемого (акт различения, записываемый в Rocq) есть центральная методологическая работа Главы 1 и Главы 2. Это различение Том II делает явным, чтобы оно работало на протяжении всех последующих частей.

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

Что делать с границей: переход к акту различения

Не объяснять, а двинуться

Установив в § 1.3 границу формализации $A=\exists$ и обнаружив, что эта граница онтологически содержательна, мы сталкиваемся с естественным методологическим вопросом: что делать дальше?

Возможны несколько ответов на этот вопрос. Один путь — разворачивать обсуждение границы. Можно посвятить тома анализу того, что лежит по ту сторону: соотношение Логики и формальной системы, природа условия, асимметрия выразимого и предпосылок выразимости. Хайдеггер, Левинас, Деррида в XX веке посвятили этой работе значительные тексты, и каждый из них — собственная философская традиция, со своими терминологией, методологией, тонкостями.

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

Стратегия Тома II относительно границы такова:

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

Это не философское отступление; это рабочий метод. Признание границы было сделано в § 1.3 (Предложение «Структура границы»). Теперь нам предстоит сделать второй шаг: найти тот объект, который, опираясь на $A=\exists$, является первым, что Том II может записать формально — то есть формализовать в Rocq и работать с ним как с объектом математической теории.

Иными словами, вопрос меняется. Мы больше не спрашиваем: что есть $\exists$? — вопрос, ведущий в метафизику Тома I. Мы спрашиваем: что является первым формализуемым после $\exists$? — вопрос, ведущий в Главу 2 и далее.

Этот сдвиг — от онтологии (что есть) к операциональной онтологии (как с этим работать) — характерен для всего Тома II. Том не останавливается на каждой границе для её содержательного анализа; он фиксирует границы там, где они встречаются, и переходит к работе с тем, что лежит по сю сторону границы. Эта стратегия будет повторяться многократно — в Части IV (граница, отделяющая завершённую актуальную бесконечность как объект от бесконечности как свойства процессов; принцип $P4$), в Части X (граница «множества как первичного объекта», $M3$), в Главе 14.8 (граница «универсума всего», открытость иерархии). Каждый раз структура работы будет одной и той же: признать, не сокращать, двинуться.

Прослеживание условий: применение ЗДО к $A=\exists$

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

Ход обнаружения такой. У нас есть $A=\exists$ как первичный факт. Применяем к нему Закон Достаточного Основания: каковы условия, делающие этот факт возможным? Что должно быть, чтобы существование чего-либо имело место? Это не риторический вопрос; ЗДО — работа Логики, а Логика, по природе своей, не оставляет ни одного факта без основания.

Развёрнутое обнаружение этих условий — задача Тома I по метафизике. Тому II достаточно опереться на его результат и кратко повторить существенное.

В Томе I показано: для того чтобы существование чего-либо имело место, должна быть структура, в которой различимое было бы различимым. А именно:

• Существующее должно быть тождественно самому себе — иначе оно не было бы определённым нечто, а растворилось бы в неразличимом. Закон Тождества.
• Существующее не может одновременно быть и не быть в одном отношении — иначе само различие между «есть» и «не есть» утратило бы смысл, и $A=\exists$ ничего бы не утверждало. Закон Непротиворечия.
• Различимое должно разворачиваться в структуре, где одно есть условие для другого — иначе все различения возникали бы одновременно и без отношения друг к другу, что есть не структура, а хаос. Закон Порядка.

Это не аксиомы, к которым мы пришли, и не правила, которые мы выбрали. Это условия, которые ЗДО, применённый к $A=\exists$, обнаруживает как необходимые. Без любого из них существование чего-либо невозможно.

Производным от Тождества и Непротиворечия оказывается Закон Исключённого Третьего: если нечто есть (Тождество) и не может быть одновременно собой и не собой (Непротиворечие), то между «есть» и «не есть» нет третьего — ничего, что было бы ни одним, ни другим. В метафизике Тома I этот закон признаётся производным; в формализации Тома II, как мы помним из Методологического введения, он получает статус самостоятельного $L3$ по техническим причинам Rocq.

Эти законы — Тождество, Непротиворечие, Исключённое Третье (производный), Порядок — суть структура самой Логики, делающая возможным факт $A=\exists$. Они онтологически первичны: они не следуют из существования, они есть его условия. Том I разворачивает эту картину в полноте; Том II принимает её и переходит к собственно математической задаче.

Положение ЗДО. ЗДО не входит в этот список как ещё один закон. ЗДО — мета-закон, само действие Логики, через которое указанные законы обнаруживаются как условия. Применение ЗДО к $A=\exists$ и есть тот ход, которым были выявлены остальные законы; ЗДО работает над ними, не рядом с ними. Это согласуется с положением метафизики Тома I: ЗДО есть само обоснование, а не одно из обоснованных. В дальнейшем мы увидим, что и в самом акте различения ЗДО действует не как одно из его условий, а как мета-структура, в которой работают все четыре поля записи.

Здесь важно сразу различить онтологический и формальный уровни, чтобы позже не возникло терминологической двусмысленности. В онтологическом изложении ЗДО есть мета-закон — само действие Логики, требующее основания. В формальной же записи Тома II это действие имеет несколько различных технических следов, и они не должны смешиваться. В структуре Distinction оно проявляется как самозаземление различения: из положительной стороны следует отрицание отрицательной. В аксиоматическом слое оно проявляется иначе — как требование определённого свидетеля для индивидуального существования. И через весь том оно работает как общий методологический принцип явного основания. Эти технические следы не исчерпывают ЗДО и не отождествляются с ним: каждый выражает лишь одну рабочую сторону мета-закона внутри формальной системы. Когда ниже мы говорим о законе $L4$ как о теореме формализации, речь идёт именно об одном из этих следов, а не о ЗДО в его онтологической полноте.

Простейшее проявление законов: акт различения

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

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

Простейшее структурное движение есть разделение некоторого «есть» на положительную и отрицательную стороны. Рассмотрим его внимательно:

• Положительная сторона — то, что есть в смысле совершаемого разделения. Утверждение positive. Закон Тождества применяется к ней: положительная сторона тождественна самой себе — positive есть positive.
• Отрицательная сторона — то, чем положительное не является. Утверждение negative.
• Закон Непротиворечия требует: положительное и отрицательное не могут одновременно иметь место. exclusive: $\neg (‘positive‘\wedge ‘negative‘)$.
• Между положительным и отрицательным нет третьего; вместе они исчерпывают возможные стороны разделения. exhaustive: $‘positive‘\vee ‘negative‘$. (Это — Исключённое Третье, производное от Тождества и Непротиворечия в онтологии Тома I, но в формализации Rocq записываемое как самостоятельное поле.)

Над всем этим работает Закон Достаточного Основания как мета-закон. ЗДО не есть один из четырёх перечисленных законов; он есть само действие Логики, в котором различение происходит. Развернём это утверждение по существу.

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

• Поле positive имеет содержание потому, что есть основание для его утверждения; ЗДО требует, чтобы это содержание было предъявлено.
• Поле negative имеет смысл потому, что есть основание для отрицания — именно это полагается отсутствующим, не нечто иное.
• Поле exclusive требует основания для исключительности: почему именно эти две стороны не могут совпадать? ЗДО требует, чтобы исключительность опиралась на структуру самого разделения, не была произвольным условием.
• Поле exhaustive требует основания для исчерпанности: почему именно эти две стороны вместе охватывают всё? ЗДО требует, чтобы исчерпанность была проявлением структуры, не случайным дополнением.

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

Таким образом, акт различения есть одновременное проявление всех законов Логики: Тождества и Непротиворечия — в содержании полей; Исключённого Третьего — в их совместности; ЗДО — в самой работе различения как обоснованного акта. Ни один из законов не может быть удалён без распада структуры: убери Тождество — positive перестаёт быть определённым; убери Непротиворечие — exclusive теряет силу; убери Исключённое Третье — exhaustive становится произвольным; убери ЗДО — и сам акт различения теряет основание, становясь случайным.

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

Это структурное движение мы называем актом различения. И именно его Том II обнаруживает как первое формализуемое — не выбирает, не назначает, а констатирует как простейшее проявление всех законов Логики (включая ЗДО), доступное для записи в Rocq.

В каком смысле акт различения «первый»

Слово «первое» применительно к акту различения требует точного прояснения, поскольку оно работает сразу в нескольких смыслах, и важно не смешать их.

Первое в онтологии Тома I — порождающее время. В метафизике Тома I показано, что первый акт различения (Свет, в терминологии Тома I — акт Логики, различающей внутреннее состояние Источника) есть первое событие в онтологии. До этого акта существуют Логика и Источник как факты, но событий нет; нет, соответственно, и последовательности; нет и времени. Время рождается в самом акте различения — как структура последовательности актов, которая стартует от первого различения.

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

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

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

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

Первое в записи в Rocq — технически приоритетное. В репозитории theory-of-systems-coq запись Distinction исторически появилась раньше других основных структур и служит основанием для дальнейших определений. Это — технический факт о порядке файлов и теорем в репозитории, не претендующий на онтологическое утверждение.

Все три смысла «первого» — онтологический (порождает время), структурный (базовый для дедукции), технический (приоритет в репозитории) — согласованы между собой, но имеют разные основания и работают на разных уровнях. Когда мы говорим, что акт различения есть первое формализуемое в Томе II, мы используем все три смысла одновременно, поскольку в нашем случае они совпадают на одном объекте.

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

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

Первое формализуемое в Томе II — акт различения. Он будет введён и развёрнут в Главе 2; здесь мы лишь обозначим контур того, что Глава 2 будет содержать.

Акт различения формализуется в CIC как запись с четырьмя полями:

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

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

Содержательно negative читается как отрицательная сторона положительного — то, чем положительное не является. Однако технически в записи Distinction поле negative оставлено самостоятельным полем типа Prop: запись не требует синтаксического равенства negative = ~ positive. Связь между positive и negative задаётся не равенством, а доказательствами exclusive и exhaustive. Канонический случай — конструкция distinction_of, которая по пропозиции $P$ строит различение, выбирая отрицательную сторону равной $\neg P$, — но общая запись Distinction шире: она сохраняет более широкую структурную форму, оставляя отрицательную сторону явным полем акта. Это различение общего и канонического случая будет важно в Главе 2.

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

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

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

В последующей главе о со-определении положительного и отрицательного будет развёрнуто со-определение: невозможно построить Distinction, имея лишь одну из сторон. Положительное и отрицательное со-возникают в самом акте, и эта со-возникающая структура — основа дальнейшего понимания дуальностей в Томе II.

В последующей главе об аксиоматическом слое Rocq будут проговорены технические аксиомы, на которые опирается работа с Distinction (classic и L4_witness), и впервые развёрнут механизм, заменяющий Аксиому Выбора — передача статуса через E/R/R с применением $L4$ и $L5$.

В Главе 6 будут зафиксированы четыре сквозных мотива тома $M1$, $M2$, $M3$, $M4$, к которым Том II будет возвращаться через все последующие части.

Что мы выиграли

Прежде чем закрыть § 1.4 (и тем самым Главу 1) подведём итог того, что было достигнуто, поскольку этот итог имеет значение не только для Главы 1, но и для всей дальнейшей работы Тома II.

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

Внутри формальной системы Том II имеет конкретное основание: акт различения как первое формализуемое. Из него выводятся законы логики (Глава 3), типизация (Глава 2.4), онтология положительно-отрицательного (Глава 4). Дальнейшая работа Тома II получает прочный фундамент в виде формального объекта, на котором стоит строго.

При этом $A=\exists$ остаётся пред-формальным основанием, к которому Том II отсылает — через Методологическое введение, через обсуждение в Главе 1, через возвраты мотивов в дальнейших частях, — но которое не присваивает в свой формальный язык. Это уважение к структурной границе. То, что онтологически первично (Логика, $\exists$, ЗДО как действие Логики), остаётся за пределами формальной системы и принадлежит Тому I по метафизике. То, что математически первое формализуемое (акт различения), становится центральным объектом Главы 2 и фундаментом всего Тома II.

Связь со всем томом

Стратегия, развёрнутая в Главе 1, — различить пред-формальное и формальное, признать границу, двинуться к ближайшему формализуемому, — является методологической матрицей Тома II. Эта матрица будет работать на разных уровнях через все 16 частей. Краткий анонс важнейших возвратов:

• Часть IV. Принцип $P4$ — бесконечность есть свойство процессов, не завершённых объектов. Здесь не вводится запрет; здесь констатируется структурный факт о природе бесконечности — бесконечность как завершённый объект не существует, поскольку завершённость и неисчерпаемость суть несовместимые характеристики. Что существует — бесконечный процесс как актуальная сущность, разворачивающаяся шаг за шагом. Первое формализуемое в этой онтологии — RealProcess как функция $N\to Q$: первичный объект анализа, из которого затем реконструируются те функции, которые классически выполняет $R$.
• Часть X. Принцип $M3$ — множества как режим рассмотрения. Граница лежит между списком как онтологически первичной структурой и множеством как абстрактным «уже-собранным» объектом. Первое формализуемое за границей — список как индуктивный тип, на котором работает оператор в режиме игнорирования части атрибутов.
• Глава 14.8. Принципиальная открытость категории $\mathbf{ToS}$. Граница лежит между конкретными уровнями иерархии $\text{Sys}(L_0),\text{Sys}(L_1),\dots ,\text{Sys}(L_n)$ и гипотетическим «универсумом всего», который Том II не формализует как завершённый объект. Первое формализуемое за границей — сама схема перехода между уровнями (функторы forget и embed с их сопряжением).

В каждом случае работает одна и та же матрица:

1. Обнаружение границы: содержательное наблюдение, что некоторый объект (актуальная бесконечность, завершённое множество всего, универсум типов) не может быть формализован без вырождения или циркулярности.
2. Признание границы: фиксация, что объект не подлежит формализации в Томе II, и сохранение уважения к этому факту, не попытка обойти.
3. Движение к ближайшему формализуемому: нахождение того объекта, который, опираясь на пред-формальное, является первым формализуемым по эту сторону границы.

Глава 1 в этом смысле есть не только введение в Часть I, но образец методологии всего Тома II. Каждое из последующих обнаружений структурной границы будет повторять структуру обнаружения, развёрнутую здесь — но в контексте конкретной математической работы. Освоив эту структуру в Главе 1, читатель имеет инструмент, который будет работать многократно.

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

---

---

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

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

Навигация: ← Методологическое введение · Глава 2. Акт различия: запись Distinction →

Footnotes

1. Аристотель, Аналитики, I, 3 (72b5–25). Аристотель рассматривает три позиции относительно начала научного знания: бесконечный регресс, круг и наличие неподвижных начал. Первые две он отвергает; третью принимает. ↩

2. Гёдель К., О формально неразрешимых предложениях Principia Mathematica и родственных систем, 1931. Вторая теорема Гёделя устанавливает, что в любой формальной системе, способной выразить арифметику, утверждение о непротиворечивости этой системы не доказуемо средствами самой системы. ↩

3. Ансельм Кентерберийский, Proslogion, II–IV. Аргумент впоследствии воспроизводили в различных формах Декарт (Размышления, V) и Лейбниц (Монадология, §44–45); критическому разбору подвергли Кант (Критика чистого разума, B 620–630) и в XX веке — Рассел. ↩

4. Парменид, фр. B6 DK. См. также фр. B2: «один путь — что есть и что невозможно не быть… другой — что не есть и что необходимо не быть». ↩

5. Парменид, фр. B2.3–5 DK. Греч.: $\dot{\eta }$ $\mu \grave{\epsilon }\nu$ $\ddot{o}\pi \omega \varsigma$ $\ddot{\epsilon }\sigma \tau \iota \nu$ $\tau \epsilon$ $\kappa \alpha \grave{\iota }$ $\dot{o}\varsigma$ $o\dot{v}\kappa$ $\ddot{\epsilon }\sigma \tau \iota$ $\mu \grave{\eta }$ $\epsilon \tilde{\iota }\nu \alpha \iota$\dots ↩

6. Парменид, фр. B2.7–8 DK. ↩

7. Аристотель, Метафизика, IV.3, 1005b19–23. ↩

8. Там же, IV.4. Аристотель пишет: «Тот, кто отрицает закон, должен говорить, а говорящий говорит нечто, то есть утверждает определённое значение; без этого нет осмысленной речи». ↩

9. Декарт, Размышления о первой философии, II. Латинский оригинал, AT VII 25: «Ego sum, ego existo, quoties a me profertur, vel mente concipitur, necessario esse verum» — «Я есмь, я существую, всякий раз как это произносится мной или мыслится, необходимо истинно». ↩

10. Августин, О граде Божием, XI.26. ↩

11. Хайдеггер М., Бытие и время, §1–7; особенно §2 о различии Sein/Seiendes. Русский перевод: Хайдеггер М., Бытие и время / Пер. В. В. Бибихина. Москва: Ad Marginem, 1997. ↩

12. Витгенштейн Л., Логико-философский трактат, § 6.44. Нем.: Nicht wie die Welt ist, ist das Mystische, sondern, dass sie ist. ↩

13. Гёдель К., Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, 1931. Русский перевод: Гёдель К., О формально неразрешимых предложениях Principia Mathematica и родственных систем // Гёдель К. Избранные труды. М.: ОГИЗ, 2003. ↩