Глава 3. Счётность рациональных чисел

Что значит счётность в Теории Систем

Вопрос, оставленный предыдущей главой

Глава III.2 построила рациональные числа — координатную разметку с соразмерным шагом — и в конце оставила вопрос, который сама лишь обозначила. Рациональные числа суть позиции соразмерной разметки, и разметка эта не завершена: за всякой достигнутой позицией есть следующая, всякий отрезок делим ещё тоньше. Можно ли тогда говорить о рациональных числах как о списке — перечислить их одно за другим так, чтобы всякое было достигнуто?

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

Счётность в стандартном изложении

Стандартное определение таково. Множество $X$ называется счётным, если существует биекция $f : N \to X$ — взаимно однозначное соответствие между натуральными числами и элементами $X$ . Множество счётно, если такая функция существует.

В этом определении две вещи приняты как сами собой разумеющиеся. Первая: $N$ и $X$ берутся как готовые множества — завершённые совокупности, лежащие наготове, между которыми устанавливается соответствие. Вторая: счётность есть существование функции — факт о том, что функция в принципе есть, безотносительно к тому, предъявлена ли она.

Для стандартной математики оба допущения привычны и работают. И стоит сразу сказать прямо: ToS не объявляет стандартное определение неприменимым. Само свойство счётности вполне можно выразить и формально — как утверждение об инъективности и сюръективности некоторой функции; именно в таком виде оно и доказывается в Rocq, и ToS этим доказательством пользуется. Различие ToS со стандартным изложением не в том, что стандартное понятие неприложимо, а в том, какой методологической формы ToS от счётности требует. Как показала уже Часть II, ToS не берёт бесконечные совокупности готовыми (принцип $P 4$ ): натуральный ряд не есть завершённое множество, а потенциально продолжаемый ряд; и рациональные числа, как показала Глава III.2, не суть завершённое множество, а потенциальная разметка. Поэтому ToS требует от счётности не просто утверждения о существовании соответствия, а более сильной формы: явного обхода, который можно вычислить, проследить шаг за шагом и обратить. Не <<функция в принципе есть>>, а <<вот процедура, и она работает>>. Счётность в ToS читается операционально — и эту операциональную форму глава далее и выстраивает.

Счётность как процедура обхода

ToS переопределяет счётность операционально.

Совокупность счётна, если существует конструктивная процедура, которая по всякому натуральному числу $n$ строит $n$ -й элемент обхода, и обратная процедура, которая по всякому элементу находит его номер.

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

Стоит оговорить, что это — усиленная форма счётности. Обычная счётность в стандартной математике может задаваться по-разному — сюръекцией $N \to X$ , инъекцией $X \to N$ , биекцией либо перечислением, — и не всякая из этих форм требует уметь эффективно находить номер по предъявленному элементу. Требование обратной процедуры — <<по элементу найти его номер>> — сильнее минимального: это эффективная индексация с вычислимым обращением. ToS в этой главе берёт именно сильную, операциональную форму: не только процедуру $n \mapsto x_{n}$ , но и обратную к ней. Это — рабочее усиление, и оно избрано не случайно: для рациональных чисел такая усиленная форма, как покажет глава, доступна — обход дерева Калкина–Уилфа обратим, и обратный ход тоже строится явно.

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

Что предстоит показать

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

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

Зачем нужна явная биекция

Стандартное доказательство счётности

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

Доказательство верное, и в рамках стандартной математики ему нечего возразить. Стоит лишь заметить, чем именно оно доказывает счётность. Оно доказывает её через общие теоремы: ссылается на теорему о счётности произведения и подмножеств, та — на свои основания, и в итоге утверждается, что биекция между натуральными и рациональными числами существует. Такой маршрут корректен — но он скрывает сам механизм обхода: какова биекция, как она устроена, что она даёт на входе $n = 5$ или $n = 100$ , из доказательства через общие теоремы прямо не видно. Стоит, впрочем, не впасть в карикатуру: стандартная математика не ограничена этим абстрактным маршрутом — учебные доказательства нередко дают и явное диагональное перечисление пар, и обходы вроде дерева Калкина–Уилфа или Штерна–Броко. ToS не упрекает стандартный подход в недостатке строгости. Она лишь выбирает из двух возможных маршрутов не абстрактный, а явный: не сослаться на теорему о счётности произведения, а построить конкретную функцию перечисления и её обратный ход.

Почему этого недостаточно для Теории Систем

Для ToS такое доказательство неудовлетворительно — и неудовлетворительно не по строгости, а по существу.

Счётность в ToS (§ 3.1) есть не существование биекции, а наличие работающей процедуры обхода. Сказать <<биекция существует>> значит ответить не на тот вопрос. Операциональное понимание счётности спрашивает: есть ли обход, и доходит ли он до всякого элемента? Ответ <<функция, осуществляющая обход, в принципе существует>> этого вопроса не закрывает: существование функции и наличие процедуры, которую можно запустить и проследить, — не одно и то же.

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

Требуется явная процедура

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

И такая процедура есть. Она называется перечислением Калкина–Уилфа, и устроена так, что по всякому номеру строит рациональное число, а по всякому рациональному числу — его номер, причём строит вычислимо: всякий шаг есть конкретное действие, которое можно совершить и проверить. ToS формализует это перечисление полностью — и формализует, что важно, конструктивно: без ссылок на отвлечённые теоремы существования, одним лишь построением.

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

К построению перечисления

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

Дерево Калкина–Уилфа

Положительные рациональные числа как пары

Построение обхода начинается с положительных рациональных чисел — с позиций соразмерной разметки по одну сторону опоры. На них обход и будет задан; распространение его на все рациональные числа, вместе с нулём и отрицательной стороной, прибавляется потом и просто (§ 3.5).

Положительное рациональное число берётся здесь через пару натуральных чисел — числитель и знаменатель.¹ В Rocq это записывается так:

Definition QPos := (positive * positive)%type.

Тип QPos есть тип всех положительных пар $(a, b)$ : первая составляющая — числитель, вторая — знаменатель. Здесь нужны две оговорки. Первая — о типе positive. В стандартной библиотеке Rocq positive — это отдельный технический тип положительных натуральных значений в двоичной записи; он не тождествен типу nat с условием $n > 0$ и не есть тот первичный ряд $N$ от единицы, о котором говорила Часть II. Роль его в этой главе проста и чисто служебная: он гарантирует, что числитель и знаменатель положительны, а знаменатель в особенности не равен нулю. Вторая оговорка — о соотношении пар и рациональных значений. Тип QPos содержит все пары, в том числе сократимые: $(2, 4)$ и $(1, 2)$ — разные элементы QPos. Но дерево Калкина–Уилфа, как покажет глава, перечисляет именно те пары, где числитель и знаменатель взаимно просты; эти несократимые пары и служат каноническими представителями положительных рациональных чисел. Брать положительное рациональное число через пару удобно тем, что устраняет с самого начала заботу о знаке и о нуле: пара positive ни того, ни другого не допускает по устройству типа.

Корень и два ребёнка

Дерево Калкина–Уилфа размещает положительные рациональные числа по узлам так, что каждое попадает в дерево ровно один раз. Устроено оно тремя правилами.

Корень дерева есть дробь $1/1$ :

Definition cw_root : QPos := (1, 1).

Левый ребёнок узла $a / b$ есть дробь $a / (a + b)$ ; правый ребёнок — дробь $(a + b) / b$ :

Definition cw_left  (ab : QPos) : QPos :=
  let (a, b) := ab in (a, a + b).
Definition cw_right (ab : QPos) : QPos :=
  let (a, b) := ab in (a + b, b).

От корня $1/1$ влево лежит $1/2$ , вправо — $2/1$ . От $1/2$ влево — $1/3$ , вправо — $3/2$ . От $2/1$ влево — $2/3$ , вправо — $3/1$ . И так без конца: всякий узел даёт двух детей, дерево ветвится бесконечно.

Три свойства дерева

Дерево Калкина–Уилфа — не произвольная раскладка дробей по узлам, а структура с тремя свойствами, и в этих свойствах вся его сила.

Первое: всякое положительное рациональное число стоит в дереве, и стоит ровно один раз. Здесь нужна точность в том, что считать <<тем же>> числом. Если рациональное число понимать как значение, то каждое положительное рациональное значение появляется в дереве ровно один раз — ни пропусков, ни повторов. Если же понимать дробь как сырую пару числителя и знаменателя, то дерево перечисляет не все пары, а только несократимые: сократимая запись вроде $2/4$ в дереве не появляется — она уже представлена узлом $1/2$ . Иначе говоря, дерево обходит несократимые пары как канонических представителей, и в этом смысле каждое положительное рациональное значение достигается единожды.

Второе: всякая дробь в дереве несократима. В каждом узле числитель и знаменатель взаимно просты — не имеют общего делителя больше единицы. Дерево не порождает $2/4$ или $3/6$ ; оно порождает сразу $1/2$ , в несократимом виде. Это свойство не привнесено проверкой, а вытекает из устройства дерева: корень $1/1$ несократим, а оба правила — левый ребёнок и правый — несократимость сохраняют. ToS доказывает это формально — теоремой о том, что наибольший общий делитель числителя и знаменателя в каждом узле равен единице.²

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

Дерево Калкина–Уилфа размещает положительные рациональные числа по узлам: корень есть $1/1$ , левый ребёнок узла $a / b$ есть $a / (a + b)$ , правый — $(a + b) / b$ . Дерево обладает тремя свойствами: всякое положительное рациональное число стоит в нём ровно один раз; всякая дробь в нём несократима (что ToS доказывает формально); дерево бинарно — у всякого узла два ребёнка. Эти свойства и делают дерево основой обхода рациональных чисел.

От дерева к обходу

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

Обход дерева: навигация двоичным путём

Путь к узлу есть череда выборов

Дерево Калкина–Уилфа размещает положительные рациональные числа по узлам (§ 3.3). Чтобы получить из него обход, нужно связать узлы с натуральными числами — так, чтобы по всякому номеру отыскивался узел, а по всякому узлу — номер. Сделать это позволяет одно простое наблюдение об устройстве дерева.

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

Череда выборов записывается числом

Конечную череду выборов <<влево или вправо>> можно записать числом — и это ключ ко всему обходу.

Натуральное число в двоичной записи есть не что иное, как конечная череда двоичных знаков. ToS пользуется этим прямо. Путь к узлу кодируется натуральным числом по трём правилам: число $1$ есть путь к корню; если число $p$ кодирует путь к некоторому узлу, то число, записанное как $p$ с приписанным двоичным нулём, кодирует путь к его левому ребёнку, а $p$ с приписанной двоичной единицей — к правому. В Rocq, где натуральное число типа positive само построено из двоичных конструкторов, это записывается прямо:

Fixpoint cw_node (p : positive) : QPos :=
  match p with
  | xH    => cw_root            (* 1 = root *)
  | xO p' => cw_left  (cw_node p')   (* left child *)
  | xI p' => cw_right (cw_node p')   (* right child *)
  end.

Функция cw_node читает число как путь и проходит дерево от корня до нужного узла.³ Конструктор xH — единица — даёт корень. Конструкторы xO и xI интуитивно соответствуют добавлению к уже заданному пути ещё одного двоичного шага — перехода к левому либо к правому ребёнку: xO ведёт к левому ребёнку того узла, к которому ведёт остаток пути, xI — к правому. Технические подробности порядка битов в индуктивном представлении типа positive здесь не важны; важно одно: каждый из двух конструкторов однозначно кодирует следующий переход по дереву. Так всякое число типа positive прочитывается как маршрут по дереву, а всякому маршруту отвечает узел — положительное рациональное число.

Перечисление

Остаётся связать с узлами не числа типа positive, а натуральные числа обхода — $0, 1, 2, 3, \dots$ , — чтобы обход начинался с нуля, как положено перечислению. Это делается сдвигом на единицу:

Definition enum_QPos (n : nat) : QPos :=
  cw_node (Pos.of_nat (S n)).

Перечисление enum_QPos берёт натуральное число $n$ , прибавляет к нему единицу и читает результат как путь по дереву. Сдвиг на единицу нужен затем, что пути нумеруются с единицы (путь $1$ есть корень), а обход — с нуля.

Проследим первые его шаги. Номер $0$ : путь $1$ , корень — дробь $1/1$ . Номер $1$ : путь $2$ , что есть двоичный нуль при единице, — левый ребёнок корня, дробь $1/2$ . Номер $2$ : путь $3$ , двоичная единица при единице, — правый ребёнок корня, $2/1$ . Номер $3$ : путь $4$ — левый ребёнок узла с путём $2$ , то есть левый ребёнок дроби $1/2$ , — $1/3$ . Номер $4$ : путь $5$ — правый ребёнок дроби $1/2$ , — $3/2$ . Обход выстраивает положительные рациональные числа в ряд:

\frac{1}{1}, \frac{1}{2}, \frac{2}{1}, \frac{1}{3}, \frac{3}{2}, \frac{2}{3}, \frac{3}{1}, \dots

Это и есть перечисление Калкина–Уилфа: процедура, которая по всякому номеру $n$ строит $n$ -е положительное рациональное число, и строит его вычислимо — всякий шаг есть конкретное действие: прибавить единицу, прочитать двоичные знаки, пройти дерево.

Путь от корня дерева к любому узлу есть конечная череда выборов <<влево или вправо>>, а такая череда записывается натуральным числом в двоичном виде: единица — корень, приписанный двоичный нуль — левый ребёнок, приписанная единица — правый. Функция cw_node читает число как путь и находит узел; перечисление enum_QPos сдвигает нумерацию к нулю и строит по номеру $n$ положительное рациональное число. Первые члены обхода — $1/1, 1/2, 2/1, 1/3, 3/2, \dots$ . Это вычислимая процедура: всякий шаг есть конкретное действие.

Чего недостаёт до биекции

Половина дела сделана: есть процедура, которая по номеру строит рациональное число. Но счётность в смысле ToS (§ 3.1) требует и обратного — процедуры, которая по рациональному числу находит его номер, — и требует доказательства, что обе процедуры точно обращают друг друга. Этим — обратной процедурой и доказательством биекции — глава занимается дальше.

Обратная процедура и биекция

От дроби к её номеру

Перечисление строит по номеру дробь (§ 3.4). Счётность в смысле ToS требует и обратного: по дроби — её номер. Эта обратная процедура устроена так же прозрачно, как прямая, и опирается на ту же связь узла с путём.

Дано положительное рациональное число $a / b$ . Найти его номер значит проследить путь от его узла назад к корню. Делается это по устройству дерева. Если $a = b$ , дробь есть $1/1$ — сам корень, путь пуст. Если $a < b$ , дробь есть левый ребёнок некоторого узла: левый ребёнок узла $c / d$ есть $c / (c + d)$ , значит узел-родитель восстанавливается как $a / (b - a)$ . Если $a > b$ , дробь есть правый ребёнок, и родитель есть $(a - b) / b$ . Повторяя этот шаг, мы поднимаемся от узла к родителю, от родителя к его родителю, и так до корня, записывая по дороге, левым или правым ребёнком был всякий узел. В Rocq это записывается так:

Fixpoint path_to_node_fuel (fuel : nat) (a b : positive)
  : positive :=
  match fuel with
  | O => xH
  | S fuel' =>
      if (a =? b) then xH
      else if (a <? b)
           then xO (path_to_node_fuel fuel' a (b - a))
           else xI (path_to_node_fuel fuel' (a - b) b)
  end.

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

Definition index_of_QPos (ab : QPos) : nat :=
  Pos.to_nat (path_to_node ab) - 1.

Две процедуры обращают друг друга

Есть, стало быть, две процедуры: прямая — от номера к дроби, и обратная — от дроби к номеру. Чтобы они вместе составляли биекцию, нужно, чтобы они точно обращали друг друга: пройдя номер в дробь и обратно, вернуться к тому же номеру; пройдя дробь в номер и обратно, вернуться к той же дроби.

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

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

Отсюда — главная теорема главы: перечисление положительных рациональных чисел есть биекция.

Theorem Q_positive_countable :
  (forall n m, enum_QPos n = enum_QPos m -> n = m) /\
  (forall a b, Z.gcd (Z.pos a) (Z.pos b) = 1%Z ->
     exists n, enum_QPos n = (a, b)).

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

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

Все рациональные числа

Доказанное — и доказанное формально, теоремой Q_positive_countable — касается положительных рациональных чисел в несократимом представлении. Распространение обхода на все рациональные числа — вместе с нулём и отрицательной стороной — теперь тоже закреплено теоремами: и прямой ход (сюръекция), и обратный (по рациональному — его номер), а с ними и полная биекция $N \leftrightarrow Q$ . Глава приводит формулу обхода и указывает теоремы, её замыкающие.

Отрицательные рациональные числа суть те же положительные позиции, взятые по другую сторону опоры (Глава III.2, § 2.7); нуль есть сама опора. Обход всех рациональных чисел получается из обхода положительных так. Нулю даётся номер $0$ ; далее номера чередуются — нечётные несут положительную копию обхода, чётные (кроме нуля) — отрицательную. В явной записи, если $enum_{Q^{+}}$ есть построенный выше обход положительных рациональных, полный обход $E : N \to Q$ задаётся так:

E (0) = 0, E (2 n + 1) = + enum_{Q^{+}} (n), E (2 n + 2) = - enum_{Q^{+}} (n) .

Всякое рациональное число — положительное, отрицательное или нуль — получает в этом чередовании свой номер, и всякому номеру отвечает ровно одно рациональное число.

{ Здесь нужно быть точным относительно статуса этого шага — и теперь он замкнут. В файле Countability_Q.v приведённая формула реализована буквально: функция enum_Q задаёт $enum_{Q} (0) = 0$ , нечётному номеру сопоставляет положительную копию обхода, чётному (кроме нуля) — отрицательную. К ней построена обратная функция index_of_Q: по произвольному рациональному — через приведение к несократимому виду и обратный ход для положительных — она находит его номер, разбирая нуль, плюс и минус. Обе доказаны взаимно обратными — теоремами enum_Q_index_id ( $‘ e n u m_{Q} ‘ (‘ in d e x_{o} f_{Q} ‘ q) == q$ ) и index_of_Q_enum_id ( $‘ in d e x_{o} f_{Q} ‘ (‘ e n u m_{Q} ‘ n) = n$ ), — а соединяет их теорема Q_bijection:

(forall n, index_of_Q (enum_Q n) = n) /\ (forall q, enum_Q (index_of_Q q) == q).

Это полная биекция $N \leftrightarrow Q$ с вычислимым обращением — уже не только для положительных, а для всего $Q$ , конструктивно и без единой аксиомы (Print Assumptions Q_bijection: <>).

Остаётся единственная точность формулировки — не ограничение, а правильная мера. Биекция связывает $N$ с $Q$ , взятым с точностью до Qeq: обратный ход проходит через приведение Qred, так что $2/4$ и $1/2$ получают один номер. Иначе и нельзя — на сырых записях дробей биекции нет, ибо $2/4$ и $1/2$ суть разные записи одного числа (§ 2.5). Потому index_of_Q_enum_id точна на $N$ (равенство номеров), а enum_Q_index_id — с точностью до Qeq на $Q$ ; вместе это и есть биекция рациональных значений.}

Обратная процедура path_to_node по дроби прослеживает путь от её узла к корню и находит номер. Две теоремы о круговом обходе доказывают, что прямая и обратная процедуры точно обращают друг друга. Главная теорема Q_positive_countable утверждает, что перечисление инъективно и сюръективно, — то есть есть биекция для положительных рациональных чисел. Доказательство полностью конструктивно, без закона исключённого третьего: счётность не просто утверждена, а построена — и построение есть способ её доказать. Обход всех рациональных чисел — с нулём и отрицательной стороной — реализован функцией enum_Q по формуле $E (0) = 0$ , $E (2 n + 1) = + enum (n)$ , $E (2 n + 2) = - enum (n)$ ; к ней построен обратный ход index_of_Q, и теорема Q_bijection доказывает их взаимную обратность — полную биекцию $N \leftrightarrow Q$ (с точностью до Qeq, 0 аксиом) уже для всего $Q$ .

Что доказано

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

Что счётность значит онтологически

Рациональные числа имеют достижимый обход

Счётность рациональных чисел доказана построением обхода (§ 3.5). Стоит теперь сказать, что этот результат означает по существу — чем оказываются рациональные числа, коль скоро их можно так обойти.

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

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

Обычная бесконечность

Из счётности следует и то, какова бесконечность рациональных чисел.

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

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

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

Счётность и режим рассмотрения

Стоит связать сказанное с тем, как ToS вообще говорит о бесконечных совокупностях.

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

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

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

К следующему различению

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

Данные и поведение

Почему рациональные числа удалось обойти

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

Рациональное число обходимо потому, что оно есть конечный объём данных. Всё рациональное число без остатка задаётся парой натуральных чисел — числителем и знаменателем (§ 3.3). Пара эта конечна: числитель есть конкретное натуральное число, знаменатель — конкретное натуральное число, и всё. Записать рациональное число значит записать два числа — выражение конечной длины, которое можно выписать полностью и иметь перед собой целиком.

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

Процесс есть бесконечное поведение

Но не всё, о чём говорит математика, есть конечный объём данных. Есть предметы иного рода — и ToS встретит их в следующей части.

Возьмём процесс — скажем, бесконечную последовательность рациональных приближений, шаг за шагом уточняющих некоторую величину. Здесь нужна точность, иначе сказанное войдёт в противоречие с тем, что процесс часто можно задать конечно. Различить нужно три вещи. Отдельный вычислимый процесс вполне может иметь конечное описание — конечное правило, программу: <<на шаге $n$ выдай такую-то дробь>>. Но процесс как поведение не тождествен этой конечной записи: он разворачивается как бесконечная последовательность ответов — $0$ , $1$ , $2$ и так без конца, — и весь его ход, весь его график есть объект бесконечный. И, наконец, процесс как произвольная функция $N \to Q$ вообще не обязан иметь конечного описания: вычислимые процессы суть лишь часть всех функций $N \to Q$ .

Различие это — между данными и поведением — и проходит здесь. Данные суть нечто записанное, конечное, имеющееся целиком. Поведение есть способ отвечать, развёрнутый на всю бесконечность шагов; отдельное вычислимое поведение задаётся конечным правилом, но само поведение как бесконечная последовательность ответов конечной записью не исчерпывается. И решающее: тогда как совокупность конечных выражений — конечных программ — перечислима наравне с прочими конечными данными, совокупность всех функций $N \to Q$ к совокупности конечных программ не сводится: функций больше, чем конечных правил, и не всякая задаётся правилом. Рациональное число есть данные. Процесс есть поведение; и совокупность всех процессов-функций — не то же, что перечислимая совокупность конечных данных.

Граница перечислимого

Здесь — граница, к которой глава вела, и здесь же — задел к тому, что разворачивается за рациональными числами.

Совокупности конечных выражений счётного типа перечислимы — это глава показала и объяснила: их члены суть конечные записи над счётным запасом, а такие записи поддаются обходу. Натуральные числа, целые, рациональные — все суть конечные данные, и все перечислимы (§ 3.6). Но совокупность всех процессов — всех функций, отвечающих рациональным числом на всякий шаг, — устроена иначе. Отдельный вычислимый процесс задаётся конечной программой, и программы, как конечные выражения, перечислимы; но совокупность всех функций $N \to Q$ к совокупности конечных программ не сводится, и оснований, по которым перечислимы конечные данные, к ней не приложить. Перечислима ли совокупность всех процессов — настоящая глава не решает; она лишь отмечает, что вопрос этот иной и оснований для утвердительного ответа здесь нет.⁶

Этим очерчена граница. По одну её сторону — конечные данные: натуральные, целые, рациональные числа, обычная перечислимая бесконечность. По другую — бесконечное поведение, процессы; и бесконечность их, быть может, иного рода. Часть IV возьмётся именно за эту, другую сторону: построит процессы как самостоятельный предмет и разберёт, перечислимы ли они. Настоящая глава границу лишь называет, не переходя её. В терминах E/R/R здесь граница между конечными данными (рациональное — элемент) и бесконечным поведением (процесс); разбор § 3.8.3.

Рациональные числа удалось обойти потому, что всякое из них есть конечный объём данных — пара натуральных чисел, выражение конечной длины. Перечислима всякая совокупность конечных выражений над счётным алфавитом или конечным набором конструкторов; рациональные числа именно таковы. Процесс — правило, отвечающее рациональным числом на всякий шаг без конца, — задаётся конечной программой как отдельное вычислимое поведение, но совокупность всех функций $N \to Q$ к совокупности конечных программ не сводится. Здесь проходит граница: конечные данные (натуральные, целые, рациональные числа) перечислимы; перечислима ли совокупность всех процессов — вопрос Части IV.

К итогу главы

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

Итог. Переход к аномалиям рациональных чисел

Что прошла глава

Глава прошла счётность рациональных чисел.

Начала она с того, что уточнила саму счётность. Стандартное понимание — существование биекции — можно воспроизвести и формально, как утверждение об инъективности и сюръективности функции; ToS этим пользуется, но требует более сильной, операциональной формы: не утверждения о существовании соответствия, а явного обхода, который можно вычислить, проследить и обратить (§ 3.1). Отсюда следовало требование: не сослаться на теорему существования, а предъявить обход явно (§ 3.2). Глава его и предъявила — через дерево Калкина–Уилфа, размещающее всякое положительное рациональное число в единственном узле, и всякую дробь в несократимом виде (§ 3.3); через навигацию двоичным путём, связывающую узлы с натуральными числами (§ 3.4); через обратную процедуру и доказательство, что прямой и обратный обход точно обращают друг друга, — доказательство полностью конструктивное, без закона исключённого третьего (§ 3.5). Затем глава показала, что счётность означает онтологически: рациональные числа суть процессуально достижимый список, обычная перечислимая бесконечность — та же, что у натурального ряда (§ 3.6). И очертила границу: конечные данные перечислимы, процессы — бесконечное поведение — лежат по другую сторону (§ 3.7).

Рациональные числа перечислимы

Итог главы сводится к одному. Рациональные числа перечислимы — и перечислимы не по теореме существования, а на деле: есть обход, который до всякого из них доходит за конечное число шагов, и обход этот построен, выписан и конструктивно обоснован.

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

Разбор E/R/R: счётность как операциональный обход

{ Пройденную счётность стоит разобрать по E/R/R (Часть I): разбор закрепляет, чем операциональная счётность ToS богаче существования биекции. Опорный файл — Countability_Q.v (776 строк, без единой аксиомы, даже без закона исключённого третьего): дерево Калкина–Уилфа, перечисление enum_QPos и обратная index_of_QPos, теорема Q_positive_countable; а для всего $Q$ — функция enum_Q, обратная index_of_Q и теорема Q_bijection. Оговорка о статусе теперь снята: для всего $Q$ доказана полная биекция $N \leftrightarrow Q$ с вычислимым обращением — две круговые теоремы enum_Q_index_id и index_of_Q_enum_id, 0 аксиом — с единственной точностью, что $Q$ берётся до Qeq ( $2/4$ и $1/2$ получают один номер), иначе биекции и быть не может. Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements.}

Rules — правила (закон $L 5$ ). Конституция — построение дерева: корень и два правила ветвления (cw_left/cw_right), § 3.3. К нему — навигация: двоичный путь $\leftrightarrow$ узел, узел $\leftrightarrow$ номер (§ 3.4), и обратимость прямого и обратного обхода (enum_injective и enum_surjective дают Q_positive_countable, § 3.5). И правило канона: несократимость (enum_coprime) — всякое рациональное значение встречается ровно раз, $2/4$ не появляется отдельно от $1/2$ (§ 3.3). По $P 4$ обход есть процесс: до всякого рационального он доходит за конечное число шагов, а не предъявляет завершённый список.

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

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — узлы дерева (пары QPos, их представители — несократимые) и натуральные номера. По $L 1$ всякий узел тождествен себе. По $P 4$ всякое рациональное есть конечный объект — пара числитель/знаменатель, выражение конечной длины, — и потому поддаётся обходу; <<все рациональные>> при этом суть потенциальный обход, не готовая совокупность.

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

Компонент	Что фиксирует	E/R/R
дерево: корень + `cw_left`/`cw_right`	конституция обхода	Rule
навигация $\leftrightarrow$ номер; обратимость	биекция `nat` $\leftrightarrow$ `QPos`	Rule
несократимость (`enum_coprime`)	каждое значение однажды	Rule
номер обхода (`index_of_QPos`)	роль рационального	Role
узлы-пары / несократимые представители	носители (конечны, $P 4$ )	Element
законы $L 1$ – $L 5$ (здесь $L 5$ )	универсальный слой	Rule (универс.)

{ Хорошая сформированность. Обход сформирован верно: он биективен (прямой и обратный обращают друг друга, доказано) и каноничен по несократимости — ни одно значение не сосчитано дважды (нет $2/4$ рядом с $1/2$ ). И здесь разбор оборачивается диагностикой, двоякой. Первое: счётность ToS читает как правило-обход — процедуру, которую можно вычислить, проследить и обратить, — а не как голое существование соответствия; операциональная форма строго сильнее (§ 3.1). Второе, и главное для дальнейшего: нельзя смешивать данные и поведение. Рациональное — конечные данные (пара, элемент), и потому перечислимо; процесс приближения — бесконечное поведение (функция $N \to Q$ ), и к совокупности конечных программ он не сводится (§ 3.7). Считать процессы так же, как точки, — смешение категорий: элемент-данные и роль-поведение суть разные уровни.}

Что даёт разбор. Счётность предстаёт не свойством готового множества, а правилом: обход, дающий каждому рациональному конечный номер. Этим замыкается арка чисел-позиций Части III — натуральные, целые, рациональные — все суть конечные данные, уложимые в обход. И тем же разбор ставит порог Части IV: данные перечислимы, поведение — открытый вопрос. Процессы приближения, не завершающиеся рациональной позицией (§ 3.8.4), и есть то поведение; перечислимы ли они — разберёт Часть IV (несчётность процессов).

Чего рациональным числам недостаёт

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

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

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

Переход к следующей главе

Рациональные числа построены, показаны как поле в стандартной алгебраической оболочке и показаны перечислимыми. Следующая глава вглядится в их аномалии — в те процессы приближения, которые рациональные числа описывают всё точнее, но которые ни на какой рациональной позиции не завершаются. Аномалиям рациональных чисел посвящена Глава III.4.

Часть: Часть III. От натуральных к рациональным · Том: «Математика»

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

Навигация: ← Глава 2. Рациональные числа · Глава 4. От позиции к процессу →

Здесь и далее формальные конструкции этой главы — тип пар, дерево, функции обхода, теоремы — приводятся по файлу Countability_Q.v Rocq-репозитория ToS. Имена файлов репозитория даются для справки. ↩
Сохранение несократимости доказано в файле Countability_Q.v: леммы о левом и правом ребёнке (наибольший общий делитель сохраняется при каждом из двух правил) и теорема cw_node_coprime — что во всяком узле дерева числитель и знаменатель взаимно просты. ↩
Функция cw_node и перечисление enum_QPos определены в файле Countability_Q.v Rocq-репозитория ToS. ↩
Функции path_to_node и index_of_QPos, а также теоремы этого раздела определены и доказаны в файле Countability_Q.v Rocq-репозитория ToS. Первый аргумент fuel — технический приём Rocq: он несёт заведомо достаточное число шагов, чтобы рекурсия была явно конечной. fuel не означает, что процедура требует внешнего, непроверенного ограничения: это стандартный способ сделать рекурсию структурной для проверяющей системы Rocq, и затем доказывается теоремой, что выбранного топлива всегда достаточно — что результат не зависит от того, сколько лишних шагов отпущено сверх нужного. ↩
Теоремы о круговом обходе — path_cw_node_roundtrip и cw_node_path_roundtrip — доказаны в файле Countability_Q.v. ↩
Этот контраст уже намечен в комментариях к файлу Countability_Q.v: рациональные точки перечислимы как конечные объекты — пары числителя и знаменателя, — тогда как рациональные процессы (последовательности приближений) имеют иной статус и требуют отдельного разбора. Файл прямо отмечает, что совокупность функций $N \to Q$ так не перечисляется. ↩

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

Проводник