Глава 1. P4: бесконечность как процесс

Принцип конечной актуальности

Где стоит том

Три части позади. Часть I вывела из единственного начала — из того, что нечто есть, — акт различения и пять его законов; Часть II построила натуральный ряд как длину списка различий; Часть III развернула из натурального ряда целые и рациональные числа и показала, что рациональные числа перечислимы, а затем — что за числом-позицией встаёт объект иного рода, число-процесс. Последняя глава Части III разобрала первый такой процесс, $2$ , и довела изложение до порога: процесс как самостоятельный предмет назван, но не построен.

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

Прежде чем строить процесс как тип (это сделает следующая глава), нужно довести до полной ясности принцип, который этот тип оправдывает. Принцип называется $P 4$ . Он действовал в томе с самого построения натурального ряда, но действовал без развёрнутого изложения — упоминался там, где был нужен, и применялся, но не получал отдельной главы. Настоящая глава такую главу ему отводит.

$P 4$ {P4}: что он утверждает

Начнём с того, что $P 4$ утверждает, — и приведём утверждение дословно, в той формулировке, какую даёт ему изложение ToS.¹ Принцип носит имя конечной актуальности (в оригинале — Finite Actuality), и его утверждение состоит из двух фраз:

$P 4$ (конечная актуальность). Всякая система в любой момент конечна. Бесконечность есть свойство процесса, а не объекта.

Вчитаемся. Первая фраза — о системе в момент: что бы мы ни взяли — какую угодно систему, на какой угодно ступени её развёртывания, — взятое в данный момент конечно. Не <<мало>>, не <<ограничено числом, которое мы знаем>>, а именно конечно: состоит из конечного числа различённых элементов. Вторая фраза говорит, куда при этом девается бесконечность: она не исчезает, она меняет носителя. Бесконечность есть свойство процесса — того, как система разворачивается, шаг за шагом, без последнего шага, — а не свойство объекта, не характеристика какой-либо системы, взятой в момент. Бесконечен ход; всякий кадр этого хода конечен.

Отсюда — и только отсюда, как следствие, — получается то, что обыкновенно ставят на место самого принципа: <<нет завершённой бесконечности>>. Если всякая система в момент конечна, а бесконечность принадлежит лишь процессу, то <<завершённая бесконечность>> — бесконечная система, взятая как готовый наличный объект, — это сочетание несочетаемого: бесконечность приписана тому, чему она по $P 4$ принадлежать не может, — объекту, а не процессу. Глава будет не раз возвращаться к формуле <<нет завершённой бесконечности>>; но важно с самого начала видеть, что это вывод из $P 4$ , а не $P 4$ сам. Сам принцип утвердителен: он говорит, что есть (конечная система в каждый момент, бесконечность как свойство хода), а не чего нет.

Различие, которое $P 4$ проводит, — онтологическое, не количественное. Спор не о том, <<сколько>> всего есть; спор о том, чему принадлежит бесконечность — объекту или процессу. Стандартная математика принимает бесконечные множества как первичные объекты: в аксиоматике Цермело–Френкеля есть аксиома бесконечности, прямо постулирующая бесконечное множество как наличный предмет. $P 4$ помещает бесконечность не в предмет, а в его развёртывание. И уже из этого, как покажут следующие разделы, вытекает всё остальное — и то, какие привычные допущения оказываются не нужны, и то, чем должно быть действительное число.

Замысел главы

Глава отвечает на семь вопросов, и каждый следующий раздел берёт по одному. Что точно говорит $P 4$ и каков его формальный статус (§ 1.2). Откуда $P 4$ берётся — из каких уже введённых начал он вытекает (§ 1.3). Где $P 4$ уже работал в предыдущих частях (§ 1.4). Как $P 4$ соотносится с классическими аксиомами — какие из них он делает излишними и с какими несовместим, причём это потребует особой точности (§ 1.5). Что $P 4$ , напротив, оставляет полностью работоспособным (§ 1.6). Как $P 4$ соотносится с интуиционизмом Брауэра — ближайшим историческим предшественником (§ 1.7). И, наконец, что $P 4$ готовит для построения процесса как типа — мост к Главе 4.2 (§ 1.8).

Особая оговорка о разделе § 1.5. ToS располагает машинно-проверенной формализацией в системе Rocq, и эта глава, как и главы Части III, сверяется с нею построчно. Формализация показывает, что соотношение $P 4$ со стандартными аксиомами устроено тоньше, чем простое << $P 4$ запрещает аксиому>>. Там работают два различных слоя утверждений, и глава их аккуратно разведёт. Поспешная формулировка здесь была бы не упрощением, а ошибкой.

Точная формулировка и формальный статус

От формулировки к формализации

Раздел § 1.1 привёл формулировку $P 4$ дословно: всякая система в момент конечна, бесконечность есть свойство процесса. Формулировка эта утвердительна — она говорит, что есть. Настоящий раздел показывает, как это утверждение выглядит в машинно-проверенной формализации ToS, и каков его там статус: определение это или аксиома, доказанное или принятое.

Забегая вперёд: в формализации $P 4$ предстаёт тоже утвердительно — и даже резче, чем в прозе. Формализация не записывает <<нет завершённого бесконечного объекта>>; такое и нельзя записать прямо, ибо это утверждение о несуществовании. Она записывает противоположное — что существует: процессы определённого рода, и они ведут себя определённым образом. Разберём это — сперва саму формализацию (§ 1.2.2), затем её онтологическое прочтение (§ 1.2.3), затем её логическое основание (§ 1.2.4).

$P 4$ {P4} в формализации: что построено

{ В Rocq-репозитории ToS четыре принципа — $P 1$ , $P 2$ , $P 3$ , $P 4$ — сведены в один файл, ProcessFourPrinciples.v, и каждый получает там формальное определение.² Сам файл в пояснительном комментарии характеризует $P 4$ одной строкой: P4: Process — everything is a process (nat -> Q) — << $P 4$ : Процесс — всё есть процесс ( $N \to Q$ )>>. Заметим: и здесь формулировка утвердительна — она говорит, чем всё является (процессом), а не чего не существует. }

Определение $P 4$ в этом файле построено в согласии с такой характеристикой — но не равно ей. Оно утвердительно и состоит из трёх частей. Во-первых, существует процесс, который есть процесс Коши, — разворачивающаяся последовательность рациональных приближений, сходящаяся в том операциональном смысле, который Глава III.4 назвала свойством Коши. Во-вторых, процессы Коши замкнуты относительно умножения: произведение двух таких процессов снова есть процесс Коши. В-третьих, они замкнуты относительно сложения: сумма двух процессов Коши снова есть процесс Коши. Формально — предикат P4_formalized, конъюнкция этих трёх утверждений; вот он в записи Rocq дословно:

Definition P4_formalized : Prop :=
  (exists R : RealProcess, is_Cauchy R)
  /\ (forall R1 R2 : RealProcess, is_Cauchy R1 -> is_Cauchy R2 ->
        is_Cauchy (process_fst (process_product R1 R2)))
  /\ (forall R1 R2 : RealProcess, is_Cauchy R1 -> is_Cauchy R2 ->
        is_Cauchy (process_sum R1 R2)).

И теорема P4_holds_formalized доказывает: P4_formalized истинно. Свидетель первой части — постоянный процесс const_process 0, простейший из процессов Коши; замкнутость относительно произведения и суммы доказана отдельными леммами процессной арифметики.

Здесь нужна точность — и глава на ней настаивает с самого начала изложения формализации. Файл ProcessFourPrinciples.v не формализует весь онтологический тезис $P 4$ одной теоремой. Он фиксирует его процессное ядро: существование процессов Коши и замкнутость базовых арифметических операций над ними. Философская формула $P 4$ — <<всякая система в момент конечна, бесконечность есть свойство процесса>> — шире этого ядра. P4_formalized есть машинно-проверяемый формальный след этой формулы, а не её полный эквивалент. Доказана — и доказана честно — именно конъюнкция трёх процессных утверждений; и когда глава далее говорит, что << $P 4$ доказан в Rocq>>, это следует читать в этом точном смысле: доказан формальный процессный след $P 4$ , предикат P4_formalized.

Почему формализация устроена как утверждение о наличии процессов, а не как прямая запись <<завершённой бесконечности нет>>? Не оттого, что отрицательное утверждение нельзя записать в Rocq: записать можно, Rocq доказывает утверждения вида <<не существует $x$ со свойством $P$ >> и <<из $P$ следует ложь>> совершенно обычным образом, и § 1.5 покажет такое доказательство в самом репозитории. Дело в другом: голая фраза <<завершённой бесконечности нет>> требует точного формального носителя — определения, что именно считать завершённым бесконечным объектом. Поэтому формализация и идёт двумя путями: здесь, в ProcessFourPrinciples.v, она строит утвердительное ядро (процессы Коши есть); а несовместимость завершённой бесконечности с $P 4$ доказывается отдельно, в файлах § 1.5, и доказывается лишь после того, как там вводятся точные определения завершённого бесконечного объекта и стадийной ограниченности.

Файл идёт дальше и перечисляет именованные образцы процессов. В нём объявлен индуктивный тип ProcessInstance — ровно двенадцать конструкторов, и каждый назван по определённому роду процесса: арифметический процесс, процесс-произведение, процесс частичных сумм ряда, процесс разностного отношения (производная), процесс римановых сумм (интеграл), процесс пикаровских итераций (решение обыкновенного дифференциального уравнения) и так далее.³ И здесь — снова точность. ProcessInstance есть индуктивный тип меток: двенадцать конструкторов-ярлыков, каждый из которых называет род процессного паттерна. Леммы twelve_instances и all_instances_nodup доказывают про список этих меток ровно две вещи — что он длины двенадцать и что в нём нет повторов. Это не есть само по себе доказательство существования двенадцати конкретных процессов Коши со всеми их аналитическими свойствами: соответствующие построения и теоремы — производная как процесс, интеграл как процесс и прочее — живут в отдельных файлах процессной части репозитория. ProcessInstance фиксирует номенклатуру двенадцати паттернов; их содержательная разработка — предмет других файлов и других глав тома.

$P 4$ {P4} как онтологический тезис

Позитивная формализация § 1.2.2 говорит, что процессы Коши есть и ведут себя как замкнутая арифметическая область. Онтологический тезис $P 4$ добавляет к этому утверждение о статусе: процесс есть то, чем бесконечное входит в математику, — и единственное, чем оно входит. Бесконечность как схема, а не как объект. В разметке E/R/R это значит: бесконечность — правило, не элемент (разбор § 1.8.3).

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

$P 4$ как онтологический тезис утверждает: математике достаточно бесконечности-как-схемы, и только она и осмысленна. Натуральный ряд есть схема (правило построения), а не объект (завершённое множество). Процесс $2$ есть схема рациональных приближений, а не объект (готовая точка). Это — то же различение <<данные против поведения>>, которое Глава III.3 ввела для счётности: завершённый объект был бы данными, конечной готовой записью; схема есть поведение, способность отвечать на запрос <<дай шаг $n$ >>. $P 4$ говорит: бесконечное входит в математику только как поведение.

Здесь стоит остановиться и свести воедино то, что глава уже несколько раз разграничивала по ходу, — ибо смешение этих вещей и есть типовая ошибка, которой $P 4$ особенно легко поддаётся. У $P 4$ три различных уровня, и они не тождественны.

Первый уровень — онтологический принцип: всякая система в момент конечна, бесконечность есть свойство процесса, а не объекта. Это философско-методологический тезис ToS, формулировка из раздела 2.2.4 (§ 1.1).

Второй уровень — формальный предикат P4_formalized из ProcessFourPrinciples.v: процессы Коши существуют, и базовые арифметические операции сохраняют свойство Коши. Это машинно-проверяемый процессный след онтологического принципа, доказанный теоремой P4_holds_formalized.

{ Третий уровень — prohibition-теоремы файлов P4CompletedInfinity.v и P4Prohibits*: при специальных определениях CompletedInfSet, P4_stage_bounded и bridge завершённая бесконечность ведёт к противоречию. }

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

Уровень	Содержание	Статус
Онтологический $P 4$	Всякая система в момент конечна; бесконечность — свойство процесса, не объекта	Философско-мето-до-ло-ги-чес-кий принцип ToS
`P4_formalized`	Процессы Коши существуют; сумма и произведение сохраняют свойство Коши	Доказано в `Process\-Four\-Principles.v`
Prohibition-слой	`CompletedInfSet` $\land$ `P4_stage_bounded` $\land$ `bridge` $\to$ `False`	Доказано в `P4Comple\-ted\-In\-fi\-ni\-ty.v`

Формальные уровни — второй и третий — не тождественны философскому $P 4$ первого уровня; но вместе они дают ему сильную машинно-проверяемую опору. Именно так — как опору, а не как полный эквивалент, — и следует понимать все дальнейшие ссылки главы на Rocq-формализацию.

Формальный статус: какие аксиомы стоят за $P 4$ {P4}

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

В intended-foundation слое ToS выделены две логические аксиомы, и обе объявлены в одном файле — ToS_Axioms.v.⁴ Первая — $L 3$ , закон исключённого третьего: для всякого высказывания $P$ верно $P \lor \neg P$ . В Rocq это стандартная аксиома classic; ToS заимствует её из стандартной библиотеки и реэкспортирует. Вторая — $L 4$ , закон достаточного основания в формализованном виде: из доказанного существования можно извлечь свидетеля. Формально — аксиома L4_witness: для всякого типа $A$ и предиката $P$ на нём, если $\exists x, P (x)$ , то можно предъявить конкретный $x$ вместе с доказательством $P (x)$ .

Слова <<выделены две аксиомы>> относятся к intended-foundation слою — к тому, какие допущения ToS намеренно кладёт в основание. Технически в отдельных файлах репозитория могут встречаться локальные объявления и параметры — скажем, локальное переобъявление classic в одном из файлов оснований или неинтерпретированный параметр в файле о $Π_{1}^{1}$ -выделении (о нём § 1.5). Их следует отличать от фундаментальных логических аксиом теории: локальное объявление уже принятой classic ничего нового не добавляет, а объявленный параметр — это не логическая аксиома выбора или бесконечности. Фундаментальных логических аксиом ToS — две.

Здесь нужна особая точность, потому что $L 4$ легко принять за аксиому выбора. L4_witness не является аксиомой выбора в том сет-теоретическом смысле, в каком выбор есть одновременное извлечение представителей из завершённого семейства множеств: аксиома выбора берёт целое семейство непустых множеств сразу и для каждого его члена — своего представителя; $L 4$ извлекает свидетеля из одного экзистенциального высказывания. В онтологическом смысле ToS это и есть нужное различение: $L 4$ говорит, что единичное существование определённо — если нечто есть, оно есть нечто опознаваемое, — а не санкционирует завершённый одновременный выбор по произвольной совокупности.

Но было бы неточно сказать, что L4_witness <<не позволяет выбора>> или <<неизмеримо слабее аксиомы выбора>> в обычном техническом смысле. По своей форме — полиморфный переход от exists к sig, от доказательства существования к паре <<свидетель плюс доказательство>> — L4_witness есть принцип неопределённой дескрипции, и в типо-теоретическом смысле он обладает choice-подобной силой: имея семейство доказательств существования, из него можно построить функцию, выдающую свидетеля по индексу. Поэтому глава различает две вещи. Онтологическая аксиома выбора — это завершённый одновременный выбор по завершённому семейству; такого $L 4$ не санкционирует, и в этом смысле ToS им и не пользуется. Техническая же сила L4_witness как принципа неопределённой дескрипции — реальна, и выдавать её за нечто <<неизмеримо слабое всякого выбора>> не следует.

Существенно другое: ни аксиомы бесконечности, ни сет-теоретической аксиомы выбора среди оснований ToS нет. Этому в репозитории посвящён отдельный файл — ProcessAxiomAudit.v.⁵ { Здесь снова нужна честность относительно того, что этот файл делает. ProcessAxiomAudit.v — не автоматический обходчик зависимостей, не теорема, машинно перебирающая весь репозиторий. Сам файл указывает, что опирается на результаты команды Print Assumptions, запускаемой отдельно; внутри же Rocq он фиксирует и формализует сводку этого аудита — классифицирует зависимости ключевых результатов и закрепляет мета-классификации. Его теорема axiom_minimal — формализованная документация вывода <<формализация аксиоматически минимальна: ни аксиомы бесконечности, ни аксиомы выбора, ни аксиомы унивалентности, ни аксиомы функциональной экстенсиональности>>, — а не сканер, который этот вывод сам бы и проверил перебором. Читать его следует как документированный мета-аудит, основанный на Print Assumptions. С этой оговоркой сводка такова: результаты процессной части формализации зависят только от classic, и лишь изредка — от $L 4$ , причём $L 4$ локализован в одном файле, посвящённом вариационному принципу. Так что препринт ToS, говорящий о <<единственной аксиоме classic>>, и файл ToS_Axioms.v, объявляющий две аксиомы, друг другу не противоречат: процессная часть действительно обходится одним $L 3$ , тогда как $L 4$ принадлежит основаниям и в процессной математике почти не востребован. }

{ Подытожим формальный статус. $P 4$ — не аксиома. В файле ProcessFourPrinciples.v формальный след $P 4$ определён (как предикат P4_formalized) и доказан (теоремой P4_holds_formalized); доказательство опирается лишь на classic и процессную арифметику. Когда глава говорит, что $P 4$ <<доказан в Rocq>>, имеется в виду именно это: доказан машинно-проверяемый процессный след принципа — предикат P4_formalized, — а не весь онтологический тезис целиком. Чтобы увидеть, откуда принцип берётся содержательно — из каких начал ToS он вытекает, — перейдём к следующему разделу. }

Откуда берётся $P 4$ {P4}

Деривация из законов логики

$P 4$ выводится — из начал, уже принятых в Части I. Изложение ToS даёт этому выводу точную форму: в том самом разделе 2.2.4, откуда взята формулировка $P 4$ , принцип выводится из двух законов логики — $L 1$ и $L 5$ , — и вывод занимает шесть шагов.⁶

Ход его таков. По $L 5$ (порядок, иерархическое измерение) всякий уровень должен быть завершён прежде, чем начнутся операции уровнем выше: завершённость значит, что все элементы уровня $n$ определены до того, как пойдут операции уровня $n + 1$ . Различение, как установила Часть I, есть акт — не мгновенный готовый факт, а совершаемая операция. Допустим теперь, что некоторая система в момент $t$ имеет бесконечно много элементов; это значило бы, что бесконечно много различений уже совершено. Но каждое различение есть акт; бесконечное число совершённых актов потребовало бы либо бесконечного прошедшего времени (что противоречит словам <<в момент $t$ >>), либо бесконечного числа актов, совершённых в конечное время без последовательного порядка (что противоречит $L 5$ ). Следовательно, в любой момент $t$ совершено лишь конечно много различений — всякая система в момент конечна. А бесконечность входит как качество процесса: процесс добавления элементов не имеет границы — для всякого $n$ достижимо $n + 1$ , — но ни в какой момент процесс не завершён. Это и есть $P 4$ , и это в точности его формулировка из § 1.1.

$P 4$ , стало быть, есть содержательно выводимое следствие уже принятых начал: деривация раздела 2.2.4 получает его из $L 1$ и $L 5$ , ничего к основаниям ToS не добавляя. Но здесь нужно сразу сделать оговорку, без которой слово <<выводится>> вводило бы в заблуждение. Эта деривация — содержательная, философско-мето-до-ло-ги-чес-кая; она проведена в изложении ToS, не в Rocq. Rocq-формализация не воспроизводит цепочку $L 1 \land L 5 \Rightarrow P 4$ как доказанную теорему. Файл ProcessFourPrinciples.v не выводит $P 4$ из законов логики — он доказывает формальный процессный предикат P4_formalized (через постоянный процесс и леммы замыкания, § 1.2.2); более того, в этом файле $P 4$ характеризуется как самостоятельный — теорема P4_independent устанавливает существование процесса Коши на любом уровне безотносительно к прочим принципам. Так что <<выводится>> здесь и <<доказан в Rocq>> § 1.2 — два разных утверждения о двух разных уровнях (см. таблицу § 1.2.3): первое — об онтологической деривации принципа, второе — о машинно-проверяемом процессном следе. Глава держит их раздельно и не выдаёт одно за другое.

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

Операциональная делимость: атомарность относительна

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

Приложим это к бесконечному делению. Завершённая бесконечность в одном из своих обличий есть требование, чтобы все различения внутри некоторого предмета были проведены сразу — чтобы бесконечная делимость была не процессом, а наличным фактом, готовым результатом всех делений разом. Но операциональная делимость как раз и говорит, что делимость есть акт, а не наличный факт. Нельзя <<уже провести>> бесконечное число различений; различение совершается, и всякое конкретное совершённое различение конечно. $P 4$ есть приложение этого мотива к пределу: абсолютная, завершённая бесконечная делимость невозможна не оттого, что трудна, а оттого, что <<завершённая>> противоречит <<делимости как акту>>.

Множество как режим: список первичнее множества

Второй мотив — понимание множества как режима рассмотрения. Часть I проводила различение между списком и множеством. Список первичен: это последовательность элементов, выписанная в порядке, как она была построена. Множество есть список, взятый в особом режиме — в режиме, где порядок и кратность намеренно забыты, где оператор условился смотреть только на принадлежность. Множество не отдельная сущность рядом со списком; это список под определённым углом зрения.

Завершённая бесконечность подразумевает <<бесконечный список, составленный целиком>>. Но составление списка есть процесс: элементы выписываются один за другим. Мотив <<множество как режим>> показывает, что и бесконечное множество мыслимо лишь как режим рассмотрения некоторого списка — а бесконечный список есть процесс выписывания, который не завершается. $P 4$ есть приложение и этого мотива: процесс составления бесконечного списка не завершается никогда, и значит, <<завершённое бесконечное множество>> есть режим рассмотрения несуществующего объекта — готового бесконечного списка.

Позитивное существование: быть значит быть актуализированным

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

Здесь $P 4$ ближе всего к своему истоку. Если существовать значит быть актуализированным, а актуализация совершается по шагам, то <<завершённая бесконечность>> требует невозможного: бесконечного количества актуализаций, осуществлённых не по шагам, а сразу. $P 4$ есть прямое следствие позитивного понимания существования, приложенное к бесконечным случаям.

$P 4$ {P4} как специализация принятых начал

Три мотива сходятся к одному. Операциональная делимость: делимость есть акт, бесконечная делимость-как-факт невозможна. Множество как режим: бесконечное множество есть режим рассмотрения бесконечного списка, а тот есть незавершающийся процесс. Позитивное существование: быть значит быть актуализированным, бесконечная совокупность одновременных актуализаций невозможна. Каждый из трёх, приложенный к случаю бесконечного, даёт одно и то же: бесконечность входит в математику как схема построения, не как завершённый объект. Это и есть $P 4$ .

$P 4$ , стало быть, есть специализация трёх уже принятых мотивов для случая бесконечности — и, в содержательной деривации раздела 2.2.4, следствие, выводимое из $L 1$ и $L 5$ . Том замечает, что у начал, заложенных в Части I, есть определённое следствие, касающееся бесконечного, и даёт этому следствию имя. При этом — напомним оговорку § 1.3.1 — следует держать раздельно два уровня: содержательно $P 4$ выводится из мотивов и из $L 1, L 5$ ; формально в Rocq доказан не этот вывод, а процессный предикат P4_formalized (§ 1.2.2). Ни на одном из уровней $P 4$ не есть отдельная аксиома: он либо выводится содержательно, либо предстаёт доказанным процессным следом. Принцип, который раскрывает в основаниях уже заложенное, не требует от читателя отдельного доверия сверх того, какое уже отдано законам логики Части I: $P 4$ в этом смысле бесплатен — он стоит ровно столько, сколько уже принятые начала, и ни на йоту больше.

Где $P 4$ {P4} уже работал

Принцип, опознаваемый задним числом

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

Натуральный ряд как индуктивный тип (Часть II)

Самое раннее и самое чистое появление $P 4$ — в Части II, при построении натурального ряда. Натуральный ряд введён там не как множество, а как индуктивный тип: задано правило — нуль есть число, и за всяким числом следует число, — и натуральные числа суть в точности то, что этим правилом порождается.

Это уже $P 4$ в действии, хотя имя ещё не названо. Индуктивный тип есть схема построения, не завершённый объект. Всякое конкретное натуральное число — сто, тысяча, любое заданное — доступно: оно строится за конечное число применений правила. <<Все натуральные числа как готовое собранное множество>> в этой картине не фигурируют вовсе — и не потому, что забыты, а потому, что индуктивный тип их и не предполагает. Rocq реализует это прямо: натуральный ряд nat есть индуктивный тип, и всякое рассуждение о всех натуральных числах — всякая сумма, всякий предел, всякая проверка сходимости — проходит через принцип индукции, а не через обращение к <<множеству всех натуральных>>. Принцип индукции есть правило вывода; он не требует, чтобы натуральные числа были где-то собраны вместе. Часть II, строя счёт, уже стояла на $P 4$ .

Нужна, впрочем, точная оговорка. Формально nat существует — как тип языка Rocq, и по этому типу можно квантифицировать: запись <<для всякого $n : ‘ na t ‘$ >> совершенно законна. ToS этого формального факта не отрицает: тип nat есть. ToS отказывается лишь от одного прочтения этого типа — от прочтения, по которому nat был бы завершённой актуальностью всех натуральных чисел, готовым собранным множеством. nat здесь понимается как индуктивная схема порождения и рассуждения; квантор <<для всякого $n$ >> читается как отсылка к этой схеме, к принципу индукции, а не к обзору готового бесконечного собрания. Различение это — между типом как схемой и типом как завершённым множеством — будет важно во всей Части IV.

Незавершённость как онтология (Часть I)

Ещё раньше — в Части I — $P 4$ присутствовал в виде общего онтологического мотива, который можно назвать незавершённостью. Часть I, разбирая акт различения и иерархию уровней, проводила мысль, что процесс не обязан завершаться в готовый предмет, чтобы быть полноценным, — что незавершённость есть не изъян, не нехватка итога, а позитивная онтологическая черта. Предмет, который разворачивается и не свёртывается в точку, не <<хуже>> завершённого предмета; он другого рода.

Это прямо подготавливало $P 4$ . Если незавершённость — полноценный способ существовать, то бесконечность-как-схема (которая именно не завершается) не нуждается в оправдании ссылкой на завершённый объект. Часть III этим уже воспользовалась явно: $2$ был там разобран как процесс, который не свёртывается в готовую точку и в этом своём несвёртывании полноценен. Незавершённость из онтологического мотива Части I стала рабочим инструментом Части III — и обе опирались на то, что теперь зовётся $P 4$ .

Данные против поведения (Часть III)

Третий возврат — к Главе III.3, к различению данных и поведения. Разбирая счётность рациональных чисел, та глава развела две вещи: данные — конечную готовую запись, которую можно предъявить целиком, — и поведение — способность отвечать на запросы, которая целиком не предъявляется, а проявляется по требованию. Рациональное число есть данные: пара целых, конечная запись. Процесс есть поведение: правило, дающее ответ на запрос <<значение на шаге $n$ >>.

Глава III.3 показала, что счётность — свойство данных, а не поведения: перечислимы конечные записи, и Калкин–Уилфов обход рациональных чисел перечисляет именно их. К пространству же поведений понятие обхода неприложимо в том же смысле, в каком оно применимо к конечным данным, — и здесь нужна точность, потому что вычислимые поведения, заданные программами, как раз перечислимы: их можно обойти как программы. Несчётность относится не к вычислимым процессам, а к пространству всех процессных поведений $N \to Q$ (или к соответствующему классу процессов Коши): оно имеет иной статус, нежели конечные данные. Это различение есть $P 4$ , взятый со стороны эпистемологии: завершённый объект был бы данными, конечной готовой вещью; бесконечность-как-схема есть поведение. Когда Часть IV в следующих главах будет доказывать несчётность процессов, она будет опираться ровно на это — и Глава 4.4 проведёт различение между перечислимыми вычислимыми процессами и непересчётным пространством процессных поведений со всей нужной аккуратностью. Корень — здесь, в Главе III.3, и корень этот есть $P 4$ .

Иррациональности как процессы (Часть III)

Четвёртый и самый прямой возврат — к Главе III.4, непосредственно предшествующей этой. Та глава показала, что $2$ — не позиция на рациональной разметке, не готовая точка, лежащая где-то отдельно от приближающих её дробей, а процесс: разворачивающаяся последовательность рациональных приближений. Глава III.4 разобрала этот процесс по составу — как функциональную систему с правилами, ролями и элементами, — и показала на примере двух разных процессов, что процессное представление $2$ не обязано быть единственным: разные правила приближения могут совпадать на первых шагах и расходиться дальше, по-разному ведя себя по качеству приближения. Более сильный тезис — что все процессы, дающие $2$ , образуют единый открытый класс, эквивалентный относительно некоторого отношения эквивалентности процессов, — Глава III.4 не доказывала; он есть программа дальнейшей формализации и будет выражен через отношение эквивалентности процессов в последующих главах Части IV.

Это $P 4$ уже почти в полную силу, но ещё на одном частном примере — на одной иррациональности. Глава III.4 показала $P 4$ в работе; настоящая глава его формулирует; следующая, Глава 4.2, обобщает — строит процесс вообще как тип, для которого $2$ был лишь первым образцом. Так Глава III.4 и есть непосредственный мост: она оставила изложение ровно там, где требовалось назвать принцип и обобщить конструкцию.

Что показывают возвраты

Четыре возврата — к индуктивному nat Части II, к незавершённости Части I, к различению данных и поведения Главы III.3, к числу-процессу Главы III.4 — показывают одно. $P 4$ не вводится в этой главе впервые; он лишь называется здесь впервые. Принцип работал в томе с самого построения натурального ряда, действовал в четырёх независимых местах, на разном материале, и всякий раз — одним и тем же образом: бесконечное бралось как схема, не как объект. Глава не предлагает читателю поверить в новое допущение; она показывает ему, что он уже четырежды видел $P 4$ в деле, и теперь лишь подводит под увиденное черту.

$P 4$ {P4} и классические аксиомы

Ненужность и несовместимость

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

Rocq-формализация ToS содержит оба слоя — и содержит их раздельно, как два поколения файлов. Более того, она сама это различие документирует: один из файлов в шапке прямо описывает, что изменилось между поколениями.⁷ Настоящий раздел разбирает оба слоя по порядку: сперва ранний, слой ненужности (§ 1.5.2–1.5.3), затем поздний, слой несовместимости (§ 1.5.4–1.5.6), а в § 1.5.7 показывает, как они соотносятся. Поспешно сказать << $P 4$ запрещает аксиому выбора>> — значит свалить два слоя в один и потерять точность, которой формализация как раз достигает.

Слой первый: аксиома не нужна

{ Ранний слой формализации представлен группой файлов с общим именем вида P4_Eliminates_* — по одному на каждую аксиому. Каждый такой файл доказывает утверждение одного и того же рода: та работа, ради которой стандартная математика вводит данную аксиому, в $P 4$ -онтологии выполняется без неё — средствами, которые $P 4$ и без того предоставляет. Аксиома не опровергается; она оказывается лишней. Назовём этот слой слоем ненужности и разберём его на четырёх аксиомах. }

Аксиома бесконечности. Файл P4_Eliminates_Infinity.v показывает: всё, ради чего вводится аксиома бесконечности, делается через индуктивный тип nat.⁸ В файле построены и доказаны: принцип индукции (как встроенное правило, не аксиома), частичные суммы, предикат сходимости, сильная индукция, факториал, ограниченность конечного списка. Итоговая теорема P4_eliminates_Infinity — не отрицание аксиомы бесконечности; это конъюнкция четырёх позитивных фактов: принцип индукции работает, всякое $n$ конечно, факториал пяти равен ста двадцати, частичная сумма первых натуральных чисел вычисляется. Смысл теоремы — ровно <<вот демонстрация: всё это работает, и аксиома бесконечности для этого не понадобилась>>. Аксиома не опровергнута — показано, что она не нужна.

Аксиома выбора. Файл P4_Eliminates_AC.v устроен так же.⁹ В $P 4$ -онтологии всякое множество на стадии $N$ есть конечный список — процесс, взятый до шага $N$ . Выбор представителя из конечного непустого списка не требует аксиомы: можно взять первый элемент — голову списка. Это $L 5$ -разрешение: канонический выбор в порядке построения. Файл доказывает леммы конечного выбора, конечный вариант леммы Цорна (максимум списка) и теорему о выборе по конечному фронту: для фиксированного конечного $N$ и непустых списков $F (n)$ при $n < N$ функция выбора строится явно — как взятие головы.¹⁰ Этим выбор и исчерпывается на уровне ненужности: для конечного фронта аксиома не требуется. У того же файла есть и теорема без ограничения на $N$ — для семейства family с индексом по всем натуральным числам; её статус тоньше, и глава вернётся к нему в § 1.5.6. Здесь же зафиксируем бесспорное: для того выбора, который $P 4$ -онтология реально совершает — выбора из конечных списков на конечном фронте, — аксиома выбора не нужна.

Трансфинитная рекурсия. Файл P4_Eliminates_ATR.v берёт арифметическую трансфинитную рекурсию — в обратной математике это аксиома.¹¹ В файле объявлен индуктивный тип ординалов — с конструкторами нуля, следующего и предельного, — и трансфинитная рекурсия определена как обыкновенная Fixpoint-функция по этому типу. Термination-checker Rocq принимает её как структурную рекурсию. Итог: трансфинитная рекурсия — не аксиома, а определение. То, что в обратной математике постулируется, в $P 4$ -онтологии просто записывается как функция.

Выделение по формулам второго порядка. Файл P4_Eliminates_Pi11.v разбирает $Π_{1}^{1}$ -выделение — схему, выделяющую подмножество формулой с квантором по всем функциям из натуральных чисел в натуральные.¹² Файл вводит $P 4$ -ограниченное чтение функциональной квантификации: вместо квантора по всем функциям $N \to N$ берётся квантор по программным кодам $c : N$ , а функция восстанавливается через параметр eval_program (<<запустить код $c$ на входе $n$ >>). При таком чтении квантор <<по всем функциям>> сводится к квантору <<по всем кодам $c$ >> — к обычной арифметической квантификации по натуральным числам, и $Π_{1}^{1}$ -выделение даёт арифметический аналог соответствующих рассуждений.

Здесь нужна точная оговорка, и глава на ней настаивает. Файл не доказывает, что всякая классическая функция $N \to N$ имеет программный код — такого утверждения в нём нет. Он переопределяет режим квантификации по функциям как квантификацию по кодам; это $P 4$ -ограниченное чтение, а не теорема о совпадении класса всех функций с классом программ. И eval_program здесь — не доказанное утверждение и не определённая функция, а неинтерпретированный объявленный параметр: константа без определения, соответствующая универсальной машине Тьюринга и позволяющая говорить о программах внутри Rocq, не строя интерпретатор. Глава отмечает это для точности — и потому, что прочие три файла слоя ненужности обходятся вовсе без подобных объявлений.

Что общего у слоя ненужности

Четыре файла устроены по одному образцу. Ни один не доказывает отрицания аксиомы. Каждый берёт работу, ради которой аксиома вводится, — порождение натуральных чисел, выбор представителя, трансфинитную рекурсию, выделение подмножества, — и выполняет эту работу средствами $P 4$ -онтологии: индуктивным типом, головой списка, Fixpoint-функцией, программным кодом. Итог во всех четырёх случаях один: аксиома не нужна. Это и есть ранний слой — слой переистолкования (так его называет сама формализация): $P 4$ предоставляет альтернативу, и аксиома становится излишней.

Слой ненужности ценен, но у него есть предел. Он говорит: <<вот как обойтись без аксиомы>>. Он не говорит: <<принять аксиому вместе с $P 4$ нельзя>>. Логически он оставляет открытой возможность, что аксиому всё же можно добавить — просто незачем. Эту оставшуюся возможность закрывает второй слой.

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

Поздний слой формализации представлен файлами с именами вида P4Prohibits* и общим для них ядром — файлом P4CompletedInfinity.v.¹³ Этот слой доказывает уже не ненужность, а несовместимость: $P 4$ и завершённая бесконечность вместе ведут к противоречию. Разберём, как именно это устроено — и где проходит граница доказанного.

Файл P4CompletedInfinity.v вводит три определения. Завершённое бесконечное множество — предикат $S$ на натуральных числах, для которого всякое $n$ есть член $S$ (символически: $\forall n, S (n)$ ). $P 4$ -стадийная ограниченность — свойство <<актуальности>>: на всякой стадии число актуальных элементов ограничено сверху некоторым рубежом. Мост — условие, связывающее эти две картины: если $n$ есть член завершённого множества, то $n$ актуально уже на нулевой стадии.

И тогда центральная теорема, completed_inf_contradicts_P4, гласит: завершённое бесконечное множество, $P 4$ -стадийная ограниченность и мост — вместе ведут к противоречию. Доказательство коротко и прозрачно. $P 4$ -стадийная ограниченность даёт для нулевой стадии конкретный рубеж — некоторое число $B$ . Завершённое множество, по определению, содержит всякое натуральное число — в частности, число $B + 1$ . Мост делает $B + 1$ актуальным на нулевой стадии. Но рубеж говорит, что всё актуальное на нулевой стадии не превосходит $B$ , — то есть $B + 1 \leq B$ . Противоречие.

Аксиома выбора во втором слое

Как именно несовместимость распространяется на аксиому выбора, показывает файл P4ProhibitsAC.v.¹⁴ Аксиома выбора по натуральному ряду — утверждение, что для всякого семейства непустых списков, индексированного натуральными числами, существует функция выбора. Файл замечает: такая функция выбора есть сама по себе завершённый бесконечный объект — её график (совокупность пар <<индекс, выбранное значение>>) тотален, определён для всякого натурального индекса. Теорема ac_implies_completed доказывает это: из аксиомы выбора по натуральному ряду следует существование функции, чей график есть завершённое бесконечное множество. А тогда — по теореме предыдущего параграфа — вместе с $P 4$ -стадийной ограниченностью и мостом получается противоречие.

Здесь нужна точность, и глава на ней настаивает. Файл P4ProhibitsAC.v не доказывает замкнутого утверждения <<аксиома выбора ложна>>. Он доказывает: аксиома выбора порождает завершённый бесконечный объект; а завершённый бесконечный объект вместе с $P 4$ -стадийной ограниченностью и мостом — противоречив. Это условная теорема: противоречие получается при наличии всех трёх посылок. Сила её — в том, что $P 4$ -стадийная ограниченность есть прямая формализация $P 4$ , а мост — естественное условие, связывающее <<быть членом>> с <<быть актуальным>>. Но это всё же утверждение относительно внутренних определений формализации (<<завершённое множество>>, <<стадийная ограниченность>>, <<мост>> — так, как они записаны в P4CompletedInfinity.v), а не утверждение <<аксиома выбора противоречива в теории Цермело–Френкеля>>. Формализация доказывает строго определённую, честную и сильную вещь — и ровно её, не больше.

Здесь же снимается кажущееся напряжение между двумя файлами про выбор — ранним P4_Eliminates_AC.v и поздним P4ProhibitsAC.v. Ранний доказывает, что выбор не нужен (голова списка); поздний — что выбор несовместим (порождает завершённую бесконечность). Не противоречие ли? Нет, и разрешение тонкое. Дело в режиме чтения функции выбора. Конечная теорема P4_eliminates_AC_finite (§ 1.5.2) говорит о конечном фронте $N$ : тут функция выбора есть конечный объект, вопрос исчерпан. Но P4_eliminates_AC.v содержит и теорему для семейства с индексом по всем натуральным числам. Такую тотальную функцию выбора можно прочитать двояко. Если читать её как процессное правило — предписание, выдающее выбор по любому предъявленному индексу, — она $P 4$ -совместима: на каждый запрос даётся конечный ответ, завершённого объекта нет. Если же читать её как завершённый график — собранную воедино тотальную совокупность пар $(i, f (i))$ для всех $i$ сразу, — мы попадаем ровно в режим P4ProhibitsAC.v: такой график есть завершённая бесконечность, и вместе со стадийной ограниченностью и мостом он даёт противоречие. Различие двух файлов, стало быть, не сводится к <<конечный список против бесконечного семейства>>; оно — в режиме чтения самой функции выбора: процессное правило или завершённый график. $P 4$ оставляет первое и отсекает второе.

Как соотносятся два слоя

{ Как соотносятся два слоя, формализация ToS тоже фиксирует — файлом P4ProhibitionSynthesis.v.¹⁵ Содержательно соотношение таково: слой несовместимости сильнее слоя ненужности — если нечто несовместимо с $P 4$ , то $P 4$ тем самым уже доставляет ему альтернативу, ведь невозможное приходится чем-то заменять; обратное же неверно — наличие альтернативы не означает несовместимости исходного. }

{ Файл содержит и теорему с говорящим именем — prohibition_implies_reinterpretation. Но здесь важно не переоценить её. По формулировке она гласит: если завершённая бесконечность несовместима с $P 4$ -ограниченностью при мосте, то имеет место потенциальная бесконечность. По доказательству же она устроена просто: посылку она не использует — доказывает заключение напрямую, возвращая уже доказанную в репозитории лемму существования потенциальной бесконечности (potential_inf_exists). Поэтому prohibition_implies_reinterpretation не есть формализация нетривиальной логической зависимости <<запрет влечёт переистолкование>>. Это — скорее синтетическая сводка: документированная фиксация того, что в репозитории есть prohibition-теорема и отдельно есть доказанная альтернатива (потенциальная бесконечность). Подавать её как нетривиальное доказательство логического следования не следует; содержательное соотношение слоёв — то, что в предыдущем абзаце, — верно, но обосновано оно рассуждением, а не этой конкретной теоремой. }

Сведём оба слоя воедино. Когда глава говорит, что $P 4$ отсекает аксиому бесконечности или аксиому выбора, она имеет в виду точно следующее. Во-первых (слой ненужности): работа этих аксиом в $P 4$ -онтологии выполняется без них — индуктивным типом, головой списка, Fixpoint-функцией, программным кодом; проверено четырьмя файлами P4_Eliminates_* и подтверждено аудитом ProcessAxiomAudit.v. Во-вторых (слой несовместимости): завершённая бесконечность — в том виде, в каком она формализована предикатами P4CompletedInfinity.v, — несовместима с $P 4$ -стадийной ограниченностью при наличии моста; и аксиома выбора по натуральному ряду порождает именно такую завершённую бесконечность. Это условные теоремы относительно внутренних определений формализации — сильные и честные, но именно условные. Чего глава не утверждает — так это что в Rocq доказано замкнутое <<аксиома выбора ложна>> в смысле теории множеств. Отсечение реально и формально проверено; его точный смысл задаётся двумя слоями, а не лозунгом.

Что $P 4$ {P4} оставляет

Отсечение и сохранение — две стороны

Раздел § 1.5 показал, что $P 4$ отсекает. Естественно прочесть это как обеднение: математика лишается аксиом, значит, лишается и возможностей. Настоящий раздел показывает, что прочтение это неверно. $P 4$ отсекает завершённую бесконечность — но всё, что в математике делается без обращения к завершённой бесконечности, а это подавляющая её часть, остаётся в полной силе. И тот же файл формализации, что доказывает несовместимость, доказывает рядом и сохранение: теорема P4_preserves_three устанавливает, что $P 4$ совместим с тремя вещами — потенциальной бесконечностью, конечным выбором и индуктивными типами. Отсечение и сохранение — две стороны одного принципа, и вторую надо предъявить так же отчётливо, как первую.

Натуральные, целые, рациональные числа

Прежде всего $P 4$ оставляет в силе всё построение Частей II и III. Натуральный ряд — индуктивный тип, схема построения; он не только совместим с $P 4$ , он есть образцовый пример того, чем $P 4$ разрешает бесконечности быть. Целые числа — двусторонняя координатная разметка, надстроенная над натуральным рядом; рациональные числа — соразмерная разметка с дробным шагом. Ни одна из этих конструкций не обращается к завершённой бесконечности: каждое целое, каждое рациональное число есть конечная запись, строящаяся за конечное число шагов. Всё, что Часть III доказала о целых и рациональных числах, — включая их перечислимость — стоит при $P 4$ неколебимо. Перечислимость, более того, есть свойство, которое $P 4$ как раз и проясняет: она говорит о наличии процедуры обхода, то есть схемы, а не о готовом собранном множестве.

Конечные совокупности и индукция

$P 4$ оставляет конечные совокупности — целиком и без оговорок. Конечный список можно взять как готовый предмет: он и есть готовый предмет, его построение завершается. Множество как режим рассмотрения конечного списка — законно. Выбор представителя из конечного непустого списка — законен, он есть взятие головы (§ 1.5.2). $P 4$ ограничивает завершённость бесконечного, а не завершённость как таковую; конечное завершается по самой своей природе.

$P 4$ оставляет и индукцию — полностью. Принцип индукции есть правило вывода: чтобы доказать утверждение для всех натуральных чисел, достаточно доказать его для нуля и доказать переход. Это правило не требует, чтобы натуральные числа были собраны в готовое множество; оно требует лишь схемы их построения, а схема и есть индуктивный тип. Сильная индукция, рекурсия, определения через Fixpoint — всё это $P 4$ оставляет, и файл P4_Eliminates_Infinity.v (§ 1.5.2) есть прямая демонстрация: индукция, рекурсия, частичные суммы, факториал — все работают, и работают без аксиомы бесконечности.

Конструктивные доказательства существования

$P 4$ оставляет доказательства существования — но в определённом их виде. Доказать, что нечто существует, при $P 4$ значит предъявить это нечто: указать свидетеля, дать конструкцию, описать правило, по которому объект строится. Это и есть содержание $L 4$ (§ 1.2.4): из доказанного существования извлекается свидетель. Доказательство существования <<через предъявление>> полностью совместимо с $P 4$ , потому что предъявленный свидетель есть конечный объект или конечно описанная схема.

Что $P 4$ не оставляет — так это доказательства существования <<через невозможность отсутствия>> в той их форме, где свидетель не предъявляется и не может быть предъявлен в принципе. Но это ограничение мягче, чем кажется: $L 3$ (закон исключённого третьего) ToS сохраняет (§ 1.7 разберёт это подробно), и потому рассуждение от противного остаётся доступным. $P 4$ задевает не закон исключённого третьего, а лишь обращение к завершённой бесконечности как к объекту, по которому ведётся рассуждение. Подавляющее большинство классических доказательств существования либо уже конструктивны, либо переводятся в конструктивную форму — и остаются в силе.

Процессы и анализ

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

А на процессах строится анализ. Глава III.4 уже показала, как $2$ становится процессом и как операционально определяются сходимость и свойство Коши; следующие части тома развернут на этом основании дифференцирование, интегрирование, ряды, решение дифференциальных уравнений. В репозитории ToS уже есть значительный процессный корпус анализа — файлы по теореме о промежуточном значении, теореме о крайних значениях, теоремам Больцано–Вейерштрасса и Гейне–Бореля и другим. Подробный статус каждого из этих результатов — что именно доказано, на какие определения опирается, какие логические средства использует — следует разбирать в соответствующих главах тома, и глава не станет здесь забегать вперёд. Существенно для § 1.6 одно: процессная онтология анализ не разрушает, а даёт ему рабочий материал. Анализ, который классическая математика обыкновенно ведёт над завершённым континуумом, $P 4$ -онтология ведёт над процессами. При этом не следует ожидать, что всякая формулировка перейдёт дословно: часть определений и теорем в процессном анализе получает изменённый, операциональный вид — но содержательно анализ остаётся анализом, а его материал, по разбору § 1.5, становится более прочным, а не более бедным.

Чего стоит отсечение

Сведём баланс. $P 4$ оставляет: натуральные, целые, рациональные числа; конечные совокупности и операции над ними; индукцию, рекурсию, сильную индукцию; конструктивные доказательства существования; процессы и весь анализ, на процессах построенный. Это — не остаток, уцелевший после отсечения, а основной корпус математики. $P 4$ отсекает завершённую бесконечность — объект, который при ближайшем рассмотрении (§ 1.5) оказывается либо ненужным, либо несовместимым с принятой онтологией. Отсекается, иначе говоря, не рабочая часть математики, а определённое допущение о природе бесконечного — допущение, без которого рабочая часть прекрасно стоит. Что именно при этом теряется и почему потеря необременительна — это предмет уже не настоящей главы, а Главы 4.6, замыкающей Часть IV; здесь довольно сказать, что баланс отсечения и сохранения складывается решительно в пользу сохранения.

$P 4$ {P4} и интуиционизм Брауэра

Зачем сравнение

У $P 4$ есть важный исторический предшественник — интуиционистская программа в основаниях математики, начатая Лёйтзеном Брауэром в начале двадцатого века и развитая затем Аренда Гейтингом и другими. Сравнение с нею не дань учёности: оно проясняет место ToS точнее, чем любое описание изнутри. Интуиционизм первым в Новое время отказался считать завершённую бесконечность онтологически первичной — и потому, увидев, где ToS с интуиционизмом сходится и где расходится, читатель увидит и то, чем позиция ToS своеобразна.

В чём $P 4$ {P4} сходится с интуиционизмом

Сходств три, и они существенны.

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

Второе — конструктивность. Интуиционизм требует, чтобы доказательство существования предъявляло объект: <<существует>> значит <<вот оно, построено>>. ToS требует того же — это содержание $L 4$ и общий дух $P 4$ -онтологии (§ 1.6.4). Доказать существование значит дать конструкцию.

Третье — подозрительность к аксиоме выбора. Интуиционизм традиционно отвергает аксиому выбора в её полном виде как раз потому, что та постулирует одновременный выбор по бесконечному семейству — завершённую бесконечность выборов. ToS приходит к тому же заключению — и приходит, как показал § 1.5, через формализованный разбор: полный выбор порождает завершённый бесконечный объект, несовместимый с $P 4$ .

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

В чём $P 4$ {P4} расходится с интуиционизмом

Но есть и расхождение, и оно глубокое — настолько, что обыкновенно эти две позиции считают несовместимыми. Расхождение — в отношении к закону исключённого третьего.

Брауэр отвергает закон исключённого третьего. Для интуициониста утверждение << $P$ или не- $P$ >> не имеет права считаться истинным до тех пор, пока не доказано $P$ либо не доказано не- $P$ ; пока ни то ни другое не построено, нет и основания для дизъюнкции. Интуиционистская логика поэтому неклассическая: в ней не действует ни закон исключённого третьего в полном объёме, ни снятие двойного отрицания.

ToS закон исключённого третьего принимает. Более того — принимает не как добавочную аксиому-уступку, а как один из пяти законов логики, выведенных в Части I из единственного начала. Часть I показала: акт различения, отделяющий $A$ от не- $A$ , по самой своей природе исчерпывающ — он не оставляет третьей области, не отнесённой ни к $A$ , ни к не- $A$ . Эта исчерпанность завершённого акта различения и есть закон исключённого третьего, $L 3$ . В Rocq он входит как аксиома classic (§ 1.2.4) именно потому, что система Rocq конструктивна по построению, а $L 3$ к ней надстраивается; но в ToS $L 3$ — не произвол, а теорема об устройстве различения.

$P 4$ {P4}: конструктивизм с классической логикой

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

Сочетание это редкое — обыкновенно конструктивную онтологию и классическую логику считают тянущими в разные стороны. ToS показывает, как эти две установки могут быть разведены по уровням. Ключ — именно в различении уровней. $L 3$ есть закон о завершённом акте различения: раз акт совершён, $A$ отделено от не- $A$ исчерпывающе. $P 4$ есть принцип о бесконечных совокупностях: бесконечность не завершается в объект. Эти два утверждения о разном — одно об акте, другое о совокупности — и потому не обязаны сталкиваться. Можно держать классическую логику на уровне отдельных завершённых актов различения и при этом держать конструктивную, процессную онтологию на уровне бесконечного. Интуиционизм отверг $L 3$ , потому что связал его именно с завершённой бесконечностью — с <<обзором всех случаев>>. ToS разводит то, что интуиционизм связал, и потому может взять у интуиционизма конструктивную онтологию, не платя за неё отказом от классической логики.

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

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

Мост к построению процесса

Что следует из $P 4$ {P4}

$P 4$ сформулирован дословно, содержательно выведен из $L 1$ и $L 5$ , опознан в прежней работе тома, разобран со стороны того, что он делает излишним и с чем несовместим, и соотнесён с интуиционизмом. Остаётся спросить: что из всего этого следует для построения числа?

Следует вот что. Если всякая система в момент конечна, а бесконечность есть свойство процесса, то в $P 4$ -онтологии действительное число не должно читаться как готовая точка завершённой прямой. Привычная картина мыслит действительное число точкой: $2$ , $π$ , $e$ — каждое есть готовая точка на завершённой числовой прямой, а десятичная запись лишь приближённо эту точку называет. Но завершённая числовая прямая есть завершённая бесконечность — собранное воедино несчётное множество готовых точек, — и $P 4$ такой объект исходным онтологическим носителем не делает.

Это онтологическое утверждение, и его границы стоит очертить сразу. Глава не говорит, что точечная картина ложна или что её надо изгнать из математики. Она говорит, что точка не может быть исходным носителем: исходно дан процесс, а привычная точка восстанавливается позднее — как класс эквивалентности процессов, как режим рассмотрения, в который оператор переходит, когда ему нужно отвлечься от различий между процессами, дающими один и тот же предел. Точку $P 4$ -онтология не отменяет, а переставляет: из первичного объекта она становится производным режимом. Как именно это устроено — предмет Главы 4.3; здесь важно лишь, что <<действительное число не есть готовая точка>> означает не запрет точки, а указание её настоящего, производного места.

Что возможно вместо точки

Что же возможно? Возможно ровно то, что Глава III.4 уже показала на $2$ : процесс — разворачивающаяся по правилу последовательность рациональных приближений. Действительное число в $P 4$ -онтологии есть не точка, а процесс; не завершённый объект, а схема; не данные, а поведение. Глава III.4 установила это для одной иррациональности и разобрала её по составу. Часть IV должна теперь сделать общий шаг: построить процесс вообще как полноценный тип формализации — такой, для которого $2$ был лишь первым образцом, а двенадцать образцов из ProcessFourPrinciples.v (§ 1.2.2) — лишь первыми двенадцатью.

Этот тип в Rocq-формализации ToS называется RealProcess и определяется — предельно просто — как тип функций из натуральных чисел в рациональные, nat -> Q. Каждому шагу $n$ процесс сопоставляет рациональное приближение. Простота определения не случайна: она прямо выражает $P 4$ . Натуральные числа — индуктивный тип, схема; рациональные числа — конечные записи; функция между ними — правило, дающее по запросу <<шаг $n$ >> конечный ответ.

И здесь — последняя в этой главе оговорка о точности. Технически RealProcess := nat -> Q есть в Rocq тип тотальных функций: терм этого типа задаёт значение для любого $n$ , а не только для уже запрошенных. Было бы неверно сказать, что в RealProcess <<нет вообще ничего завершённого>>. ToS читает такой терм операционально: как правило, которое по предъявленному $n$ выдаёт рациональное значение, — и в этом операциональном чтении процесс есть схема, а не собрание. Точное утверждение поэтому такое: RealProcess не есть завершённое множество рациональных значений в сет-теоретическом смысле — завершённой бесконечности как ZFC-объекта в нём нет; но в формальном языке Rocq это именно функциональный объект, тип тотальных функций, и $P 4$ -онтология держится на операциональном прочтении этого объекта, а не на отрицании того, что он — функциональный тип. С этой оговоркой и следует понимать слова о том, что RealProcess есть $P 4$ , записанный как определение типа: он есть $P 4$ при операциональном чтении функции как правила.

Разбор E/R/R: бесконечность как схема, не объект

{ Прежде чем перейти к построению, закрепим разбором E/R/R (Часть I) то, как $P 4$ устроен в разметке элементов, ролей и правил. Эта глава разбирает не числовую систему, а принцип, и разбор здесь меньше о составе, больше о том, какой уровень разметки $P 4$ держит. Оговорка о статусе строже обычного и повторяет три уровня $P 4$ (§ 1.2): онтологический тезис; его машинно-проверяемый след P4_formalized (доказан); и условный prohibition-слой (теоремы при точных определениях завершённой бесконечности). Разбор ведём в онтологическом порядке Rules $\to$ Roles $\to$ Elements.}

Rules — правила (принцип $P 4$ ). $P 4$ есть конституция уровня элементов: бесконечность входит в математику как схема — правило <<нуль есть число; за всяким следует число>>, применимое без конца, — а не как объект, готовое собранное <<всё>> (§ 1.2.3). Содержательно $P 4$ выведен из $L 1$ и $L 5$ (§ 1.3), но именно содержательно: цепочка $L 1 \landL 5 \RightarrowP 4$ в Rocq не доказана, а след $P 4$ (P4_formalized: процессы Коши есть и замкнуты по арифметике) доказан самостоятельно. Prohibition-слой добавляет: при точном определении завершённого бесконечного объекта он с $P 4$ несовместим (P4_Eliminates_Infinity: nat — правило индукции, не готовое множество), причём функция выбора как правило с $P 4$ совместима, а как завершённый график — нет (§ 1.5).

Roles — значимость позиций (закон $L 4$ ). Бесконечность получает роль схемы — потенциально продлеваемого правила, а не наличной совокупности. Всякая стадия играет роль конечной актуализации. И точка (готовое действительное число) под $P 4$ из первичного объекта становится производной ролью — классом эквивалентности процессов, режимом рассмотрения (Глава 4.3): $P 4$ точку не отменяет, а переставляет на её настоящее, производное место.

Elements — носители (закон $L 1$ и сам $P 4$ ). Носителями остаются только конечно актуализированные объекты: всякое натуральное построимо за конечное число шагов, всякая стадия процесса есть конечная рациональная запись. Завершённого бесконечного объекта на уровне элементов нет. Оговорка о точности (§ 1.8.2): тип RealProcess := nat -> Q в Rocq есть тип тотальных функций; $P 4$ держится на операциональном чтении терма (правило, дающее ответ по предъявленному $n$ ), а не на отрицании того, что это функциональный тип.

Сведём разбор в таблицу.

Компонент	Что фиксирует	E/R/R
$P 4$ : бесконечность как схема, не объект	конституция элементов	Rule
след `P4_formalized` (Коши есть, замкнуты)	доказанное ядро	Rule
prohibition-слой (`nat` — правило, не множество)	условная несовместимость	Rule
бесконечность — схема; точка — производный режим	роли	Role
конечные актуализации (стадии, `nat`, записи)	носители (конечны)	Element
законы $L 1$ – $L 5$ (здесь $L 1$ , $L 5$ )	универсальный слой	Rule (универс.)

{ Хорошая сформированность. Разметка однозначна и здесь оборачивается корневой диагностикой всего тома. Принять бесконечность за объект (завершённое множество, готовую прямую) — это смешение категорий: схему-правило читают как элемент-предмет. $P 4$ и есть принцип, запрещающий это смешение: он держит бесконечность на уровне правил, не элементов. И всякая частная диагностика тома есть его случай: число — роль, не предмет (Часть II); точка — класс-режим, не объект (Глава 4.3); несчётность — правило о процессах, не размер множества (Глава 4.4); рациональное — класс по Qeq, не quotient-объект (Глава III.2). Честная граница: три уровня $P 4$ не сливать — доказан след P4_formalized, тогда как полный онтологический тезис и содержательная деривация из $L 1 \landL 5$ лежат за пределами одной Rocq-теоремы.}

Что даёт разбор. Он кладёт основание всей Части IV: раз бесконечность есть правило-схема, а не объект, то действительное число строится как процесс (Rule), а не как готовая точка (Element); а точка возвращается позднее как производная роль-класс (Глава 4.3). $P 4$ , разобранный по E/R/R, есть та конституция, под которой разворачивается весь процессный анализ, — к его плану глава и переходит.

Куда идёт Часть IV

Построением и изучением этого типа Часть IV и занята. Глава 4.2 даёт RealProcess полное определение — с арифметикой, с метрикой, с условием Коши, выделяющим осмысленные процессы, — и показывает, что тип этот возникает не по произволу, а как структурно неизбежная конструкция. Глава 4.3 разбирает, что такое <<точка>> в процессной онтологии: точка оказывается не объектом, а классом эквивалентности процессов — режимом рассмотрения, в который оператор переходит, когда ему нужно отвлечься от различий между процессами, дающими один и тот же предел; там же — разбор знаменитого равенства нуля целых девяти в периоде единице. Глава 4.4 доказывает несчётность процессов диагональным рассуждением — и доказывает её как следствие различения данных и поведения, а не как загадку о размерах бесконечностей. Глава 4.5 переформулирует вопрос о континууме. Глава 4.6 замыкает часть, сводя баланс того, что $P 4$ отсекает и что оставляет, и помещая ToS в ландшафт оснований.

Настоящая глава была философско-методологическим введением ко всему этому. Она не строила процесс — она оправдывала принцип, ради которого процесс будет построен. Теперь принцип $P 4$ предъявлен в полную силу: сформулирован точно, выведен из оснований, проверен по формализации, отграничен от поспешных прочтений. С этим основанием Часть IV может перейти к делу — и Глава 4.2 начинает его, давая процессу определение типа.

{ $P 4$ — принцип конечной актуальности: всякая система в любой момент конечна, а бесконечность есть свойство процесса, а не объекта. Содержательно он выводится из $L 1$ и $L 5$ , и три мотива тома (операциональная делимость, множество как режим, позитивное существование) суть его грани; что завершённой бесконечности при этом <<нет>> — вывод из принципа, а не сам принцип. У $P 4$ следует различать три уровня: онтологический принцип; его формальный процессный след P4_formalized, доказанный в Rocq (процессы Коши существуют, сумма и произведение сохраняют свойство Коши); и prohibition-теоремы, показывающие несовместимость завершённой бесконечности с $P 4$ -стадийной ограниченностью при специальных определениях. Эти уровни — опора принципа, а не его полный эквивалент. Фундаментальных логических аксиом у ToS две, $L 3$ и $L 4$ ; ни аксиомы бесконечности, ни сет-теоретической аксиомы выбора среди них нет, что зафиксировано документированным мета-аудитом. Отношение $P 4$ к классическим аксиомам формализация разрабатывает в двух слоях: ненужность (работа аксиомы выполнима без неё — показано для бесконечности, конечного выбора, трансфинитной рекурсии, $Π_{1}^{1}$ -выделения) и несовместимость (завершённая бесконечность, как она формализована, противоречит $P 4$ -стадийной ограниченности при мосте — условные, но строгие теоремы). При этом $P 4$ оставляет рабочим основной корпус математики: числа, конечные совокупности, индукцию, конструктивные доказательства, процессы и процессный анализ. ToS есть конструктивизм с классической логикой — сочетание, возможное оттого, что $L 3$ говорит о завершённом акте различения, а $P 4$ — о бесконечной совокупности; эти две установки ToS разводит по разным уровням. Из $P 4$ следует, что действительное число не есть исходно готовая точка — точка восстанавливается позднее как режим рассмотрения процессов; чем действительное число является исходно — процессом — и как этот процесс строится как тип, показывает Глава 4.2.}

Часть: Часть IV. Процессные действительные числа · Том: «Математика»

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

Навигация: ← Глава 4. От позиции к процессу — Часть III · Глава 2. RealProcess как тип →

Формулировка $P 4$ цитируется по работе: А. Хорсократ, <> (PhilArchive, 2026), раздел 2.2.4. Перевод с английского. Там же — полная деривация принципа из законов логики, кратко изложенная ниже в § 1.3. ↩
ProcessFourPrinciples.v Rocq-репозитория ToS (каталог src/process/); файл содержит 25 доказанных утверждений, 0 Admitted, и наследует единственную логическую аксиому classic (о ней § 1.2.4). Имена теорем, приводимые ниже, — из этого файла. ↩
Тип ProcessInstance, список all_instances; лемма twelve_instances доказывает, что список имеет длину двенадцать, лемма all_instances_nodup — что в нём нет повторов. ↩
ToS_Axioms.v Rocq-репозитория ToS (каталог src/); 3 доказанных производных утверждения, 0 Admitted. Файл озаглавлен как объявляющий фундаментальные логические аксиомы теории. ↩
ProcessAxiomAudit.v (каталог src/process/), 13 доказанных утверждений. ↩
А. Хорсократ, <> (PhilArchive, 2026), раздел 2.2.4, заголовок: << $P 4$ : Finite Actuality (derived from L1 $+$ L5)>> и последующая шестишаговая деривация. ↩
P4ProhibitionSynthesis.v (каталог src/foundation/); вступительный комментарий файла противопоставляет ранний слой (<< $P 4$ делает аксиому ненужной>>) позднему (<< $P 4$ несовместим с завершёнными бесконечностями>>) и фиксирует, что второе сильнее первого. ↩
P4_Eliminates_Infinity.v (каталог src/foundation/), 12 доказанных утверждений, 0 Admitted, 0 новых аксиом. ↩
P4_Eliminates_AC.v (каталог src/foundation/), 0 Admitted, 0 новых аксиом. ↩
Теорема P4_eliminates_AC_finite: для всякого семейства family и всякого конечного фронта $N$ , если family $i$ непуст при $i < N$ , то выбор головы списка попадает в family $i$ при всех $i < N$ . Это конечная, stage-wise формулировка выбора; именно она безоговорочно совместима с $P 4$ . ↩
P4_Eliminates_ATR.v (каталог src/foundation/), 15 доказанных утверждений, 0 Admitted, 0 новых аксиом. ↩
P4_Eliminates_Pi11.v (каталог src/foundation/), 15 доказанных утверждений. В этом файле, в отличие от трёх предыдущих, есть объявленный параметр (см. ниже). ↩
P4CompletedInfinity.v (каталог src/foundation/), 12 доказанных утверждений, 0 Admitted, 0 новых аксиом. Это ядро, на которое опираются файлы P4ProhibitsAC.v и P4ProhibitsImpredicative.v. ↩
P4ProhibitsAC.v (каталог src/foundation/), 10 доказанных утверждений, 0 Admitted, 0 новых аксиом; опирается на P4CompletedInfinity.v. ↩
P4ProhibitionSynthesis.v (каталог src/foundation/), 8 доказанных утверждений, 0 Admitted. Файл доказывает P4_prohibits_three (несовместимость с тремя вещами: завершёнными множествами, полной аксиомой выбора, парадоксом Рассела) и P4_preserves_three (совместимость с тремя: потенциальной бесконечностью, конечным выбором, индуктивными типами). ↩

Путь Мудрости

Проводник