Методологическое введение

Место Тома II в серии

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

• Том I. Метафизика разворачивает онтологию — описание того, что есть как структура реальности. Он устанавливает Логику как первичный мета-аспект Абсолюта, формулирует Закон Достаточного Основания (ЗДО) как действие Логики, выводит законы логики, вводит понятия Источника и Свидетеля, и описывает структуру каскада систем, в котором разворачивается реальность. Том I — метафизическое основание всей серии.
• Том II. Математика (настоящий том) разворачивает математику как операциональное проявление онтологии Тома I. Он работает с тем минимальным фрагментом метафизики, который достаточен для математической работы, и доводит развёртывание до квантовой информации.
• Последующие тома применяют установленную систему к физике (Том III), информатике, биологии, социальным системам и философии. Каждый следующий том опирается на предыдущие.

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

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

Минимальный онтологический фрагмент

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

Логика как структура бытия

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

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

Это различие важно для всей дальнейшей работы. Когда в Главе 3 будет сказано, что L1–L4 выводятся как теоремы из структуры Distinction, это будет означать формально-математическое утверждение о доказуемости этих теорем внутри Rocq, не утверждение об онтологическом обосновании логики. Онтологически законы логики первичны; они не выводятся из акта различения — акт различения становится возможен благодаря им. То, что в формальной системе они появляются как теоремы об одном объекте, есть результат конкретного способа формализации; это техническая особенность, а не онтологическая позиция.

Закон Достаточного Основания как действие Логики

Закон Достаточного Основания (ЗДО) утверждает: ничто не существует и ничего не утверждается без основания. У Лейбница ЗДО был сформулирован как один из законов наряду с тождеством и непротиворечием. В метафизике Тома I ЗДО получает более глубокий статус: он не один из законов рядом с другими, а действие самой Логики как мета-структуры.

Различие можно прояснить так. Закон Тождества говорит о том, что есть устойчивость предметов: $A$ есть $A$. Закон Непротиворечия говорит о том, что невозможно: $A$ и $\neg A$ одновременно. ЗДО говорит о том, как работает установление этих положений: всякое утверждение требует основания, всякое существование — основания, всякая структура — условия, по которому она такова. ЗДО — это работа Логики, не закон в одном ряду с тождеством и непротиворечием.

Эта формулировка ЗДО будет работать через весь том. Каждый раз, когда мы будем требовать конструктивного построения, явного критерия, алгоритмически проверяемого условия, — мы будем применять ЗДО. Принцип $P4$ (бесконечность как свойство процессов, Часть IV) есть конкретное применение ЗДО: для актуальной бесконечности как завершённого объекта нет основания, по которому её можно было бы предъявить — есть лишь основание для бесконечного процесса как разворачивающейся сущности. Принцип $M3$ (множества как режим, Часть X) есть применение ЗДО: для существования множества как онтологически данного нет основания, есть лишь основание для решения оператора работать со списком в определённом режиме. Так ЗДО будет проявляться через весь том как структурный принцип работы Логики.

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

Законы логики в онтологическом и в формально-математическом изложении

Здесь требуется явное предупреждение о терминологическом различении, которое будет работать через всю Главу 3 и в дальнейшем.

В метафизике (Том I) законы логики выделяются и нумеруются следующим образом:

• ЗДО — мета-закон, действие Логики; первичен.
• Закон Тождества — $A=A$.
• Закон Непротиворечия — $\neg (A\wedge \neg A)$.
• Закон Порядка — структура иерархии уровней, на которой разворачивается реальность.
• Закон Исключённого Третьего — $A\vee \neg A$; производный от Тождества и Непротиворечия.

В формальной системе Rocq, в которой Том II формализован, законы получают другую нумерацию:

• $L1$ — Закон Тождества: positive D = positive D, доказываемый через reflexivity.
• $L2$ — Закон Непротиворечия: exclusive — поле записи Distinction.
• $L3$ — Закон Исключённого Третьего: exhaustive — поле записи Distinction, опирающееся на аксиому classic.
• $L4$ — Закон Достаточного Основания: теорема positive D -> ~ negative D, выводимая из exclusive.
• $L5$ — Закон Порядка: тип Level с отношением <<, выражающий иерархию уровней.

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

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

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

Нумерация $L1$–$L5$ в Rocq есть стабильный технический интерфейс формализации. Она сложилась исторически — по мере формализации, начиная с привычных в логической традиции Тождества и Непротиворечия, — и в дальнейшем сохраняется неизменной сознательно: её задача не в том, чтобы отображать онтологическую иерархию законов, а в том, чтобы обеспечивать устойчивость ссылок, доказательств и зависимостей в машинно-проверенном корпусе репозитория. Мы, стало быть, различаем две вещи: имена интерфейса ($L1$–$L5$ в том порядке, в каком они зафиксированы) и онтологический порядок законов (в котором ЗДО первичен, а исключённое третье производно). Внутренние имена формальной системы не являются онтологическими утверждениями, и смешивать их с онтологическим порядком не следует.

Том II принимает следующее терминологическое соглашение:

В обсуждении онтологии (отсылки к Тому I, философские замечания, обсуждение природы законов логики) мы пользуемся названиями без номеров: Закон Тождества, Закон Непротиворечия, Закон Достаточного Основания, Закон Порядка, Исключённое Третье. Порядок важности — ЗДО как мета-закон, далее Тождество и Непротиворечие как основные, Порядок как структурный, Исключённое Третье как производное.

В обсуждении формализации (записи в Rocq, ссылки на конкретные теоремы и определения) мы пользуемся номерами $L1$–$L5$ в той последовательности, в которой они зафиксированы в репозитории: $L1$ — Тождество, $L2$ — Непротиворечие, $L3$ — Исключённое Третье, $L4$ — Достаточное Основание, $L5$ — Порядок.

Когда требуется одновременно работать с обоими уровнями, мы явно указываем — например: «Закон Достаточного Основания (формально: $L4$)».

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

Первичный факт: $A=\exists$

Существование чего-либо есть первичный факт, не аксиома и не выбор. Установление этого факта — предмет Тома I. Здесь укажем лишь основное.

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

О самом же первичном факте здесь достаточно зафиксировать три положения.

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

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

Акт различения как первое формализуемое

Если существование есть первичный факт, не записываемый в формальной системе (потому что условие самой её возможности), то акт различения — первое, что записывается.

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

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

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

Это не определение различения — определение происходит на онтологическом уровне (Том I). Это запись различения в типах CIC — технический эквивалент онтологического объекта в формальной системе. Подробное обсуждение этой записи и того, что она формализует, — в Главе 2.

Что Том II делает и чего не делает

Чтобы у читателя были ясные ожидания, перечислим прямо.

Том II делает

• Разворачивает математику от акта различения (Часть I) до квантовой информации (Часть XV) и завершающего синтеза (Часть XVI), проходя через числовые системы, анализ, алгебру, геометрию, теорию чисел, теории категорий и информации.
• Формализует ключевые конструкции в Rocq, в репозитории theory- of- systems- coq.
• Развивает четыре сквозных мотива — M1 — позитивная онтология, M2 — операциональная делимость, M3 — множества как режим, M4 — структурная неизбежность, — через все 16 частей тома, отмечая их возвраты на полях.
• Готовит онтологический мост к Тому III (физике), не входя сам в физическое содержание.

Том II не делает

• Не обосновывает онтологию заново. Установление онтологии — работа Тома I по метафизике. Том II принимает онтологические положения как опору и развивает на них математическое содержание.
• Не разворачивает Источник, Свидетеля, Свет и каскад вложенных систем как онтологические структуры. Это структуры метафизики, принадлежащие Тому I. Для математического разворачивания они не требуются.
• Не претендует на новую физическую теорию или на решение открытых задач физики. Том II — математическая работа; физическое применение — задача Тома III.
• Не претендует на «окончательную» формализацию математики. Принципиальная открытость иерархии уровней (Глава 14.8) означает, что математическое разворачивание — процесс, не завершаемый одним томом.

Статус математических объектов

Естественный вопрос читателя, столкнувшегося с операциональной онтологией Тома II: что есть математические объекты — число, функция, группа, многообразие — в этой картине?

Том II не работает в классических альтернативах: ни в платонизме (числа существуют независимо от нас в идеальном царстве), ни в чистом формализме (числа суть лишь имена в формальной системе), ни в чистом конструктивизме (числа возникают только через нашу деятельность).

Позиция Тома II — операциональный реализм, согласованный с метафизикой Тома I. Математические объекты:

• Реальны в том смысле, что они — объективные структуры, не зависящие от индивидуального субъекта. Натуральное число $5$ тождественно само себе независимо от того, кто его рассматривает.
• Операциональны в том смысле, что их существование разворачивается через акты различения; они не уже даны как завершённые сущности, а актуализируются в процессе работы.
• Согласуются с Логикой в том смысле, что их структура есть проявление работы законов логики на конкретном уровне. ЗДО требует, чтобы у каждого объекта было основание; и оно есть — через явный конструктивный путь, по которому объект разворачивается.

Это положение будет работать через весь том. Каждое математическое определение в Томе II сопровождается явным основанием того, по какому пути объект разворачивается — ЗДО на математическом уровне. И каждый раз, когда классическая математика обращается к актуальной бесконечности, к Аксиоме Выбора, к завершённому объединению — то есть к структурам без явного конструктивного основания, — Том II ищет альтернативный путь.

Условные обозначения и порядок чтения

Условные обозначения. На полях текста ставятся метки (M1)–(M4) в местах возврата сквозных мотивов тома. В конце тома — алфавитный указатель возвратов мотивов: читатель, интересующийся одним конкретным мотивом, может проследить его по всему тому через указатель.

Особые формулировки выделяются врезками:

• Онтологические замечания (отсылки к Тому I, философские пояснения) — врезкой с пометой Онтология.
• Технические детали (которые можно пропустить при первом чтении без потери смысла) — врезкой с пометой Техника.
• Сквозные мотивы (вводимые в Главе 6 Части I и возвращающиеся через том) — врезкой с рамкой и заголовком.

Порядок чтения. Том построен как дедуктивная последовательность: каждая часть опирается на предыдущие. Линейное чтение — от Части I до Части XVI — даёт полное разворачивание.

Возможны два укороченных маршрута:

• Читатель, желающий получить философско-методологическую картину без полной математической детализации, может прочитать Часть I (Главы 1–6), Часть IV (вводящую процессную онтологию), Часть X (множества как режим), Часть XIV (категорная структура) и Часть XVI (синтез). Это даёт около 350 страниц вместо полных 1400.
• Читатель-математик, заинтересованный конкретными результатами в формальной системе, может пропустить философские главы и читать технические — Часть II–III (числовые системы), Часть IV–IX (анализ), Часть XI–XIII (алгебра, геометрия, теория чисел), Часть XV (информация). Это даёт около 800 страниц более плотного математического содержания.

Полное чтение тома — линейное — предполагается основным.

Источники. Все ключевые определения и теоремы сопровождаются ссылками на конкретные файлы и теоремы в репозитории theory-of-systems-coq, доступном по адресу

https://github.com/Horsocrates/theory-of-systems-coq

Читатель, интересующийся машинной проверкой утверждений, может самостоятельно их верифицировать.

С установленной онтологической опорой и зафиксированными терминологическими соглашениями мы переходим к Части I, начинающейся с Главы 1 о первоначале и границе формализации.

---

Том: «Математика»

Навигация: Глава 1. Первоначало: A = ∃ — Часть I →