Глава 4. Несчётность процессов

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

Что оставила Глава 4.3

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

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

Классический ответ и его цена

Классическая математика отвечает на этот вопрос знаменитой теоремой Кантора: точек на отрезке несчётно много. Их нельзя перенумеровать натуральными числами; никакая последовательность $x_{0}, x_{1}, x_{2}, \dots$ не исчерпает отрезок $[0, 1]$ . Доказательство — диагональный аргумент: по любому предъявленному списку строится точка, в списке отсутствующая.

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

Возникает естественное опасение: не потеряет ли $P 4$ -математика теорему Кантора? Если завершённого несчётного множества нет, то и говорить о его несчётности будто бы не о чем. Настоящая глава показывает, что опасение напрасно: теорема Кантора не теряется — она переформулируется, и переформулированная оказывается утверждением не о множестве, а о процессах.

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

План главы таков. Сначала — что <<несчётность>> не может значить под $P 4$ и какова её правильная, процессная формулировка (§ 4.2). Затем — сама эта формулировка через перечисления процессов: что такое Enumeration и почему перечисление должно быть регулярным (§ 4.3, § 4.4). Затем — устройство диагональной конструкции: почему она делит интервал на три части, а не на две (§ 4.5), и как из этого деления получается диагональный процесс с тремя доказанными свойствами (§ 4.6). Затем — перенос результата в язык процессного ядра (§ 4.7). Наконец — итог, честный учёт того, на каких логических средствах результат стоит, и мост к Главе 4.5 (§ 4.8).

Глава, как и предыдущие, сверяется с Rocq-формализацией построчно. Опираются её рассуждения на два файла. Конструкция диагонального процесса и сама теорема несчётности доказаны в файле ShrinkingIntervals_ERR.v; процессная переформулировка результата — в файле ProcessUncountable.v. Эти два файла глава будет всё время держать раздельно: первый строит и доказывает, второй переводит доказанное на язык процессного ядра. И там, где формализация оговаривает условия — регулярность перечисления, опору на классическую логику, — глава оговорит их вместе с ней, не выдавая результат сильнее, чем он доказан.

Чего не может значить <<несчётность>> под $P 4$ {Чего не может значить «несчётность» под P4}

Классическая формулировка и её предмет

Классическая теорема Кантора утверждает: множество точек отрезка $[0, 1]$ несчётно — не существует биекции между ним и множеством натуральных чисел $N$ . У этого утверждения есть предмет — два готовых множества, $[0, 1]$ и $N$ , и говорится, что между ними нет взаимно однозначного соответствия. Утверждение о множествах: берёт два завершённых объекта и сравнивает их по <<размеру>>.

Под $P 4$ у этого утверждения предмета нет — по крайней мере, не весь. Множество $N$ как завершённая совокупность $P 4$ уже не признаёт; но с $N$ ещё можно работать как с типом, область значений которого порождается процессом (Глава 4.1). А вот <<множество всех точек отрезка>> как готовая завершённая совокупность — это в точности то, чего, как показали Главы 4.1–4.3, в $P 4$ -онтологии нет. Завершённого $[0, 1]$ , собранного из готовых точек-атомов, не существует. Значит, классическое <<множество $[0, 1]$ несчётно>> в исходном виде не имеет того предмета, о котором говорит: нет множества, чью несчётность можно было бы утверждать.

Что нельзя и что можно сохранить

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

Но кое-что — и кое-что существенное — сохранить можно и нужно. Сохраняется содержательное ядро диагонального аргумента: указание на то, что всякая попытка перенумеровать точки проваливается. Это указание можно высказать, не прибегая к завершённым множествам вовсе. Не <<множество $[0, 1]$ больше множества $N$ >>, а: какой угодно процесс перечисления точек — при том уточнении допустимости, которое будет введено ниже, — не охватывает их все. Сколько ни нумеруй, всегда останется точка, не получившая номера. Это утверждение не о завершённых совокупностях, а о процессах перечисления и об их ограниченности — и оно $P 4$ -онтологии не противоречит.

Несчётность как утверждение о процессах

Так $P 4$ переформулирует несчётность. Не <<существует несчётное множество>>, а <<не существует процесса перечисления, который охватил бы все процессные точки отрезка>>. В терминах E/R/R (разбор § 4.8.2) это правило-уровень: невозможность для процесса-нумератора охватить все классы-роли, — а не суждение о завершённом множестве. Утверждение становится отрицательным и процессным: оно говорит о невозможности — о том, что определённого рода процесс (перечисляющий) не может сделать определённой вещи (охватить всё), — и говорит это о процессах, не о множествах. Файл Rocq-формализации, посвящённый этой теореме, прямо так и формулирует своё содержание: под $P 4$ <<несчётность>> означает, что никакое перечисление-процесс не захватывает все процессы Коши — это утверждение о процессах, а не о множестве.¹

Почему интервалы, а не цифры

Прежде чем строить диагональный процесс, стоит сказать об одном выборе средств, который формализация делает с самого начала. Классический диагональный аргумент чаще всего излагают через десятичные цифры: по списку чисел строят новое число, у которого $n$ -я цифра отлична от $n$ -й цифры $n$ -го числа списка. Для процессной математики это плохой носитель доказательства, и Глава 4.3 уже показала, почему. Извлечение цифры — операция разрывная: у числа на границе между двумя десятичными промежутками цифра <<прыгает>>. И оно чувствительно к двойным записям: $0, 999 \dots$ и $1, 000 \dots$ — две цифровые записи одной точки, одного класса (§ 3.7 Главы 4.3), и аргумент, работающий с цифрами, на такой двойственности спотыкается.

Поэтому формализация $T o S$ строит диагональ не через цифры. Носителем служат вложенные интервалы и рациональные оценки: на каждом шаге диагональный процесс не <<выбирает цифру>>, а сужает интервал, в котором лежит будущий предел, отступая от того места, где находится очередной перечисляемый процесс. Интервальная диагональ непрерывна по построению и к двойным записям нечувствительна — она работает с приближениями как с рациональными числами, а не с их позиционными записями. Дальнейшие разделы разворачивают именно эту, интервальную конструкцию.

Перечисление процессов

Что такое перечисление

Чтобы высказать <<никакой процесс перечисления не охватывает все точки>>, нужно сперва точно определить, что такое перечисление. Интуитивно это попытка занумеровать точки: процесс, который на шаге $n$ предъявляет $n$ -ю точку. В ShrinkingIntervals_ERR.v определение выглядит так:

Definition Enumeration := nat -> RealProcess.

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

Процесс, выдающий процессы

В классической картине перечисление — это список готовых чисел: $x_{0}, x_{1}, x_{2}, \dots$ , где каждое $x_{n}$ — точка-атом. В процессной картине так быть не может: готовых точек-атомов нет. Поэтому $n$ -й член перечисления — сам процесс: не точка, а процесс рациональных приближений к точке.

Развернём типы. Голый процесс есть функция из номеров шагов в рациональные приближения: RealProcess $=$ nat -> Q. А перечисление есть функция из номеров в процессы: Enumeration $=$ nat -> RealProcess. Подставив одно в другое:

‘ E n u m er a t i o n ‘ = ‘ na t ‘ \to (‘ na t ‘ \to Q) .

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

E 0 : ‘ R e a l P r ocess ‘, E 1 : ‘ R e a l P r ocess ‘, E 2 : ‘ R e a l P r ocess ‘, \dots

каждый член $E n$ — процесс рациональных приближений к некоторой точке.

Стоит сразу заметить, что перечисление может быть избыточным: два разных номера могут выдавать эквивалентные процессы — то есть двух представителей одной и той же точки (одного класса по process_equiv из Главы 4.3). Это теореме не мешает — напротив, делает её сильнее: она утверждает, что как бы перечисление ни было устроено, даже с повторами, найдётся точка — класс, — не представленная ни одним его членом. Перечисление вольно тратить номера на повторы; теорема говорит, что и без повторов оно всё равно пропустило бы хотя бы один класс.

Допустимое перечисление: регулярность

Не всякая функция nat -> RealProcess годится в перечисление точек отрезка. Нужны два условия. Во-первых, каждый член должен быть настоящим процессом точки — сходящимся, то есть Коши; иначе он не задаёт никакой точки. Во-вторых, все члены должны лежать в отрезке $[0, 1]$ — мы нумеруем точки именно этого отрезка.

ShrinkingIntervals_ERR.v вводит два предиката допустимости. Первый, послабее:

Definition valid_enumeration (E : Enumeration) : Prop :=
  forall n, is_Cauchy (E n) /\ (forall m, 0 <= E n m <= 1).

Каждый член есть процесс Коши и лежит в $[0, 1]$ . Второй предикат сильнее, и именно он понадобится главной теореме:

Definition valid_regular_enumeration (E : Enumeration) : Prop :=
  forall n, is_Regular_Cauchy (E n) /\ (forall m, 0 <= E n m <= 1).

{

Здесь от каждого члена требуется быть не просто Коши, а регулярным Коши — is_Regular_Cauchy. Что это значит и почему этого требуют — предмет следующего раздела. Файл доказывает, что регулярное перечисление есть и обычное (лемма valid_regular_implies_valid): регулярность — усиление, а не отклонение от понятия допустимости. }

Точная формулировка несчётности

Теперь несчётность можно высказать точно. Она утверждает: для всякого регулярного перечисления процессов точек отрезка $[0, 1]$ существует процесс Коши, лежащий в $[0, 1]$ , не эквивалентный ни одному члену перечисления. Сколько бы точек перечисление ни занумеровало, найдётся точка — процесс, — которая его обходит.

Стоит сразу зафиксировать, чего эта формулировка не говорит, чтобы не прочесть её сильнее, чем она есть. Она говорит о регулярных перечислениях, а не о любых перечислениях процессов Коши: член перечисления обязан иметь известный модуль сходимости (§ 4.4). И она говорит о процессах единичного отрезка, а не о <<всех процессах>> вообще: и диагональный процесс, и все члены перечисления лежат в $[0, 1]$ . Это, впрочем, не ослабляет результат до малозначительного — напротив. Несчётность обнаруживается уже внутри одного отрезка: дело не в <<размере всей прямой>>, а в самой процессной структуре сколь угодно малого куска континуума. Одного отрезка довольно, чтобы регулярное перечисление провалилось.

Почему перечисление должно быть регулярным

Сходимость и скорость сходимости

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

Регулярность это положение исправляет. Регулярный процесс Коши — это процесс с известной наперёд скоростью сходимости. В ShrinkingIntervals_ERR.v регулярность задана не абстрактно (<<скорость как-то известна>>), а вполне конкретной оценкой:

Definition is_Regular_Cauchy (R : RealProcess) : Prop :=
  forall m n : nat, (m > 0)%nat -> (n > 0)%nat ->
    Qabs (R m - R n) <= (1 # Pos.of_nat m) + (1 # Pos.of_nat n).

Расхождение приближений на шагах $m$ и $n$ ограничено суммой $\frac{1}{m} + \frac{1}{n}$ . Это не существование скрытого модуля, а явная, выписанная формула: к шагу $m$ процесс заведомо приблизился к своему пределу не хуже чем на $\frac{1}{m}$ с небольшим. Скорость сходимости перестаёт быть скрытой — она прямо записана в определении.

Идея Бишопа

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

Под $P 4$ эта мысль ложится особенно естественно. Если процесс первичен, а точка производна, то процесс должен быть управляем: оператор должен уметь не просто запустить его, но и знать, сколько шагов до нужной точности. Регулярность — это и есть управляемость, выписанная формулой. Регулярный процесс — процесс, которым можно пользоваться, а не только про который известно, что он сходится. Файл доказывает, что регулярность не уводит из класса сходящихся процессов — регулярный Коши есть и обычный Коши (лемма Regular_implies_Cauchy); регулярность лишь добавляет к сходимости знание её скорости.

Зачем регулярность диагональному аргументу

Теперь видно, зачем регулярность нужна именно здесь. Диагональный процесс на каждом шаге $n$ должен <<отступить>> от $n$ -го перечисляемого процесса $E (n)$ — сдвинуться в сторону от того места, где $E (n)$ находится. Но где находится $E (n)$ ? $E (n)$ — процесс; на разных шагах он выдаёт разные рациональные приближения. Чтобы отступить от него осмысленно, диагональная конструкция должна посмотреть на какое-то определённое приближение $E (n)$ и быть уверенной, что это приближение уже близко к пределу — что дальнейшие шаги $E (n)$ не уведут его далеко.

Вот ровно для этой уверенности и нужна регулярность. Будь $E (n)$ просто процессом Коши, конструкция не знала бы, на каком шаге его приближение уже надёжно: рубеж существует, но не предъявлен. У регулярного же процесса скорость известна формулой — и конструкция может вычислить номер шага (в коде он называется trisect_ref $n$ ), на котором приближение $E (n)$ гарантированно попало в узкую окрестность предела. Зная это, она может безопасно отступить: отойти не от случайного приближения, а от места, где $E (n)$ заведомо останется. Регулярность — то, что превращает <<отступить от $E (n)$ >> из неопределённого намерения в выполнимую операцию.

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

Трисекция, а не бисекция

Замысел диагонали через интервалы

Диагональный процесс строится так. Берём отрезок $[0, 1]$ . На шаге $n$ смотрим, где находится $n$ -й перечисляемый процесс $E (n)$ , и сужаем текущий интервал до его части, отступающей от $E (n)$ . Интервалы вкладываются друг в друга и стягиваются; их середины образуют процесс — диагональный. Поскольку на шаге $n$ интервал отошёл от $E (n)$ , предел диагонали окажется отделён от $E (n)$ — диагональ не совпадёт ни с одним перечисляемым процессом.

Весь вопрос — как именно <<сузить, отступив>>. И здесь у конструкции есть развилка, от которой зависит, пройдёт доказательство или нет.

Краевая трудность бисекции

Простейший способ — бисекция: делить интервал пополам. Посмотреть, в какой половине — левой или правой — находится $E (n)$ , и взять другую. ShrinkingIntervals_ERR.v этот подход реализует (конструкция avoid_E, diagonal_intervals), но сам же помечает его как вытесненный лучшим — из-за краевой трудности.

Трудность вот в чём. Конструкция не знает положение $E (n)$ точно — она знает его приближённо, через одно из рациональных приближений процесса $E (n)$ . Вокруг этого приближения есть неустранимая неопределённость — назовём её доверительным интервалом: полоска $[приближение - δ, приближение + δ]$ , внутри которой предел $E (n)$ заведомо лежит, но где именно — неизвестно. И вот беда: эта полоска может оседлать середину делимого интервала. Тогда непонятно, в какой половине $E (n)$ : часть доверительного интервала слева от середины, часть справа. Какую половину ни выбери <<противоположной>>, предел $E (n)$ может оказаться в ней же — у самой границы. Бисекция на этом краевом случае спотыкается: <<враг ровно на середине>>, и отступить некуда.

Решение: деление на три

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

Inductive TrisectChoice : Set := TC_Left | TC_Middle | TC_Right.

Идея проста. Доверительный интервал вокруг приближения $E (n)$ имеет некоторую ширину — скажем, $2 δ$ . Если эта ширина короче одной трети, то доверительный интервал, как бы он ни лежал, не может пересечь все три трети сразу. Значит, хотя бы одна треть свободна — доверительный интервал её не касается, и $E (n)$ в неё попасть не может. В эту свободную треть конструкция и сужает интервал. <<Враг ровно на середине>> больше не страшен: даже оседлав границу двух третей, доверительный интервал, будучи короче трети, оставляет третью треть нетронутой. Выбор свободной трети выполняет функция smart_trisect_choice; она устроена не как <<выбор>> в каком-либо проблемном смысле, а как детерминированное ветвление по рациональным неравенствам — о чём подробнее в § 4.8.

Синхронизация параметров

Чтобы рассуждение прошло, нужно гарантировать ключевое неравенство: ширина доверительного интервала меньше ширины трети, и не для какого-то одного шага, а для всех шагов сразу. Здесь и нужна регулярность из § 4.4: она позволяет связать три величины так, чтобы неравенство держалось всегда. В актуальном коде параметры синхронизированы так:

‘ r e f ‘ (n) = 48 \cdot 3^{n}, δ (n) = \frac{1}{24 \cdot 3 ^{n}}, ширина (n) = \frac{1}{3 ^{n}} .

Здесь $‘ r e f ‘ (n)$ — номер шага, на котором берётся приближение $E (n)$ (регулярность гарантирует, что к этому шагу $E (n)$ уже близок к пределу); $δ (n)$ — полуширина доверительного интервала; ширина — размер интервала после $n$ трисекций, убывающий как $1/ 3^{n}$ . При такой синхронизации выполнено

2 δ (n) < \frac{ширина ( n )}{3} для всех n,

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

{ Ширина вложенных интервалов убывает геометрически, как $1/ 3^{n}$ — тройное сжатие на каждом шаге; отсюда и следует свойство Коши диагонального процесса (§ 4.6.2). Эту скорость в процессной переформулировке отмечают отдельной величиной — diagonal_convergence_rate, равной $1/3$ . }

Диагональный процесс

Построение

Собрав трисекцию воедино, получаем диагональный процесс. Начинаем с отрезка $[0, 1]$ . На каждом шаге $n$ берём приближение $E (n)$ на шаге $‘ r e f ‘ (n)$ , строим вокруг него доверительный интервал полуширины $δ (n)$ , находим свободную треть и сужаем текущий интервал до неё. Так получается последовательность вложенных, стягивающихся интервалов. Диагональный процесс — это процесс их середин: на шаге $n$ он выдаёт середину $n$ -го интервала. В Rocq-формализации он называется diagonal_trisect_v2.

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

Диагональ есть процесс Коши

{ Первое: диагональный процесс сходится — есть процесс Коши. Это лемма diagonal_trisect_v2_is_Cauchy. Доказательство опирается на стягивание интервалов: ширина $n$ -го интервала есть $1/ 3^{n}$ , а степени тройки растут неограниченно (архимедова лемма Archimedean_pow3 из того же файла). Значит, для всякой точности $ε$ найдётся шаг, после которого интервалы уже уже $ε$ ; а середины, начиная с этого шага, все лежат в одном узком интервале и потому расходятся меньше $ε$ . Диагональ — настоящий процесс точки, а не расходящийся набор рациональных чисел. }

Диагональ лежит в отрезке

{ Второе: диагональный процесс не выходит из $[0, 1]$ . Это лемма diagonal_trisect_v2_in_unit: на всяком шаге значение диагонали заключено между $0$ и $1$ . Доказательство простое по сути: начальный интервал есть $[0, 1]$ , а каждая треть лежит внутри делимого интервала — трисекция не выводит за пределы. Середина любого из вложенных интервалов остаётся, стало быть, в $[0, 1]$ . Это свойство нужно, чтобы диагональ была законным соперником перечисляемым процессам: те по условию допустимости лежат в $[0, 1]$ , и диагональ — тоже, иначе сравнивать было бы не вполне честно. }

Диагональ отлична от каждого перечисляемого процесса

Третье свойство — сердцевина доказательства: диагональный процесс не эквивалентен ни одному перечисляемому. Это лемма diagonal_trisect_v2_differs_from_E_n. Здесь нужно вспомнить, что значит <<не эквивалентен>>. В ShrinkingIntervals_ERR.v это предикат not_equiv:

Definition not_equiv (R1 R2 : RealProcess) : Prop :=
  exists eps, eps > 0 /\ forall N, exists m,
    (m > N)%nat /\ Qabs (R1 m - R2 m) >= eps.

Это не просто отрицание сходимости разности к нулю — это положительное утверждение об устойчивом зазоре: существует $ε > 0$ , такой что после любого рубежа $N$ найдётся шаг $m > N$ , на котором расхождение процессов не меньше $ε$ . Зазор не обязан стоять на каждом позднем шаге — определение этого и не требует; оно требует, чтобы расхождение снова и снова достигало $ε$ , сколь угодно далеко по ходу процесса. Два процесса, связанные not_equiv, разведены не <<в пределе>>, а по существу: расхождение между ними не угасает — оно неограниченно повторяется.

Почему диагональ так разведена с каждым $E (n)$ . На шаге $n + 1$ конструкция сузила интервал в треть, свободную от доверительного интервала $E (n)$ . Диагональ, начиная с этого шага, лежит внутри выбранной трети; а $E (n)$ — по построению свободной трети — от этой трети отделён, по другую сторону зазора. Зазор имеет вычислимую положительную ширину (она получается из той же синхронизации $2 δ < ширина /3$ ). Этот зазор и служит порогом $ε$ в not_equiv: расхождение диагонали и $E (n)$ снова и снова достигает его, сколь угодно далеко по шагам. Диагональ отлична от $E (n)$ не случайно и не <<в пределе>> — она отделена от него устойчивой щелью, и это доказано для каждого $n$ .

Главная теорема

Три свойства вместе и составляют теорему несчётности. В ShrinkingIntervals_ERR.v она записана так:

Theorem unit_interval_uncountable_trisect_v2 :
  forall E : Enumeration,
  valid_regular_enumeration E ->
  exists D : RealProcess,
    is_Cauchy D /\
    (forall m, 0 <= D m <= 1) /\
    (forall n, not_equiv D (E n)).

Прочтём дословно. Для всякого перечисления $E$ , если оно регулярно допустимо, существует процесс $D$ , такой что: $D$ есть Коши; $D$ лежит в $[0, 1]$ ; и для всякого $n$ процесс $D$ не эквивалентен $E (n)$ . Процесс $D$ — это и есть диагональ diagonal_trisect_v2, а три конъюнкта — три разобранных свойства.

Стоит отметить одну точность сигнатуры. О диагонали $D$ теорема утверждает, что она есть процесс Коши (is_Cauchy), — но не утверждает, что она регулярна. Регулярность требуется от перечисляемых процессов — чтобы конструкция могла знать, где они находятся (§ 4.4); сама же построенная диагональ заявлена лишь как сходящийся процесс в $[0, 1]$ . Регулярность диагонали в сигнатуру главной теоремы не входит, и глава её не утверждает: формализация доказала ровно то, что записано — is_Cauchy, нахождение в отрезке и неэквивалентность всем членам.

Процессная переформулировка

Зачем нужен перевод

Теорема предыдущего раздела доказана в ShrinkingIntervals_ERR.v — файле, который сложился вокруг вложенных интервалов и имеет свой рабочий язык. Между тем основное процессное ядро ToS — файл ProcessCore.v, разобранный в Главах 4.2 и 4.3, — говорит на немного другом языке. Чтобы теорема несчётности встала в общий ряд процессной математики, её нужно перевести в термины ProcessCore. Этим занят отдельный файл — ProcessUncountable.v.

{ Важно сразу развести роли двух файлов, не смешивая их. ShrinkingIntervals_ERR.v — это файл, где диагональ построена и теорема доказана; вся тяжёлая работа — трисекция, синхронизация, зазор — там. ProcessUncountable.v — это файл-переводчик: он не строит диагональ заново и не доказывает несчётность с нуля, он переносит уже доказанное на язык процессного ядра. Его собственная теорема прямо опирается на unit_interval_uncountable_trisect_v2. }

Мост между двумя записями свойства Коши

Перевод требует одного технического моста. Свойство Коши в двух файлах записано чуть по-разному. В ShrinkingIntervals_ERR.v рубеж берётся строгим неравенством — приближения сближаются для шагов строго больше $N$ . В ProcessCore.v — нестрогим, для шагов не меньше $N$ . Разница невелика и чисто кванторная — одно и то же условие сходимости в двух оформлениях, — но формально это два разных предиката, и их надо связать. ProcessUncountable.v связывает их леммой si_cauchy_compat: две записи свойства Коши равносильны. Это — мост, как мост между is_Cauchy и is_cauchy в Главе 4.2: не тождество термов, а доказанная равносильность двух формулировок одного содержания.

Аналогичный мост нужен и для <<различия>> процессов. В ShrinkingIntervals_ERR.v различие выражено предикатом not_equiv (устойчивый зазор $ε$ ); в ProcessCore.v есть отношение эквивалентности process_equiv (Глава 4.3). ProcessUncountable.v доказывает лемму not_equiv_implies_not_process_equiv: если процессы связаны not_equiv, то они не эквивалентны по process_equiv.

Несчётность в языке процессного ядра

С этими мостами теорема переносится. В ProcessUncountable.v её процессная версия выглядит так:

Theorem process_uncountable :
  forall E : Enumeration,
  valid_regular_enumeration E ->
  exists D : RealProcess,
    is_Cauchy D /\
    (forall m, 0 <= D m /\ D m <= 1) /\
    (forall n, ~ process_equiv D (E n)).
Proof.
  intros E Hvalid.
  destruct (unit_interval_uncountable_trisect_v2 E Hvalid)
    as [D [HD1 [HD2 HD3]]].
  ...

{

Та же несчётность — но в типах ProcessCore. И структура доказательства видна сразу: оно разбирает результат главной теоремы (destruct … unit_interval_uncountable_trisect_v2) и переоформляет три его конъюнкта через мосты. Файл-переводчик честен относительно своего источника: он не претендует на самостоятельное доказательство, он переводит. }

Одна точность: $\neg$ {не} process_equiv и not_equiv

{ Здесь надо отметить тонкость, чтобы не прочесть переведённую теорему сильнее исходной. Исходная теорема в ShrinkingIntervals_ERR.v даёт not_equiv — положительное утверждение об устойчивом зазоре: предъявлен порог $ε$ , которого расхождение снова и снова достигает, сколь угодно далеко по шагам. Переведённая теорема в ProcessUncountable.v даёт $\neg‘ p r oces s_{e} q u i v ‘$ — отрицание эквивалентности. }

Мост ведёт в одну сторону: not_equiv влечёт $\neg‘ p r oces s_{e} q u i v ‘$ , и эта импликация доказана. Обратной импликации — что из отрицания эквивалентности можно извлечь устойчивый зазор — в репозитории отдельной леммой не выделено. Поэтому точнее всего сказать так: на уровне текущей формализации not_equiv есть более информативное утверждение — оно несёт явный свидетель-зазор; а ProcessUncountable.v пользуется лишь следствием этого факта, отрицанием process_equiv. Это — различие уровня информативности двух формулировок в нынешнем коде, а не заявление о том, что одно утверждение математически строго слабее другого безусловно.

Связь с Главой 4.3: диагональ как новый класс

Перевод на язык process_equiv даёт прямую смычку с Главой 4.3. Там точка была понята как setoid-класс процессов: для представителей CauchySeq — по отношению cauchy_equiv, а для голых RealProcess — по согласованному с ним отношению process_equiv (мост между двумя отношениями доказан в ProcessBridge.v, § 3.3.1). Это два разных отношения на двух репрезентациях, но связанные мостом — одно и то же <<задавать одно число>>. Процессы в одном классе — одна точка. Переведённая теорема говорит, что диагональ не находится в отношении process_equiv ни с одним перечисляемым процессом. На языке Главы 4.3 это значит: диагональ представляет новый класс — точку, которой в перечислении нет. Перечисление занумеровало какие-то классы; диагональ предъявляет класс, в нумерацию не попавший.

Здесь стоит, как и в Главе 4.3, держать осторожность с словом <<класс>>. Фактортип точек — тип, термами которого были бы сами классы, — в репозитории не построен (Глава 4.3, § 3.4.3); глава 4.4 этого тоже не утверждает. Но отношение, отделяющее классы друг от друга, — process_equiv, — построено и доказано, и именно оно работает в формальной теореме: диагональ отделена от каждого $E (n)$ по этому отношению. Несчётность относится к классам — но выражается через отношение, не через готовый фактортип: теорема говорит не о голых процессах как отдельных записях, а о классах эквивалентности, и формально выражает это отношением process_equiv.

И отделена диагональ от $E (n)$ именно по отношению эквивалентности, а не поточечно. Глава 4.3 в § 3.8 это предсказала: различие, нужное для диагонального аргумента, — не поточечное несовпадение (его, как мы видели, и недостаточно, и не требуется), а несовпадение по process_equiv, непопадание в общий класс. Диагональ может на отдельных шагах быть сколь угодно близка к $E (n)$ — важно, что в один класс с ним она не попадает: расхождение между диагональным процессом и $E (n)$ не может стать нулевым в смысле процессной эквивалентности. Эту перекличку с ролями-классами Главы 4.3 разбор § 4.8.2 сводит воедино: счёт ведётся по классам, а диагональ предъявляет новый класс-роль.

Что доказано и на чём оно стоит

Что доказано

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

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

Разбор E/R/R: несчётность как утверждение о процессах

{ Доказанное имеет E/R/R-устройство (Часть I), и его разбор закрепляет главный сдвиг главы. Заголовок опорного файла задаёт разметку прямо: элементы — вложенные интервалы, избегающие каждого перечисляемого процесса; роль — диагональ отлична от каждого перечисляемого; правило — на шаге $n$ избегать $E (n)$ , выбирая свободную треть.³ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе: речь о процессах над $Q$ , фактортип классов не построен (Глава 4.3), <<система>> — не объект System $L$ .}

Rules — правила (закон $L 5$ ). Конституция-конструкция — правило трисекции: на шаге $n$ сузить интервал в треть, свободную от $E (n)$ (а не делить пополам — бисекция спотыкалась о краевой случай, § 4.5). Различие процессов фиксирует правило not_equiv — устойчивый зазор, которого расхождение снова и снова достигает (счёт идёт по классам, не поточечно). Условие допустимости — регулярность перечисления (valid_regular), управляемый доступ к каждому процессу (§ 4.4). И самая общая конституция — $P 4$ : несчётность есть утверждение о процессах и перечислении, а не о завершённом множестве. Честная граница средств: доказательство опирается на $L 3$ (classic), но не на аксиому выбора и не на завершённую бесконечность (§ 4.8.4 ниже).

Roles — значимость позиций (закон $L 4$ ). Перечисление $E$ играет роль нумератора — процесса, выдающего процессы (§ 4.3); диагональ $D$ — роль соперника, процесса, отличного от каждого перечисляемого (так роль и названа в заголовке файла); регулярность — роль управляемости, без которой <<отступить от $E (n)$ >> неосуществимо (§ 4.4). И счёт ведётся по классам, как подготовила Глава 4.3: диагональ предъявляет новый класс-роль, в перечисление не попавший.

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — процессы: перечисляемые $E (n)$ и диагональный $D$ , а под ними — вложенные интервалы и их середины. По $L 1$ каждый процесс тождествен себе. По $P 4$ всё конечно на каждом шаге: диагональ строится шаг за шагом, перечисление есть функция, выдающая функции, — завершённого несчётного множества точек нигде не образуется.

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

Компонент	Что фиксирует	E/R/R
процессы $E (n)$ , диагональ $D$ ; вложенные интервалы	носители (конечны, $P 4$ )	Element
$E$ — нумератор; $D$ — соперник; регулярность — управляемость	роли	Role
трисекция: избегать $E (n)$ свободной третью	конституция-конструкция	Rule
`not_equiv`; счёт по классам	правило различия	Rule (конкр.)
$P 4$ : несчётность — о процессах, не о множестве	конституция	Rule
законы $L 1$ – $L 5$ (здесь $L 3$ )	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: процессы — элементы, нумератор и соперник — роли, трисекция и not_equiv — правила. И здесь разбор снова оборачивается диагностикой: классический <<парадокс>> сверхбольшого несчётного множества возникал от смешения категорий — от чтения <<всех точек отрезка>> как готового элемента-совокупности. В верной разметке несчётность — не свойство завершённого множества, а правило о процессах: ни один процесс-нумератор не охватывает все классы-роли. Завершённой бесконечности нет ни на входе, ни на выходе.

Разбор замыкает процессную линию Части IV. Глава 4.2 прочла число как прогрессию ролей (кандидат $\to$ представитель $\to$ класс), Глава 4.3 — точку как роль-класс; настоящая глава отвечает, сколько таких ролей-классов в отрезке — и отвечает на языке процессов: больше, чем может занумеровать любой регулярный процесс-нумератор. Несчётность из утверждения о <<размере множества>> стала утверждением о пределе перечисляющего процесса. Сколько именно и как устроен этот <<избыток>> структурно — вопрос Главы 4.5.

На чём это стоит: классическая логика

{ Честность требует назвать логические средства, на которых результат держится. Оба опорных файла — и ShrinkingIntervals_ERR.v, и ProcessUncountable.v — используют классическую логику: аксиому classic, закон исключённого третьего. В ShrinkingIntervals_ERR.v это видно прямо: файл импортирует классический модуль и снабжён философской заметкой о роли этого закона; ProcessUncountable.v наследует ту же аксиому. Результат о несчётности процессов — не полностью конструктивный: он опирается на $L 3$ . }

Это не противоречие и не изъян. Глава 4.1 показала, что $L 3$ — закон исключённого третьего — в ToS есть один из принятых законов различения, а не сомнительное допущение: различение есть или его нет, третьего акт различения не оставляет. Опора несчётности на $L 3$ означает лишь, что результат стоит на том же логическом основании, что и весь том. Назвать эту опору — значит быть точным, а не признать слабость.

Чего здесь нет: выбора и завершённой бесконечности

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

И доказательство не использует завершённую бесконечность как готовый объект. Завершённого бесконечного множества точек оно нигде не образует: процессы — это функции, перечисление — функция, выдающая функции, диагональ строится шаг за шагом, и на каждом шаге всё конечно. Файл ShrinkingIntervals_ERR.v это машинно проверяет: для ключевых теорем он содержит команды Print Assumptions, выводящие список аксиом, от которых теорема зависит. В этих зависимостях появляется классическая логика и не появляется ни отдельная аксиома выбора, ни аксиома бесконечности теоретико-множественного, ZFC-подобного образца. (Оговорим точно: Print Assumptions проверяет зависимости указанной теоремы, а не <<сканирует файл целиком>>; и говорить здесь надо именно о зависимостях главных теорем несчётности.)

Здесь важно ещё одно различение, чтобы у внимательного читателя не осталось недоумения. В доказательстве активно участвует тип nat — номера шагов; через него строятся nat -> Q и nat -> RealProcess. Не есть ли уже сам nat <<завершённая бесконечность>>? Нет — и Глава 4.1 это разобрала. nat в ToS читается не как готовое множество всех натуральных чисел, а как индуктивная схема порождения: правило <<есть нуль; от всякого числа есть следующее>>. Тип nat предъявляет правило, а не завершённый набор. Аксиома же бесконечности теоретико-множественного образца постулирует готовое бесконечное множество как актуальный объект — и вот её доказательство не использует. nat как тип шагов процесса с $P 4$ совместим; завершённая бесконечность как объект — нет. Несчётность процессов получена средствами первого рода: классическая логика — да, завершённая актуальная бесконечность — нет.

Мост к Главе 4.5

Теорема несчётности ставит новый вопрос — и им займётся следующая глава. Рациональные точки счётны: их можно занумеровать, для них процесс перечисления существует. Процессные классы отрезка — как мы показали — от регулярного перечисления ускользают. Значит, между рациональными точками и процессными есть какая-то разница — но какая? Классическая математика ответила бы: разница в мощности, рациональных <<счётно много>>, а точек отрезка <<несчётно много>>, и второе <<больше>> первого.

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

{Итог главы — в трёх частях. Первое: что доказано. Никакое регулярное перечисление процессов Коши в отрезке $[0, 1]$ не покрывает все процессные классы этого отрезка: для всякого такого перечисления строится диагональный процесс Коши, лежащий в $[0, 1]$ и отделённый устойчивым зазором (not_equiv) от каждого члена. Это теорема Кантора в $P 4$ -прочтении — утверждение не о завершённом несчётном множестве, а о невозможности процессного перечисления; конструкция диагонали — трисекционная.}

{Второе: на чём это стоит. Конструкция и теорема доказаны в ShrinkingIntervals_ERR.v; процессная переформулировка — в ProcessUncountable.v, который переносит результат на язык ProcessCore через мост si_cauchy_compat и импликацию not_equiv_implies_not_process_equiv. Теорема требует регулярного перечисления — с известным модулем сходимости; для произвольных перечислений Коши она не устанавливается. Оба файла используют классическую логику ( $L 3$ , аксиому classic); аксиома выбора и аксиома бесконечности не используются — трисекция детерминирована, завершённых бесконечностей нет.}

{Третье: что остаётся открытым. Процессная теорема даёт $\neg‘ p r oces s_{e} q u i v ‘$ — отрицание эквивалентности; исходная not_equiv с явным зазором более информативна, и обратный переход отдельной леммой в коде не выделен. Диагональ представляет новый класс эквивалентности; фактортип этих классов отдельным Rocq-типом не построен (Глава 4.3) — работает отношение, отделяющее классы, а не готовый фактортип. И открытым остаётся вопрос о <<величине>> процессного континуума: чем именно процессные классы отрезка отличаются от счётных рациональных точек, если говорить о различии не на языке завершённых мощностей, — к этому вопросу ведёт Глава 4.5.}

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

Понятия: Формализация

Навигация: ← Глава 3. Точка как класс эквивалентности процессов · Глава 5. Процессный континуум →

ProcessUncountable.v Rocq-репозитория ToS (каталог src/process/); заголовочный комментарий файла. Точная формальная версия, как будет видно в § 4.3–4.4, требует регулярного перечисления (valid_regular_enumeration): не любого перечисления процессов Коши, а перечисления с управляемым, регулярным доступом к каждому процессу. ↩
Оговорка о сверке: часть пояснительных комментариев в ShrinkingIntervals_ERR.v использует более раннее численное обозначение параметров (с множителем $12$ вместо $48$ и $24$ ). В настоящей главе приведены фактические определения из кода — trisect_ref и trisect_delta, — а не устаревшие комментарии; на справедливость леммы $2 δ < ширина /3$ это расхождение не влияет, так как лемма доказана для определений, а не для комментариев. ↩
E/R/R-разметка в шапке файла ProcessUncountable.v; здесь разворачивается по образцу Части I. ↩

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

Проводник