Глава 5. Процессный континуум

От количества к структуре

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

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

И в самом конце Глава 4.4 оставила вопрос — открытым, нарочно не предрешая ответа. Рациональные точки счётны: для них процесс перечисления существует. Процессные классы отрезка — ускользают от всякого регулярного перечисления. Между первыми и вторыми есть какая-то разница. Но какая? Чем именно процессные классы отличаются от счётных рациональных — если говорить не на языке завершённых мощностей?

Соблазн мощности и почему он не подходит

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

Под $P 4$ этот ход рассуждения недоступен с самого первого шага. <<Мощность>> — это характеристика завершённого множества: сколько в нём элементов, взятых разом, как готовая совокупность. А завершённых множеств точек $P 4$ не признаёт (Главы 4.1–4.3). Спрашивать <<какова мощность континуума>> или <<есть ли промежуточная мощность>> — значит уже принять то, что отвергнуто: что континуум есть готовое множество с определённым числом элементов. Вопрос о промежуточной мощности под $P 4$ не получает ложного ответа — он вовсе теряет предмет. В разборе E/R/R (§ 5.7.5) континуум окажется не мощностью, а структурным типом — ролью, не объектом.

Переход к вопросу о структуре

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

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

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

Чтобы высказать и обосновать эту дихотомию, главе понадобится сменить рабочую модель. Главы 4.2–4.4 работали с процессами Коши над $Q$ — моделью, близкой к привычной числовой прямой. Настоящая глава переходит к бинарным процессам — пространству Кантора $2^{N}$ . Зачем нужна смена модели и чем она оправдана — предмет § 5.2. Затем — диагональный аргумент в новой модели, оказывающийся проще прежнего (§ 5.3); аппарат деревьев и замкнутых совокупностей (§ 5.4); совершенные поддеревья (§ 5.5); и, как кульминация, — сама дихотомия Кантора–Бендиксона (§ 5.6) и её прочтение в роли процессной версии вопроса о континууме (§ 5.7). Заключительный раздел подводит итог не только главе, но и всей Части IV (§ 5.8).

Глава, как и предыдущие, сверяется с Rocq-формализацией построчно. Опорных файлов на этот раз три, и они образуют восходящую линию. ProcessTypes.v вводит типы бинарных процессов, деревьев и совокупностей. ProcessDiagonal.v строит на них диагональный аргумент. ProcessContinuumHypothesis.v доказывает центральную теорему — структурную дихотомию. И там, где формализация оговаривает условия — замкнутость совокупности, опору на законы логики, — глава оговорит их вместе с ней.

Другая модель: бинарные процессы

Зачем менять модель

Главы 4.2–4.4 строили действительное число как процесс Коши над $Q$ : функцию из номеров шагов в рациональные приближения, RealProcess $=$ nat -> Q. Эта модель близка к привычной числовой прямой и хороша, когда нужно говорить о величинах — о том, к какому числу процесс сходится, как быстро, в каком отрезке лежит.

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

Поэтому глава переходит к другой модели — более простой и прямо приспособленной к разговору о структуре. К бинарным процессам.

Бинарный процесс

Бинарный процесс — это процесс, который на каждом шаге выдаёт не рациональное приближение, а одно из двух значений: <<да>> или <<нет>>, $1$ или $0$ , true или false. В ProcessTypes.v определение предельно короткое:

Definition BinProcess := nat -> bool.

Функция из номеров шагов в булевы значения. На шаге $0$ процесс говорит <<да>> или <<нет>>, на шаге $1$ — снова одно из двух, и так далее. Бинарный процесс — это бесконечная последовательность двоичных выборов.

Совокупность всех бинарных процессов — всех функций nat -> bool — называется пространством Кантора и обозначается $2^{N}$ . Это классический объект, и на нём настоящая глава и будет работать.

Как и ранее с RealProcess (Глава 4.2), здесь нужна $P 4$ -оговорка. nat -> bool — это формальный тип языка Rocq, а не онтологически первичная завершённая совокупность всех бинарных последовательностей. ToS читает его не как готовое множество, взятое разом, а как тип процессных правил: бинарный процесс есть правило, которое на каждый конечный запрос — номер шага $n$ — отвечает значением true или false. <<Все бинарные процессы>> — оборот речи о типе правил, а не о завершённой бесконечной совокупности; и когда ниже глава спросит, перечислимы ли те или иные совокупности таких процессов, спрашивать она будет именно о правилах и об их обходе, не о готовых множествах.

Бинарная модель — не отрезок

Здесь нужно сразу поставить важную оговорку, чтобы не возникло ложного отождествления. Пространство Кантора $2^{N}$ — это не отрезок $[0, 1]$ и не та модель, с которой работали Главы 4.2–4.4. Связь между ними, конечно, есть: бесконечную последовательность нулей и единиц можно прочесть как двоичную запись числа из $[0, 1]$ , и классически пространство Кантора тесно сплетено с континуумом. Эта связь теперь и формализована — в одну сторону: файл ProcessBinReal.v строит перевод bin_to_real, который всякому бинарному процессу сопоставляет точку отрезка (частичные суммы $\sum_{k} bit_{k} / 2^{k + 1}$ , лежащие в $[0, 1]$ ). Но тождества нет, и это видно прямо на переводе: двоичная запись неоднозначна — $0, 0111 \dots$ и $0, 1000 \dots$ задают одну точку, — и образцом служит доказанная лемма bin_ones_equiv_one ( $0, 111 \dots_{2} = 1$ как равенство точек). Из-за этой неоднозначности $2^{N}$ и $[0, 1]$ устроены по-разному; перевод не взаимно однозначен, и пространство Кантора, строго говоря, не есть отрезок.

Для настоящей главы это не помеха, а удобство. Глава занята структурой, и $2^{N}$ — более чистая структурная модель, чем $[0, 1]$ : в ней нет рациональных приближений, нет краевых сложностей с двойными записями внутри аргумента (каждый шаг просто true или false), и ветвление видно прямо. Бинарная модель — это отдельная ветвь процессной формализации континуума: не замена модели Коши, а её структурный двойник, на котором теорему о строении доказать чище. Глава 4.4 работала в модели Коши на отрезке; Глава 4.5 работает в модели Кантора — и это сознательный, оговорённый переход.

Равенство бинарных процессов

Когда два бинарных процесса считать одним? Здесь нужно ещё одно разведение — с понятием эквивалентности из предыдущих глав.

В ProcessTypes.v равенство бинарных процессов — это bp_eq:

Definition bp_eq (p q : BinProcess) : Prop := forall n, p n = q n.

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

И вот тут важно не спутать. В Главах 4.3–4.4 процессы сравнивались не поточечно. Там отношение process_equiv связывало процессы Коши с общим пределом: два процесса могли на каждом шаге расходиться, выдавать разные приближения — и всё же быть эквивалентными, если сходились к одному числу. Точка там была классом по такому отношению <<одинакового предела>>.

В бинарной модели всё иначе. bp_eq — именно поточечное совпадение, а не <<одинаковый предел>>. И рассматриваются здесь сами бинарные процессы как последовательности — а не классы по пределу. Это сознательный выбор модели: предыдущие главы строили точку как класс, эта глава работает с процессами-последовательностями напрямую. Совокупность бинарных процессов — BinCollection — есть просто набор таких последовательностей:

Definition BinCollection := BinProcess -> Prop.

А перечислимость совокупности — наличие процесса, который её обходит:

Definition is_enumerable (C : BinCollection) : Prop :=
  exists f : nat -> BinProcess,
    forall p, C p -> exists n, bp_eq (f n) p.

Совокупность $C$ перечислима, если есть функция $f$ из номеров в бинарные процессы, накрывающая всякий член $C$ : для любого $p \in C$ найдётся номер $n$ с bp_eq $(f n) p$ . Перечислимость — это и есть <<совокупность можно обойти счётным списком>>. Вокруг этого понятия — перечислимо или нет — и построится вся глава.

Несчётность снова — но проще

Диагональ для бинарных процессов

Первое, что стоит сделать в новой модели, — убедиться, что теорема Кантора в ней по-прежнему верна: бинарных процессов тоже несчётно много, никакое перечисление их не охватывает. Это нужно и само по себе, и как разгон к главному результату главы. И здесь обнаруживается приятное: в бинарной модели диагональный аргумент оказывается намного проще, чем трисекционная конструкция Главы 4.4.

Основа — две короткие операции из ProcessDiagonal.v. Первая — переворот, булево отрицание:

Definition flip (b : bool) : bool :=
  match b with true => false | false => true end.

flip меняет true на false и обратно. Вторая — сам диагональный процесс:

Definition diagonal (f : nat -> BinProcess) : BinProcess :=
  fun n => flip (f n n).

По перечислению $f$ строится бинарный процесс, который на шаге $n$ выдаёт перевёрнутое $n$ -е значение $n$ -го процесса перечисления. Это классическая диагональ Кантора в чистом виде: идём по диагонали таблицы <<номер процесса $\times$ номер шага>> и всюду переворачиваем.

Почему здесь нет краевых трудностей

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

В бинарной модели ничего этого не нужно, и причина проста. Значение бинарного процесса на шаге $n$ — это не рациональное приближение с неопределённостью вокруг, а просто true или false: один из двух точных вариантов. <<Отступить>> от него — это просто flip: взять другой вариант. Никакой приближённости, никакого доверительного интервала, никакой границы, которую можно оседлать. Нет и аналога проблемы $0, 999 \dots = 1$ — той двойственности записи, что мешала цифровому аргументу в Главе 4.3: координата бинарного процесса однозначна. flip гарантирует несовпадение в одной координате — и этого довольно.

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

Ключевое свойство диагонали — лемма diagonal_differs:

Lemma diagonal_differs : forall f n,
  ~ bp_eq (diagonal f) (f n).

Диагональный процесс не равен (по bp_eq) ни одному члену перечисления. Доказательство умещается в одну мысль: если бы diagonal $f$ совпадал с $f n$ на каждом шаге, то совпадал бы и на шаге $n$ ; но на шаге $n$ диагональ по построению выдаёт flip $(f nn)$ — перевёрнутое значение, — а перевёрнутое значение не равно исходному (flip_neq). Противоречие.

И вот что здесь существенно. Эта лемма доказана без всяких аксиом. Файл проверяет это машинно командой Print Assumptions, и для diagonal_differs она показывает: ни одной аксиомы, доказательство замкнуто. Это резкий и поучительный контраст с Главой 4.4: там трисекционная диагональ опиралась на классическую логику ( $L 3$ ). Здесь — чистая конструкция: flip вычисляется, несовпадение проверяется, никакого закона исключённого третьего не требуется. Бинарная диагональ конструктивна в полном смысле.

Теорема Кантора в бинарной модели

Из diagonal_differs немедленно следует несчётность. ProcessDiagonal.v формулирует её так:

Theorem cantor_for_processes :
  forall f : nat -> BinProcess,
  exists g, forall n, ~ bp_eq g (f n).

Для всякого перечисления $f$ существует бинарный процесс $g$ , не равный ни одному $f n$ , — и этот $g$ есть просто diagonal $f$ . Тот же результат файл подаёт и как прямое отрицание перечислимости всего пространства:

Theorem binary_processes_not_enumerable :
  ~ exists f : nat -> BinProcess,
      forall p, exists n, bp_eq (f n) p.

Никакая функция $f$ из номеров в бинарные процессы не накрывает их все: диагональ всегда ускользает.

{ Оговорим точно, чем эта теорема не является. Это не та же теорема, что unit_interval_uncountable_trisect_v2 из Главы 4.4. Та говорила о процессах Коши в отрезке $[0, 1]$ ; эта — о бинарных процессах в пространстве Кантора $2^{N}$ . Две разные модели — две разные теоремы Кантора, пусть и об <<одном и том же>> в неформальном смысле. Бинарная — проще и конструктивнее; и она расчищает площадку для главного. Несчётность установлена; теперь вопрос не <<сколько>> процессов, а как устроены их совокупности. }

Деревья и замкнутые совокупности

Дерево как разрешимый предикат

Чтобы говорить о строении совокупностей бинарных процессов, нужен аппарат деревьев. Бинарный процесс прокладывает путь через развилки: на каждом шаге — влево (false) или вправо (true). Конечный отрезок такого пути — это конечный список булевых значений; а дерево — это указание, какие конечные отрезки допустимы.

В ProcessTypes.v дерево определено так:

Definition PrunedTree := list bool -> bool.

Дерево — это функция из конечных бинарных строк в булевы значения: для каждой строки она говорит true (строка — узел дерева) или false (не узел). Существенно, что значение здесь — bool, а не Prop. Это разрешимый предикат: членство строки в дереве — конечная операция, завершающаяся определённым ответом. Таков $P 4$ -рефакторинг: принадлежность узла дереву надо проверять за конечное число шагов, а не <<устанавливать>> как логическое свойство. И действительно, файл доказывает разрешимость прямо — леммы tree_mem_dec, is_splitting_dec и другие, причём доказывает без обращения к классической логике, простым разбором булевых значений.

Что требуется от дерева

Не всякая функция list bool -> bool есть дерево. Условие <<быть деревом>> задаёт предикат is_tree:

Definition is_tree (T : PrunedTree) : Prop :=
  T [] = true /\
  forall sigma, T sigma = true -> T (removelast sigma) = true.

Два требования. Первое: пустая строка — корень — есть узел ( $T [] = ‘ t r u e ‘$ ). Второе: префикс-замкнутость — если строка есть узел, то и строка без последнего элемента (removelast) есть узел. Иначе говоря: всякий узел достижим из корня, дерево не имеет <<висящих в воздухе>> кусков.

Здесь нужна точность, чтобы не прочесть определение сильнее, чем оно есть. Тип называется PrunedTree — <<подрезанное дерево>>, — но is_tree не требует, чтобы у каждого узла был хотя бы один ребёнок, — то есть не требует отсутствия <<тупиков>>. <> здесь — имя типа, а не доказанное математическое свойство. Условие is_tree — ровно два пункта: корень и префикс-замкнутость, и ничего сверх. Свойства ветвления, когда они понадобятся, задаются отдельно — через предикат is_perfect и связанные с ним леммы (§ 5.5).

Пути и замкнутые совокупности

Бесконечный путь через дерево — это бинарный процесс, всякий конечный начальный отрезок которого есть узел дерева. В файле — предикат is_path: процесс $p$ есть путь дерева $T$ , если для всякого $n$ начальный отрезок $p$ длины $n$ принадлежит $T$ .

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

Definition is_closed (C : BinCollection) : Prop :=
  exists T : PrunedTree,
    is_tree T /\ forall p, C p <-> is_path T p.

$C$ замкнута, если существует дерево $T$ , такое что членство в $C$ равносильно <<быть путём $T$ >>. Замкнутая совокупность — это в точности совокупность, заданная деревом.

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

И именно к замкнутым совокупностям — не к произвольным — будет относиться главная теорема. Это первый из её предохранителей, и далее глава будет держать его постоянно.

Совершенные поддеревья

Ветвящийся узел

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

Узел дерева — конечная строка — может иметь продолжения. Влево, если строка с приписанным false тоже есть узел (has_left); вправо, если строка с true есть узел (has_right). Узел называется ветвящимся, если у него есть оба продолжения:

Definition is_splitting (T : PrunedTree) (sigma : list bool) : Prop :=
  has_left T sigma /\ has_right T sigma.

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

Совершенное дерево

Дерево называется совершенным, если ветвление в нём не иссякает — если из всякого узла можно дойти до ветвящегося:

Definition is_perfect (T : PrunedTree) : Prop :=
  is_tree T /\
  forall sigma, T sigma = true ->
    exists tau, T (sigma ++ tau) = true /\
                is_splitting T (sigma ++ tau).

Из любого узла $σ$ найдётся продолжение $τ$ , ведущее к ветвящемуся узлу $σ + + τ$ . В совершенном дереве, куда ни зайди, впереди всегда есть новая развилка. Ветвление возобновляется без конца.

Совокупность содержит совершенное подмножество, если какое-то совершенное дерево целиком вложено в неё путями. Определение has_perfect_subset это и говорит: существует древесная структура — с корнем, префикс-замкнутая, совершенная (всякий узел продолжается до ветвящегося), — все пути которой лежат в совокупности.

Два уровня: разрешимое дерево и логический свидетель

Здесь — важная архитектурная тонкость, которую глава обязана назвать прямо. Деревья замкнутых совокупностей (§ 5.4) заданы разрешимо: тип PrunedTree есть list bool -> bool, членство узла — конечная вычислимая проверка. Но совершенное поддерево, которое извлекает главная теорема, задано иначе. В определении has_perfect_subset свидетель — структура

mem : list bool -> Prop

со значениями в Prop, не в bool. Это логический предикат, не обязательно вычислимый.

Различие не случайно, и это не оплошность формализации, а сознательная граница. Исходное дерево замкнутой совокупности — разрешимо: про всякую строку за конечное время известно, узел она или нет. А совершенное поддерево, добываемое теоремой Кантора–Бендиксона, — его ядро, — может быть задано лишь как логическое свойство: <<строка принадлежит ядру>> — утверждение, для которого вычислимой проверки может не быть. Поэтому глава, говоря о $P 4$ -разрешимости, держит два уровня раздельно: членство в исходном дереве — конечная проверка (bool); членство в совершенном ядре — логическое свойство (Prop). Сказать, что вся конструкция совершенного ядра разрешима, было бы неверно; разрешимо исходное дерево, а ядро — предикат над Prop.

Что такое <<совершенное>> содержательно

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

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

Дихотомия Кантора–Бендиксона{Дихотомия Кантора-Бендиксона}

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

Весь аппарат собран — бинарные процессы, деревья, замкнутость, ветвление, совершенство, — и можно высказать центральную теорему главы. В ProcessContinuumHypothesis.v она записана так:

Theorem process_continuum_hypothesis :
  forall C : BinCollection,
    is_closed C ->
    is_enumerable C \/ has_perfect_subset C.

Прочтём дословно. Для всякой совокупности бинарных процессов $C$ , если она замкнута, верно одно из двух: либо $C$ перечислима, либо $C$ содержит совершенное подмножество. Союз <<либо – либо>> здесь — доказанная дихотомия: одна из двух возможностей непременно имеет место.

Сразу отметим оба условия — предохранителя теоремы. Во-первых, $C$ обязана быть замкнутой: теорема говорит о совокупностях, заданных деревом (§ 5.4), а не о произвольных BinCollection. Во-вторых, всё происходит в бинарной модели — в пространстве Кантора (§ 5.2), не в модели Коши отрезка. Внутри этих рамок дихотомия полная.

Концептуальное ядро доказательства

Доказательство теоремы технически длинное, но его идея — одна, и она замечательно ясна. Стоит изложить именно идею, не пересказывая выкладок.

Вопрос дихотомии — почему между <<перечислимо>> и <<содержит совершенное подмножество>> нет ничего третьего, промежуточного. Ответ держится на одной альтернативе, касающейся ветвления.

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

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

Если нет — если повторное ветвление в какой-то момент иссякает, — происходит вот что. Раз нет узла, расщепляющегося в обе стороны с продолжением, существенная для неперечислимости часть дерева больше не может удерживаться двумя ветвящимися направлениями и для целей классификации путей сводится к главной цепи со счётно классифицируемыми отклонениями. Можно выделить одну главную цепь — единственный <<магистральный>> путь (в файле он строится функцией выбора направления pick_dir). И тогда всякий путь дерева устроен просто: он либо следует этой главной цепи до конца, либо отклоняется от неё — и у отклонения есть первый шаг, на котором путь сошёл с магистрали. Путей, следующих главной цепи, не больше одного. А отклонившиеся пути классифицируются по номеру первого отклонения: для каждого номера — свой класс, и каждый такой класс перечислим. Всех классов — счётное число (по одному на номер шага), а счётное объединение перечислимых совокупностей перечислимо. Значит, и вся совокупность перечислима. Это первый полюс дихотомии.

Вот и всё ядро: либо ветвление возобновляется без конца — и тогда есть совершенное подмножество; либо ветвления не хватает — и тогда дерево есть цепь со счётными отклонениями, а совокупность перечислима. Промежуточному просто негде поместиться: возобновляемого ветвления либо хватает на совершенное поддерево, либо нет — и тогда структура схлопывается в счётный режим. В формализации эту развилку несут две леммы: no_split_implies_enum (нет возобновляемого ветвления $\Rightarrow$ перечислимо) и perf_subtree_has_splitting (совершенное поддерево всегда где-то ветвится).

Два полюса населены

Дихотомия была бы пустой, окажись один из её исходов невозможным. Файл проверяет, что оба исхода реальны, двумя предельными случаями. Пустая совокупность замкнута и перечислима (empty_closed_enum) — это полюс перечислимости. А вся совокупность бинарных процессов имеет совершенное подмножество (full_has_perfect) — полюс совершенства. Обе стороны дихотомии населены: ни <<перечислимо>>, ни <<содержит совершенное подмножество>> не пустует.

Имена теоремы

{ Файл даёт центральному результату и второе имя — no_intermediate_process_type, — доказывая его дословным повторением первого. Имя выбрано говорящим: оно подчёркивает суть — нет промежуточного типа. Замкнутая совокупность бинарных процессов попадает в одну из двух структурных альтернатив: она перечислима или содержит совершенное подмножество. Главное для настоящей главы — отсутствие промежуточного случая: если замкнутая совокупность не перечислима, она уже содержит совершенное подмножество. Именно это и несёт третья формулировка теоремы, PCH_structural_dichotomy: замкнутая и не перечислимая совокупность непременно содержит совершенное подмножество — та же дихотомия, прочитанная как импликация. (Что две альтернативы вдобавок взаимно исключают друг друга — перечислимая замкнутая совокупность не содержала бы совершенного подмножества, — математически ожидаемо для пространства Кантора, но отдельной леммы о несовместимости в опорном файле не выделено; глава поэтому говорит об отсутствии промежуточного случая, не утверждая формальную взаимоисключаемость как доказанную.) }

Процессное прочтение континуум-гипотезы

Имя и его опасность

Центральная теорема названа в файле process_continuum_ hypothesis — <<процессная континуум-гипотеза>>. Имя выразительное, и оно требует осторожного разбора, иначе прочтётся куда сильнее, чем теорема есть.

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

Что теорема есть на самом деле

Чем же она является? Формально process_continuum_hypothesis — это процессная версия классической теоремы Кантора–Бендиксона, известной также как теорема о совершенном множестве (perfect set dichotomy). Классическая теорема Кантора–Бендиксона говорит: всякое замкнутое подмножество подходящего пространства либо счётно, либо содержит совершенное подмножество. Это — структурная теорема о замкнутых множествах, и она доказуема обычными средствами, в отличие от континуум-гипотезы.

{ Процессная версия — ровно то, что разобрано в § 5.6: всякая замкнутая совокупность бинарных процессов либо перечислима, либо содержит совершенное подмножество. Это структурная дихотомия, а не утверждение о мощности. Имя файла no_intermediate_process_ type называет суть точнее заглавного: нет промежуточного структурного типа. }

Как дихотомия занимает место вопроса о континууме

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

И вот на этот, переформулированный вопрос теорема даёт ответ — ответ отрицательный и доказанный. Замкнутая совокупность бинарных процессов бывает либо <<перечислимого типа>> (обходима счётным списком), либо <<континуального типа>> (содержит совершенное подмножество). Промежуточного структурного типа нет. Дихотомия Кантора–Бендиксона занимает место, на котором классически стоял вопрос о промежуточной мощности: тот же интерес — есть ли что-то между счётным и континуальным, — но поставленный структурно и получивший строгий ответ.

Подчеркнём границу ещё раз, чтобы она стояла твёрдо. Это не решение классической континуум-гипотезы и не заявка на него. Это другая теорема — Кантора–Бендиксона, — которая под $P 4$ занимает место классического вопроса о континууме, переведя его из языка мощностей в язык структурных типов. <<Процессная континуум-гипотеза>> — имя по этой роли, а не по тождеству с классическим утверждением.

Почему это и есть процессный континуум

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

Разбор E/R/R: процессный континуум как система

{ Закрепим прочитанное разбором E/R/R (Часть I). Шапка опорного файла задаёт разметку прямо: элементы — бинарные процессы (пространство Кантора $2^{N}$ ); роли — замкнутые совокупности, совершенные поддеревья, пути; правила — дихотомия континуум-гипотезы, Кантора–Бендиксон.¹ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе: дихотомия доказана в бинарной модели $2^{N}$ , отдельной от модели Коши Глав 4.2–4.4 (§ 5.8); <<система>> — содержательная интерпретация над типом BinProcess, читаемым операционально.}

{ Rules — правила (законы $L 3$ , $L 4$ ). Конституция — сама дихотомия Кантора–Бендиксона (process_continuum_hypothesis): всякая замкнутая совокупность либо перечислима, либо содержит совершенное подмножество, и промежуточного структурного типа нет (no_intermediate_process_type). К ней — разрешимое дерево (PrunedTree, предикат над конечными префиксами) и счётное объединение перечислимых классов (countable_union_enum). Логические средства — ровно две аксиомы: $L 3$ (classic) и $L 4$ (L4_witness; последний извлекает перечислитель класса — работа, похожая на выбор, но на уровне свидетелей, не теоретико-множественная аксиома выбора, § 5.8).

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

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — бинарные процессы, BinProcess := nat -> bool (пространство Кантора $2^{N}$ ). По $L 1$ каждый тождествен себе. По $P 4$ это тип процессных правил (правило отвечает на конечный запрос $n$ значением true/false), а не завершённое множество; завершённого несчётного объекта на уровне элементов нет (§ 5.2).}

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

Компонент	Что фиксирует	E/R/R
дихотомия КБ; нет промежуточного типа	конституция (развилка)	Rule
разрешимое дерево; счётное объединение ( $L 4$ )	замкнутость, нумерация	Rule
два типа: перечислимый / континуальный	роли (структурные типы)	Role
совершенное поддерево; пути	ядро и носимое	Role
бинарные процессы (`nat -> bool`, $2^{N}$ )	носители (тип, $P 4$ )	Element
законы $L 1$ – $L 5$ (здесь $L 3$ , $L 4$ )	универсальный слой	Rule (универс.)

{ Хорошая сформированность. Разметка однозначна: бинарные процессы — элементы, два типа и совершенное ядро — роли, дихотомия и дерево — правила. Соблюдён $P 1$ : совокупность есть совокупность процессов, дерево — разрешимый предикат над конечными префиксами; самочленства нет. И здесь разбор оборачивается диагностикой — завершающей процессную линию. <<Континуум-гипотеза>> в имени теоремы опасна (§ 5.7.1): принять её за решение мощностной КГ или за несчётное множество — то же смешение категорий, что лежит в корне всего тома ( $P 4$ , Глава 4.1): структуру (правило-развилку) читают как объект. В верной разметке <<процессный континуум>> — не вещь и не мощность, а роль-тип: доказанная структурная развилка. Честные границы: взаимоисключаемость двух типов отдельной леммой не выделена (глава говорит об отсутствии промежуточного случая, не о доказанной несовместимости); совершенное ядро — логический свидетель (Prop), не разрешимое дерево; модель $2^{N}$ держится отдельно от Коши.}

Что даёт разбор. Континуум, прочитанный по E/R/R, — последняя из процессных переустановок: бесконечность стала процессом (Глава 4.1), число — процессом (4.2), точка — классом (4.3), несчётность — правилом о процессах (4.4), а континуум — структурным типом, развилкой между счётным и неиссякающе ветвящимся. Всякий раз объект классической картины оказывается ролью или правилом процессной.

Что доказано и на чём оно стоит. Итог Части IV

Что доказано

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

Дихотомия установлена в бинарной модели — пространстве Кантора $2^{N}$ , — отдельной от модели Коши Глав 4.2–4.4. Это сознательное разделение: модель Коши ближе к числовой прямой и хороша для разговора о величинах; бинарная модель чище для разговора о структуре. Две модели — две ветви процессной формализации континуума, и глава работала во второй.

На чём это стоит

Назовём логические средства. Центральная теорема в ProcessContinuumHypothesis.v опирается на две аксиомы — оба раза это законы логики ToS. Первая — $L 3$ , классическая логика (аксиома classic). Вторая — $L 4$ , закон достаточного основания (в файле — L4_witness).

Стоит сказать, где появляется $L 4$ , потому что место это поучительное. Доказательство в одном месте берёт счётное объединение перечислимых совокупностей — когда отклонившиеся от главной цепи пути собираются в один класс по всем номерам первого отклонения (§ 5.6). Чтобы такое объединение осталось перечислимым, нужны две вещи. Первая — канторова кодировка пар натуральных чисел из стандартной библиотеки: техническая функция, взаимно однозначно сопоставляющая паре $(a, b)$ один номер; она позволяет занумеровать <<номер класса плюс номер внутри класса>> одним числом. Это вычислительный приём, а не <<мощность континуума>> — просто способ свести двойную нумерацию к одинарной. Вторая — $L 4$ , L4_witness: для каждого класса он извлекает конкретный перечислитель. Закон достаточного основания здесь и работает: у каждого перечислимого класса есть основание — свидетель его перечислимости, — и $L 4$ позволяет этот свидетель взять.

{ И — столь же важно — назовём, чего в доказательстве нет. Нет аксиомы выбора как отдельной теоретико-множественной аксиомы — акта выбора над завершённым семейством множеств. Оговорить, впрочем, надо точно. L4_witness в countable_union_enum выполняет работу, похожую на выбор, но на уровне свидетелей: из доказательства перечислимости каждого класса он извлекает конкретный перечислитель. Поэтому верная формулировка такая: доказательство не использует отдельную сет-теоретическую аксиому выбора над завершёнными семействами множеств, но использует $L 4$ -свидетельствование как внутренний закон ToS. Это не теоретико-множественный выбор, а закон достаточного основания в работе — и назвать его честнее, чем умолчать. }

Нет и завершённой бесконечности как готового объекта: ZFC- подобной аксиомы бесконечности доказательство не использует. Здесь тоже нужна оговорка, чтобы не возникло ложного впечатления. Разумеется, индуктивный тип nat и функциональные типы — nat -> bool, BinCollection — в доказательстве используются: это типы языка Rocq, и их $P 4$ -чтение процессное, типовое, а не как завершённых множеств (§ 5.2). Не используется именно сет-теоретическая аксиома завершённой бесконечности — постулат о готовом бесконечном множестве как актуальном объекте. Файл проверяет это машинно — командой Print Assumptions, которая для указанной теоремы выводит список аксиом, от которых та зависит; в списке — $L 3$ и $L 4$ , и нет ни выбора, ни аксиомы бесконечности. (Как и в Главе 4.4, оговорим: Print Assumptions проверяет зависимости указанной теоремы, не <<сканирует файл>>.) Два вспомогательных файла стоят ещё легче: ProcessTypes.v и ProcessDiagonal.v обращаются к $L 3$ лишь по одной лемме каждый — а ключевая diagonal_differs (§ 5.3) не использует аксиом вовсе. Леммы разрешимости деревьев доказаны без обращения к классике; впрочем, сам ProcessTypes.v импортирует модуль законов ToS, и одна его лемма — not_enum_union, разбирающая неперечислимость объединения, — использует $L 3$ . Так что говорить надо точно: разрешимость деревьев — без аксиом, файл в целом — с одной.

Итог главы. Переход к Главе 4.6

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

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

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

{Второе: на чём это стоит. Дихотомия доказана в бинарной модели — пространстве Кантора $2^{N}$ , отдельной от модели Коши Глав 4.2–4.4, — на трёх опорных файлах. Центральная теорема опирается на две аксиомы — законы логики $L 3$ и $L 4$ ( $L 4$ — для счётного объединения перечислимых классов). Отдельная теоретико-множественная аксиома выбора и аксиома завершённой бесконечности не используются.}

{Третье: что остаётся открытым. Теорема относится к замкнутым совокупностям — заданным деревом; произвольные совокупности она не охватывает. Совершенное поддерево извлекается как логический свидетель (предикат над Prop), не как разрешимое дерево — $P 4$ -разрешимо исходное дерево совокупности, но не ядро Кантора–Бендиксона. Отношение двух моделей теперь установлено частично: файл ProcessBinReal.v строит прямой перевод bin_to_real $: 2^{N} \to [0, 1]$ (bin_to_real_in_interval, bin_to_real_is_Cauchy — последняя опирается на $L 3$ ) и доказывает образцовое отождествление bin_ones_equiv_one ( $0, 111 \dots_{2} = 1$ ). Открытым остаётся полный перевод — обратное отображение $[0, 1] \to 2^{N}$ , общая неоднозначность записи и перенос самой дихотомии Кантора–Бендиксона на модель Коши; связь двух ветвей в полном объёме ждёт отдельного исследования.}

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

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

Навигация: ← Глава 4. Несчётность процессов · Глава 6. P4 как фильтр →

E/R/R-разметка в шапке файла ProcessContinuumHypothesis.v; здесь разворачивается по образцу Части I. ↩

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

Проводник