Глава 3. Иерархический путь: число как уровень

Второй путь

Один ряд, несколько путей

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

Можно было бы счесть, что на этом дело сделано: ряд $1,2,3,\dots$ получен, его устройство выяснено. Но ToS приходит к натуральному ряду не единожды. Уже Глава II.1 (§ 1.1) указала: путей к $N$ четыре, и кардинальный — лишь первый. Настоящая глава открывает второй.

Зачем второй путь, если ряд уже построен? Затем, что тот же ряд, полученный из иной деривации, обнаруживает в натуральном ряде не случайную, а структурную неизбежность. Если бы $N$ возникал в ToS лишь одним способом, можно было бы заподозрить, что он есть артефакт этого одного способа — особенность кардинального счёта, и только. Но когда к одному ряду ведут несколько независимых деривационных дорог, ряд оказывается не следствием частного приёма, а тем, к чему ToS вынуждена приходить с разных сторон. Множественность путей — не избыточность, а свидетельство.

Чем второй путь отличается от первого

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

Кардинальный путь (Глава II.2) исходит из повторимости акта. Его исходная точка — акт различения, который можно совершить, а совершив — совершить ещё раз. Число там есть отпечаток совершённых повторений, собранных в список; натуральный ряд порождается тем, что к списку различий можно присоединить ещё одно различие.

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

Различие исходных точек существенно. Кардинальный путь ничего не говорит об уровнях; иерархический ничего не говорит о списках. Это разные деривации — они не опираются друг на друга и не выводятся одна из другой. И именно потому совпадение их итога — то, что обе приходят к ряду $1,2,3,\dots$, — значимо: это не одно рассуждение, дважды пересказанное, а две дороги, независимо сошедшиеся.

Что предстоит главе

Глава пройдёт иерархический путь шаг за шагом. Сначала будет установлено, на что путь опирается, — закон $L5$ и порождаемая им иерархия уровней (§ 3.2). Затем — что иерархия имеет основание, что она конечна снизу, и почему отсюда ряд уровней начинается, и начинается с единицы (§ 3.3). Далее — ядро пути: уровень есть число, ибо устройство уровней в точности воспроизводит устройство натурального ряда (§ 3.4). Затем — что восхождение по уровням порождает ряд неограниченно вверх (§ 3.5). После этого иерархический путь будет сопоставлен с кардинальным: два пути, один ряд (§ 3.6). Будет показано, что индукция и здесь не аксиома, а вырастает из устройства иерархии (§ 3.7). И глава завершится переходом к третьему пути (§ 3.8).

Иерархический путь — второй из путей ToS к натуральному ряду. Он исходит не из повторимости акта, как кардинальный, а из закона порядка $L5$ и порождаемой им иерархии уровней. Число на этом пути есть уровень иерархии; натуральный ряд — ряд уровней. Совпадение итога двух независимых путей показывает, что $N$ есть структурная неизбежность, а не артефакт одного приёма.

Закон $L5${L5} и иерархия уровней

На что опирается путь

Иерархический путь исходит из закона $L5$ и порождаемой им иерархии уровней. И то и другое уже введено в Части I: $L5$ — в Главе I.3, иерархия уровней — в Главе I.4. Настоящий раздел не переоткрывает их, а кратко собирает то, на что путь будет опираться, со ссылкой на места, где это установлено.

Закон $L5${L5}: условие возможности иерархии

Приведём $L5$ в его собственной формулировке из Главы I.3, не подменяя её пересказом. Законы $L1$–$L4$ касаются структуры одного акта различения — тождества его сторон, исключительности, исчерпанности, обоснованности. $L5$ — Закон Порядка — отличается от них уровнем своего действия: он делает возможной саму структуру отношений между актами различения — их последовательность, их упорядочение, их иерархию. Онтологически $L5$ есть структурное условие самой возможности иерархии: всякое определённое существование развёртывается на определённых уровнях, и эти уровни стоят в отношении порядка — один уровень предшествует другому.

Глава I.3 различила в действии $L5$ две стороны. Горизонтально $L5$ проявляется в упорядоченности элементов на одном уровне — в том, что они стоят в порядке относительно друг друга. Вертикально — в иерархии уровней: элементы системы уровня $n+1$ суть сами системы уровня $n$. Кардинальный путь (Глава II.2) опирался на горизонтальную сторону $L5$ — на порядок актов в списке. Иерархический путь опирается на вертикальную — на иерархию уровней. Один закон, две стороны; два пути берут разные.

Иерархия уровней

Что такое иерархия уровней, установила Глава I.4 (§ 4.7). Системы разной сложности не располагаются вперемешку, как равные. Они образуют иерархию, в которой более сложная система имеет своими элементами системы более фундаментальные: элементы системы уровня $n+1$ находятся на более фундаментальных уровнях. В ближайшем и наиболее наглядном случае это системы уровня $n$ — ровно на одну ступень ниже; но формальная идея шире: требуется лишь отношение «ниже по уровню», не обязательно ровно один шаг вниз. Это — вертикальное устройство, задаваемое $L5$.

Иерархия не есть дополнительный постулат. Глава I.4 вывела её из уже установленного — из совместной работы $L5$ и принципа $P1$: $L5$ располагает организатор выше организуемого, $P1$ требует, чтобы уровень организуемого был строго ниже уровня организатора. Применяя это: элементы данной системы сами организованы, то есть сами суть системы — но уровнем ниже. Иерархия уровней есть структурное следствие $L5$ и $P1$, не отдельное допущение.

У этого устройства есть черта, которую стоит отметить заранее, ибо она понадобится дальше. Иерархия уровней не есть одна зафиксированная лестница. $L5$ задаёт форму иерархичности — отношение «уровнем ниже / уровнем выше», — и эта форма прилагается рекурсивно, на разных масштабах. Есть внешняя иерархия — иерархия больших областей: основание её — Логика, над ней — математика, над математикой — области более производные. И есть внутренние иерархии — иерархии уровней внутри отдельной области: внутри математики, например, основанием служат натуральные числа, над ними — системы из чисел, над теми — системы из таких систем. Внешняя и внутренние иерархии — не разные устройства, а одно и то же устройство уровней, приложенное на разных масштабах. Что у всякой иерархии — какого бы масштаба она ни была — одна и та же форма, существенно для иерархического пути: именно эту форму, а не какую-либо частную иерархию, путь и возьмёт за основу.

Здесь нужна оговорка, чтобы дальнейшее не было прочитано неверно. Следует различать глобальный тип уровней, в котором базовый уровень — L1 — есть Логика, основание всего, и доменно-относительные иерархии, в которых тем или иным объектом играется роль локального основания. Когда мы говорим, что внутри математики основанием служат натуральные числа, речь идёт не о переименовании глобального L1: натуральные числа не «становятся Логикой». Речь о применении той же формы иерархии внутри отдельной области — о локальной лестнице со своим основанием, которое в глобальной иерархии само занимает некоторый уровень выше L1. Иерархический путь берёт за основу именно форму иерархии, безразличную к масштабу; какой именно объект служит основанием — глобальная Логика или локальные числа — зависит от того, какая иерархия рассматривается.

Тип уровней и отношение порядка

Поскольку $L5$ производит саму иерархию — делает её возможной как структуру, — формализация $L5$ требует отдельной структуры, в которой можно говорить об уровнях и отношениях между ними. ToS вводит такую структуру — тип уровней, Level.

Level представляет уровни иерархии: есть уровень $L_1$, есть уровни над ним. На уровнях определён оператор строгого порядка — записываемый $\ll$, — и запись $l_1\ll l_2$ читается так: $l_1$ ближе к основанию, чем $l_2$, то есть $l_1$ фундаментальнее, $l_2$ производнее. Семантика этого порядка задана $L5$: он есть тот самый порядок уровней, который $L5$ делает возможным.

У оператора $\ll$ есть свойства, доказанные в ToS как теоремы и формализующие $L5$. Он иррефлексивен: ни один уровень не ближе к основанию, чем он сам, — формально $\neg (l\ll l)$. Это прямое выражение принципа $P1$: ничто не предшествует самому себе, иначе иерархия теряла бы смысл. Он транзитивен: если $l_1$ ближе к основанию, чем $l_2$, а $l_2$ — чем $l_3$, то $l_1$ ближе к основанию, чем $l_3$. Иррефлексивность и транзитивность вместе и делают $\ll$ отношением строгого порядка — тем, что превращает набор уровней в иерархию.

Закон $L5$ — условие самой возможности иерархии: уровни существования стоят в отношении порядка. Вертикальная сторона $L5$ — иерархия уровней, в которой элементы системы уровня $n+1$ находятся на более фундаментальных уровнях (в ближайшем случае — уровня $n$); она есть следствие $L5$ и $P1$, не отдельный постулат. Формализуется $L5$ типом уровней Level с оператором строгого порядка $\ll$ («ближе к основанию»), иррефлексивным и транзитивным. На эту вертикальную структуру и опирается иерархический путь.

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

Иерархия конечна снизу

Зачем иерархии начало

Иерархия уровней задана (§ 3.2): уровни стоят в отношении строгого порядка $\ll$, одни ближе к основанию, другие дальше. Но для пути к натуральному ряду этого ещё не довольно. Натуральный ряд имеет начало — единицу (Глава II.1). Если иерархический путь приведёт к ряду уровней, то ряд уровней тоже должен иметь начало — базовый уровень, ниже которого нет ничего.

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

Базовый уровень

У всякой иерархии уровней есть наименьший уровень — основание, ниже которого уровней нет. ToS называет его базовым уровнем.

Здесь важно не сузить понятие основания. «Основание» — понятие относительное: основание есть низ данной иерархии, то, ниже чего в ней уровней нет. Чем именно занят базовый уровень, зависит от того, какая иерархия рассматривается. У внешней иерархии больших областей (§ 3.2.3) основание — Логика: тот слой, на котором работают сами законы $L1$–$L5$ как условия всякой определённости; Логика не есть одна из систем внутри иерархии — она есть то, при чём всякая система вообще возможна, и потому она в основании. У внутренней иерархии математики основание — иное: натуральные числа, ниже которых в этой иерархии систем нет. Основание у иерархий разное; общее у них — то, что основание есть.

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

В типе уровней Level базовый уровень есть отдельный, первичный элемент — L1. Все прочие уровни получаются из него надстраиванием; сам он не получается ни из чего — он не надстроен над чем-то ещё, он есть то, с чего надстраивание начинается.

Конечность снизу есть устройство, не постулат

Что иерархия конечна снизу — следствие устройства типа уровней.

Тип Level устроен так. В нём есть базовый уровень L1 — и есть единственный способ получить новый уровень: надстроить его над уже имеющимся. Операцию надстраивания ToS обозначает LS (следующий уровень): из уровня $l$ она даёт уровень LS $l$, стоящий на одну ступень дальше от основания. Других способов получить уровень нет: всякий уровень либо есть базовый L1, либо надстроен операцией LS над каким-то уровнем.

Отсюда конечность снизу следует сама. Возьмём любой конкретный уровень и станем спускаться — переходить от уровня к тому, над которым он надстроен. Каждый шаг вниз снимает одно надстраивание LS. Но надстраиваний, которыми получен данный уровень, конечное число — уровень получен из L1 конечным числом применений LS, иначе он не был бы уровнем типа Level. Значит, спуск от данного уровня за конечное число шагов упирается в L1 — и дальше идти нельзя: L1 не надстроен ни над чем, снимать больше нечего. Для каждого конкретного уровня спуск вниз конечен: он снимает конечное число надстраиваний и упирается в основание.

Стоит сразу оговорить точную границу этого утверждения. Сказанное относится к спуску от любого конкретного уровня: такой спуск конечен, потому что конечно число надстраиваний, которыми уровень получен. Это не то же, что утверждать общую теорему о несуществовании какой бы то ни было бесконечно убывающей последовательности уровней — теоремы вида «не существует функции $f:‘nat‘\to ‘Level‘$ с $f(n+1)\ll f(n)$ для всех $n$». Такая теорема в иерархическом пути не используется и в процитированных файлах не доказана; для неё понадобилась бы отдельная формализация (опирающаяся на убывание level_depth вдоль $\ll$, см. ниже).¹ Главе достаточно более слабого и прямо обоснованного утверждения: для каждого предъявленного уровня спуск конечен и упирается в основание.

Это видно и со стороны оператора $\ll$. Запись $l\ll ‘L1‘$ — «$l$ ближе к основанию, чем базовый уровень» — ложна для любого $l$: ничто не ближе к основанию, чем само основание. Под L1 оператор порядка не указывает ни на что — не потому, что там «пустой уровень», а потому, что там нет уровня. Спуск по $\ll$ обрывается на L1, ибо ниже L1 оператору порядка нечего сопоставить. Формально это поддержано доказанными в TheoryOfSystems_Core_ERR.v свойствами оператора $\ll$: леммой level_lt_depth (порядок строго убывает по глубине) и леммой level_lt_irrefl (ни один уровень не ниже самого себя). Прямую минимальность основания и открытость иерархии вверх удобно было бы выразить ещё двумя короткими леммами — $\neg (l\ll ‘L1‘)$ для всякого $l$ (ниже основания уровней нет) и $l\ll ‘LS‘l$ (над всяким уровнем есть следующий); обе тривиально доказуемы из определения $\ll$, и их добавление в основной файл сделало бы опору главы на код прямой.²

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

Почему у иерархии нет «отрицательного низа»

Иерархия конечна снизу — но не значит ли это, что она просто «упирается» в базовый уровень, тогда как мысль вправе спросить: а что под основанием? Не следовало бы ли продолжить иерархию вниз — к «уровню ниже основания», к чему-то ещё более исходному?

Этот вопрос не имеет предмета, и ToS объясняет, почему, — мотивом $M_1$, позитивной онтологией (Глава I.7). По $M_1$ всё онтологически существующее существует позитивно: нет «отрицательных объектов», небытие не есть особый род бытия. Уровень есть нечто положенное — он существует позитивно или не существует вовсе. «Уровень ниже основания» был бы уровнем, который не надстроен ни над чем и сам не есть основание, — то есть не положен ничем и не положен как исходное. Такого уровня нет не потому, что ToS его исключает особым запретом, а потому, что полагать там нечего: ниже базового уровня данной иерархии нет того, из чего ещё один уровень мог бы быть положен. «Под основанием» не пусто — там попросту нет места для уровня.

Иными словами: конечность снизу не есть остановка перед чем-то непройденным. Это не граница, за которой что-то скрыто. Базовый уровень есть низ иерархии в полном смысле — не «самый нижний из пройденных», а тот, ниже которого нет уровней.

Почему ряд начинается — и начинается с единицы

Теперь можно сказать, что конечность снизу даёт пути к натуральному ряду.

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

Она даёт, во-вторых, начало именно с единицы, а не с нуля. Здесь иерархический путь сходится с тем, что Глава II.1 установила для кардинального. ToS сопоставляет уровню его глубину — расстояние от основания, считаемое по ступеням. Глубина базового уровня L1 есть единица: основание не «нулевой уровень», а первый — оно само есть уровень, наличный и положенный, а не отсутствие уровня. Перекличка с Главой II.1 здесь точная: как первый совершённый акт различения есть единица, а не нуль (§ 1.2), так и первый уровень иерархии — основание — есть единица, а не нуль. Нуль в иерархии отметил бы отсутствие уровня; но основание есть уровень наличный, и потому ему отвечает единица.

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

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

Уровень как число: LS{LS} есть S{S}

Что осталось показать

Иерархия уровней имеет основание (§ 3.3) и наращивается надстраиванием. Этого довольно, чтобы сделать главный шаг иерархического пути: показать, что ряд уровней есть натуральный ряд — что уровень есть число.

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

Как устроен натуральный ряд

Сначала — кратко о том, как устроен натуральный ряд. Кардинальный путь (Глава II.2) показал это содержательно: ряд начинается с единицы и наращивается переходом к следующему числу. У этого устройства — ровно две составляющие. Первая: есть начальное число — единица. Вторая: есть операция следования — переход от числа к следующему за ним; ToS обозначает её S (от лат. successor, следующий). Всякое натуральное число либо есть единица, либо получается из какого-то числа применением S. Других чисел нет, и другого способа их получить нет.

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

Как устроена иерархия уровней

Теперь — как устроена иерархия уровней; § 3.3 это уже показал, здесь нужно лишь поставить рядом. У иерархии — ровно две составляющие. Первая: есть базовый уровень — основание, L1. Вторая: есть операция надстраивания — переход от уровня к следующему, стоящему на ступень дальше от основания; ToS обозначает её LS (следующий уровень, level successor). Всякий уровень либо есть базовый L1, либо получается из какого-то уровня применением LS. Других уровней нет, и другого способа их получить нет.

Поставим два устройства рядом. Натуральный ряд: начальный элемент 1, операция следования S. Иерархия уровней: начальный элемент L1, операция надстраивания LS. Это одно и то же устройство. Начальному числу отвечает базовый уровень; операции следования отвечает операция надстраивания. И там и тут: один первичный элемент плюс одна операция, порождающая из каждого элемента следующий, и всё порождается из первичного элемента её повторением.

LS{LS} есть S{S}

Совпадение устройств не случайно и не приблизительно. Тип уровней Level ToS вводит как индуктивный тип — тип, всякий объект которого либо есть базовый элемент, либо получен применением единственной операции к уже построенному объекту того же типа. Формально Level записывается так:³

Inductive Level : Set :=
  | L1 : Level
  | LS : Level -> Level.

Первая строка: L1 есть уровень — базовый, ни из чего не полученный. Вторая: LS есть операция, которая из всякого уровня даёт уровень — следующий за ним. И это всё: тип Level исчерпывается базовым уровнем и надстраиванием.

Но ровно так же — индуктивным типом с базовым элементом и одной операцией следования — устроен и тип натуральных чисел. Здесь нужна точность. Строго говоря, Level и тип nat — это не один и тот же тип в Rocq: это два разных индуктивных объявления, и LS не есть буквально тот же конструктор, что S, — они действуют на разных типах. Но оба типа имеют одну и ту же индуктивную форму: базовый элемент и один конструктор следования. Поэтому они структурно изоморфны — и через изоморфизм Level с nat конструктор LS переходит ровно в S. В этом, и только в этом, смысле LS есть S: не тождество двух Coq-объектов, а одна операция следования, взятая на двух изоморфных типах. Заголовок «LS есть S» нужно читать так: LS — это S, перенесённая на тип уровней через изоморфизм.

Отсюда — итог иерархического пути. Раз Level и тип натуральных чисел имеют одну и ту же индуктивную форму — базовый элемент плюс операция следования, — они структурно изоморфны: не один тип в Rocq, а две реализации одной индуктивной схемы. Ряд уровней $‘L1‘,‘LS‘‘L1‘,‘LS‘(‘LS‘‘L1‘),\dots$ и натуральный ряд $1,2,3,\dots$ — не два независимых ряда и не буквально один Coq-тип, а одна индуктивная схема в двух представлениях. В этом смысле натуральное число $n$ есть уровень: уровень, отстоящий от основания на $n-1$ надстраиваний.

Тип уровней Level и тип натуральных чисел — не один и тот же тип в Rocq, а два индуктивных типа одной формы: базовый элемент плюс операция следования. Они структурно изоморфны. LS (надстраивание уровня) переходит при изоморфизме ровно в S (следование числа); в этом смысле LS есть S, взятая на типе уровней. Ряд уровней и натуральный ряд суть две реализации одной индуктивной схемы; число есть уровень иерархии.

Глубина уровня как мост к числу

Тождество устройств можно предъявить и явно — сопоставлением, которое ToS вводит особо. Это функция глубины уровня.

Глубина уровня — это число надстраиваний, отделяющих его от основания, считая основание за первый уровень. ToS определяет её так: глубина базового уровня L1 есть единица; глубина уровня LS $l$ есть глубина $l$, увеличенная на единицу. Формально:

Fixpoint level_depth (l : Level) : nat :=
  match l with
  | L1    => 1
  | LS l' => S (level_depth l')
  end.

Функция глубины каждому уровню сопоставляет натуральное число и тем самым служит мостом между типом уровней и натуральным рядом. Это сопоставление — роль уровня в разборе E/R/R (§ 3.8.2): глубина и есть число уровня. Существенны две её черты. Первая: глубина базового уровня есть единица, не нуль, — основание есть уровень наличный, и ему отвечает первое число, а не отметка отсутствия (§ 3.3.5). Вторая: каждое надстраивание LS увеличивает глубину ровно на единицу — шаг по иерархии в точности отвечает шагу по натуральному ряду. Вторая черта фиксируется простой леммой:

Lemma level_depth_LS : forall l,
  level_depth (LS l) = S (level_depth l).
Proof. reflexivity. Qed.

Лемма почти тривиальна — доказывается одним reflexivity, — но содержательна: она показывает, что LS на уровнях и S на числах согласованы через level_depth поэлементно.

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

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

Два слоя нумерации уровней. { В репозитории есть две функции, сопоставляющие уровню число, и они дают разные результаты для основания. В основном файле TheoryOfSystems_Core_ERR.v функция level_depth (листинг выше) сопоставляет базовому уровню L1 глубину единицу: level_depth L1 = 1. В отдельном файле L5_NatFromHierarchy.v функция level_to_nat сопоставляет базовому уровню нуль: там level_to_nat LBase = 0. Это не противоречие, а два разных сопоставления, и различать их необходимо:}

Уровень	level_depth (Core)	level_to_nat (отд. файл)
L1 / LBase	1	0
LS L1 / LSucc LBase	2	1
LS (LS L1) / LSucc (LSucc LBase)	3	2

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

Изоморфизм standalone-типа. Файл L5_NatFromHierarchy.v⁴ доказывает изоморфизм типа уровней со стандартным nat, и доказывает его строго. Но технически этот файл использует собственную копию типа уровней: он объявляет Inductive Level := LBase | LSucc и не импортирует основной файл. Поэтому его теоремы следует читать как формализацию той же по форме структуры, а не буквально как теоремы о Core-типе Level из TheoryOfSystems_Core_ERR.v (где конструкторы названы L1 и LS). Два типа изоморфны по форме — база и один конструктор следования, — но это два разных Coq-объявления. Для полной синхронизации репозитория соответствующие леммы желательно перенести на основной тип Level или сделать файл импортирующим Core-определение; до этого изоморфизм доказан для standalone-копии структуры уровней.

Что отсюда следует. С этими оговорками формальная сторона ясна. Доказано: индуктивная структура «база плюс один конструктор следования» изоморфна стандартному nat; шаг LSucc переходит при изоморфизме ровно в S. Натуральные числа на иерархическом пути не вводятся допущением — структура всякой иерархии уровней уже есть структура натурального ряда, и это обнаруживается, а не постулируется. Тезис же о том, что глубина читается с единицы, есть онтологическое чтение (левый столбец таблицы), согласованное с level_depth основного файла.

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

Восхождение как порождение ряда

От тождества устройств к движению

Предыдущий раздел установил тождество устройств: тип уровней и тип натуральных чисел структурно изоморфны — две реализации одной индуктивной схемы (§ 3.4). Установлено это было, так сказать, в покое — предъявлением двух типов и сличением их составляющих. Теперь тот же итог нужно пройти в движении: увидеть, как ряд уровней не просто изоморфен натуральному ряду, а порождается — и порождается восхождением по иерархии.

Иерархический путь к этому и шёл. Кардинальный путь порождал натуральный ряд присоединением различия к списку (Глава II.2); иерархический порождает его восхождением — надстраиванием уровня над уровнем. Настоящий раздел проходит это порождение.

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

Восхождение по иерархии есть применение операции LS: от уровня $l$ к уровню LS $l$, стоящему на ступень дальше от основания. Один шаг восхождения — одно надстраивание.

Что этот шаг даёт в числах, показывает функция глубины (§ 3.4.5). Глубина уровня LS $l$ есть глубина $l$, увеличенная на единицу. Значит, один шаг восхождения — одно применение LS — увеличивает глубину ровно на единицу. Восхождение на ступень есть в точности прибавление единицы к числу.

Здесь иерархический путь сходится с кардинальным, и сходится в существенной точке. Кардинальный путь показал (Глава II.2, § 2.5.2): присоединить к списку ещё одно различие значит увеличить счёт на единицу — операция следования есть присоединение различия. Иерархический путь показывает то же о другой операции: надстроить над уровнем ещё один уровень значит увеличить глубину на единицу — операция следования есть надстраивание. Одна и та же операция следования предстаёт на двух путях двумя своими сторонами: как прибавление различия и как надстраивание уровня. S кардинального пути и LS иерархического — это S, увиденная дважды.

Восхождение не ограничено

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

Это ToS устанавливает прямо из устройства типа Level. Операция LS определена на всяком уровне: каков бы ни был уровень $l$, выражение LS $l$ есть уровень — следующий за $l$. Нет уровня, на котором LS была бы неприменима; нет, стало быть, и высшего уровня, за которым надстраивать было бы нечего. Над всяким уровнем есть следующий, ибо над всяким уровнем LS даёт уровень. Формально это удобно выразить двумя короткими леммами — что у всякого уровня есть надстроенный над ним уровень и что всякий уровень ниже своего надстроенного:

Lemma level_has_successor :
  forall l : Level, exists l', l' = LS l.
Proof. intro l. exists (LS l). reflexivity. Qed.
 
Lemma every_level_below_its_successor :
  forall l : Level, l << LS l.
Proof. intro l. simpl. left. reflexivity. Qed.

Первая лемма говорит, что надстроенный уровень всегда существует; вторая — что он действительно стоит выше (исходный уровень ближе к основанию, чем его надстроенный). Обе доказываются немедленно из определений LS и $\ll$. Вместе они и означают: восхождение не упирается ни в какой высший уровень.⁵

Иерархия, конечная снизу (§ 3.3), не ограничена сверху. И это не два независимых свойства, а две стороны одного устройства типа Level: базовый уровень L1 даёт иерархии низ; всюду определённая операция LS даёт ей неограниченное восхождение. Низ и открытость вверх — то же, что у натурального ряда: единица в начале, и нет последнего числа.

Восхождение порождает ряд

Теперь порождение ряда видно вполне. Начинаем с основания — с базового уровня L1, которому отвечает единица. Применяем LS — восходим на ступень; глубина становится двойкой. Применяем LS ещё раз — глубина становится тройкой. Каждый шаг восхождения прибавляет единицу; каждый достигнутый уровень есть очередное натуральное число. Восхождение, начатое от основания и неограниченно продолжаемое, порождает весь натуральный ряд:

$$‘L1‘\stackrel{‘LS‘}{\to }‘LS‘‘L1‘\stackrel{‘LS‘}{\to }‘LS‘(‘LS‘‘L1‘)\stackrel{‘LS‘}{\to }\cdots$$ $$1\stackrel{+1}{\to }2\stackrel{+1}{\to }3\stackrel{+1}{\to }\cdots$$

Две строки — одно движение. Восхождение по уровням и счёт по натуральному ряду суть одно и то же порождение, записанное в двух обозначениях.

Восхождение по иерархии порождает натуральный ряд: начатое от основания (которому отвечает единица) и продолжаемое применением LS (каждое прибавляет к глубине единицу), оно даёт уровень за уровнем — число за числом. Иерархия конечна снизу и не ограничена сверху; этим она и есть натуральный ряд: с началом и без конца.

Бесконечность ряда уровней

О бесконечности ряда уровней нужно сказать то же, что Глава II.2 сказала о бесконечности натурального ряда, — и по тому же основанию.

Восхождение неограниченно: над всяким уровнем есть следующий. Но неограниченность восхождения не есть наличие завершённой совокупности всех уровней. По принципу $P4$ — принципу конечной актуальности (Глава II.2, § 2.7) — актуально на всякой стадии конечное; ряд уровней бесконечен потенциально — как неограниченная продолжаемость восхождения, а не как готовая совокупность всех уровней сразу. Нет высшего уровня — но нет и уровня-совокупности, который стоял бы над всеми и содержал бы их все разом.

Здесь нужна точность, иначе утверждение можно прочесть сильнее, чем оно есть. ToS не отрицает, что об уровнях можно говорить как о целом в метаязыке: формально тип Level существует — это индуктивный тип Rocq (Level : Set), и о всех уровнях этой схемы в метаязыке говорить можно. Отрицается другое: внутри самой иерархии нет уровня, который содержал бы все уровни как свои элементы. Различение здесь — между тремя вещами: тип Level как индуктивный тип языка (он есть); уровень-система, которая имела бы все уровни своими элементами (его нет — он нарушил бы $P1$, ибо содержал бы и себя); и завершённая актуальность всех уровней на одной стадии (её нет по $P4$). ToS запрещает не метаязыковое описание типа Level, а превращение открытой иерархии в завершённый объект на одном из её собственных уровней. Метаязыковая речь о типе и внутрииерархическая завершённость — разные вещи; ToS отрицает вторую, не первую.

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

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

Сравнение с кардинальным путём

Чем пути различны

Два пути к натуральному ряду пройдены порознь — кардинальный в Главе II.2, иерархический в § 3.1–3.5. Настоящий раздел ставит их рядом. Сопоставление здесь не есть выбор лучшего и не есть проверка одного пути другим: оба доведены до конца, оба состоятельны. Поставить их рядом нужно, чтобы увидеть, что именно совпало и что это совпадение значит. Начать же следует с того, чем пути различны.

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

Кардинальный путь исходит из повторимости акта различения. Число на нём есть длина списка совершённых различий; порождающая операция — присоединение к списку ещё одного различия. Опорная сторона закона $L5$ — горизонтальная: порядок актов в списке.

Иерархический путь исходит из вертикального устройства, задаваемого $L5$. Число на нём есть уровень иерархии; порождающая операция — надстраивание над уровнем ещё одного уровня, восхождение. Опорная сторона $L5$ — вертикальная: иерархия уровней.

Различие не поверхностное. Пути независимы как деривационные схемы: один исходит из списка повторённых актов и не пользуется понятием уровня, другой исходит из иерархии уровней и не пользуется понятием списка; один наращивает ряд вширь, прикладывая различия, другой — ввысь, надстраивая уровни. Это две разные деривации, и ни одна не выводится из другой. Но независимость их — независимость схем построения, не независимость от общей рамки ToS: оба пути работают внутри одних и тех же законов $L1$–$L5$ и принципа $P4$, оба опираются на первичность единицы (Глава II.1) и на потенциальное понимание бесконечности. Более того, оба коренятся в одном законе $L5$ — но в разных его сторонах: кардинальный путь опирается на горизонтальную сторону $L5$ (порядок актов в списке), иерархический — на вертикальную (иерархию уровней). Пути независимы по деривации и едины по рамке; именно это делает их совпадение значимым.

В чём пути совпали

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

Кардинальный путь дал ряд с началом — единицей — и операцией следования S: присоединением различия. Иерархический дал ряд с началом — базовым уровнем, которому отвечает единица, — и операцией следования LS: надстраиванием уровня. Но S и LS — это, как показал § 3.4, одна и та же операция следования, взятая на двух типах; и единица кардинального пути и единица иерархического — одно и то же первое число. Оба пути дали натуральный ряд — не два похожих ряда, а один: с одной и той же единицей в начале, с одной и той же операцией следования, с одной и той же потенциальной бесконечностью по $P4$.

Пути расходятся в исходной точке и в порождающей операции — и сходятся в результате полностью. Разные деривации привели к тождественному ряду.

Различие и совпадение двух путей удобно свести в таблицу:

Путь	Основа	Операция	Число
кардинальный (Гл. II.2)	список совершённых различий	присоединить ещё одно различие	длина списка
иерархический (эта глава)	иерархия уровней	надстроить ещё один уровень	глубина уровня

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

Почему два пути не дают двух измерений

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

Мысль такая. Два пути независимы; кардинальный наращивает ряд вширь, иерархический — ввысь. Не задают ли они тем самым две оси — горизонтальную и вертикальную, — а две оси задают плоскость? Не возникает ли из двух путей к числу геометрия — плоскость, чьи точки суть пары «число по одной оси, число по другой»?

Мысль не проходит, и видеть, почему, важно. Две оси задают плоскость лишь тогда, когда они независимы в результате — когда точка $(3,5)$ отлична от точки $(5,3)$, когда число по одной оси и число по другой могут разниться. Но кардинальный и иерархический пути не таковы. Они независимы деривацией, но не результатом: они дают не два разных ряда, а один и тот же ряд — это и установил § 3.6.2. Их «независимость» — независимость дорог, не независимость итогов.

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

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

То, как из чисел возникают новые измерения — как строятся структуры богаче натурального ряда, — предмет дальнейших частей труда, и строиться они будут выведенно, своей деривацией, а не извлекаться из наличия двух путей. Здесь же существенно обратное: что два независимых пути дали одно. В терминах E/R/R путь — это роль-режим доступа к ряду, не отдельный объект-ряд (разбор § 3.8.2).

Что значит совпадение путей

Совпадение двух независимых путей и есть то, ради чего стоило пройти второй путь.

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

Это — довод о структурной неизбежности натурального ряда. Не «ToS умеет построить $N$» (это показал бы и один путь), а «$N$ есть то, к чему деривация ToS вынуждена приходить, какой стороной к нему ни подступай». Совпадение независимых путей свидетельствует о предмете: о том, что натуральный ряд не изобретён, а обнаружен.

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

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

Индукция по уровням

Отложенный вопрос

В § 3.4 было замечено, что доказательство тождества Level и натурального ряда опирается на индуктивное устройство типа уровней — и что к индукции придётся вернуться. Возвращаемся.

Глава II.2 показала на кардинальном пути, что индукция в ToS не аксиома: база отвечает первому акту различения, шаг — повторимости акта, и принцип индукции есть словесная запись того, как строится ряд (§ 2.6). Иерархический путь приходит к ряду иначе — не через повторимость акта, а через восхождение по уровням. Значит, и индукцию здесь нужно обосновать заново: показать, что и на иерархическом пути она вырастает из устройства, а не вводится постулатом.

Индукция по уровням

Принцип индукции для натурального ряда был приведён в Главе II.2 (§ 2.6.2): чтобы свойство было верно для всякого числа, довольно, чтобы оно было верно для первого числа (база) и чтобы из его верности для $n$ следовала верность для $n+1$ (шаг).

Раз ряд уровней есть натуральный ряд (§ 3.4), тот же принцип читается и по уровням. Индукция по уровням: чтобы свойство было верно для всякого уровня иерархии, довольно двух вещей — чтобы оно было верно для базового уровня (база), и чтобы из его верности для уровня $l$ следовала верность для надстроенного уровня LS $l$ (шаг). База и шаг вместе влекут: свойство верно для всякого уровня.

База есть основание, шаг есть надстраивание

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

Иерархия сложена из двух вещей, и других у неё нет (§ 3.3, § 3.4). Первая: есть базовый уровень — основание. Вторая: всякий неосновной уровень надстроен над другим операцией LS. Сопоставим это с индукцией. База индукции — свойство верно для базового уровня; первая составляющая иерархии — есть базовый уровень. Шаг индукции — из верности для $l$ следует верность для LS $l$; вторая составляющая — всякий уровень надстроен операцией LS. База индукции отвечает основанию; шаг индукции отвечает надстраиванию.

Отсюда и правомерность. Всякий уровень иерархии либо есть основание, либо надстроен над другим уровнем конечным числом применений LS (§ 3.3.3). Свойство, верное для основания (база) и сохраняемое надстраиванием (шаг), верно тогда вдоль всякой конечной цепочки надстраиваний — то есть для всякого уровня. Индукция по уровням властна над всей иерархией не по особому могуществу принципа, а потому, что иерархия вся и состоит из основания и надстраиваний над ним.

Индукция по уровням не есть аксиома. База индукции отвечает основанию иерархии, шаг индукции — операции надстраивания LS. Индукция по уровням есть словесная запись того, как иерархия сложена — из основания и надстраиваний; и властна она над всей иерархией потому, что иерархия вся из них и состоит.

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

Та же индукция, другое обоснование

Стоит точно сказать, как индукция по уровням соотносится с индукцией кардинального пути (§ 2.6).

Индукция та же по форме. Раз ряд уровней изоморфен натуральному ряду, индукция по уровням и индукция по числам имеют одну и ту же форму — база плюс сохраняемый шаг. Но здесь нужна та же точность, что и в § 3.4 относительно LS и S. Строго говоря, Level_ind (принцип индукции для типа уровней) и nat_ind (принцип индукции для nat) — не буквально один и тот же Coq-объект: это разные индукционные принципы, ибо относятся к разным индуктивным типам. Каждый из них Rocq порождает автоматически из объявления своего типа. Через изоморфизм Level с nat эти два принципа имеют одну и ту же форму и переносятся друг в друга — но речь идёт не о буквальном равенстве двух Coq-объектов, а о структурном совпадении индуктивной схемы. Level_ind есть nat_ind, перенесённая на тип уровней через изоморфизм, — ровно так же, как LS есть S, перенесённая на уровни (§ 3.4.4).

Но обоснование индукции на двух путях разное — и в этом всё дело. Кардинальный путь обосновал индукцию повторимостью акта: база — первый акт, шаг — ещё один акт (§ 2.6.3). Иерархический обосновывает её устройством иерархии: база — основание, шаг — надстраивание. Один и тот же принцип индукции получает на двух путях два независимых обоснования. И это — то же, что было с самим натуральным рядом (§ 3.6): не два принципа, а один; не два обоснования одного и того же рассуждения, а два независимых пути к одному принципу. Совпадение здесь свидетельствует так же, как свидетельствовало там: индукция не есть произвольно принятая аксиома — она есть то, к чему ToS вынуждена приходить, прослеживая устройство ряда, с какой бы стороны к этому устройству ни подступать.

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

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

Итог

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

Глава прошла второй из четырёх путей ToS к натуральному ряду — путь иерархический.

Путь начался с того, что ToS приходит к натуральному ряду не единожды: к одному ряду ведут несколько независимых деривационных дорог, и множественность их есть свидетельство, а не избыточность (§ 3.1). Иерархический путь оперся на закон $L5$ и порождаемую им иерархию уровней — на вертикальную сторону $L5$, тогда как кардинальный путь опирался на горизонтальную (§ 3.2). Было показано, что всякая иерархия уровней конечна снизу: у неё есть основание, и конечность снизу не постулат, а устройство типа уровней; отсюда ряд уровней имеет начало, и начало именно с единицы, ибо глубина базового уровня есть единица (§ 3.3). Затем — ядро пути: тип уровней Level и тип натуральных чисел устроены одним и тем же образом — базовый элемент плюс операция следования, — и потому LS (надстраивание уровня) есть S (следование числа), а ряд уровней есть натуральный ряд; число есть уровень (§ 3.4). Это тождество было пройдено в движении: восхождение по иерархии, начатое от основания и неограниченно продолжаемое, порождает натуральный ряд, причём ряд уровней бесконечен потенциально, по $P4$ (§ 3.5). Два пути — кардинальный и иерархический — были сопоставлены: различные деривацией, они дают тождественный ряд, и совпадение это есть довод о структурной неизбежности $N$; при этом два независимых пути не задают двух измерений, а суть два описания одной прямой (§ 3.6). Наконец, индукция и на иерархическом пути оказалась не аксиомой: база её отвечает основанию иерархии, шаг — надстраиванию (§ 3.7).

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

Разбор E/R/R: число-уровень как система

{ Пройденный путь имеет E/R/R-устройство (Часть I), и его разбор закрепляет итог главы. Заголовок отдельного файла-якоря задаёт разметку прямо: элементы — уровни; роль — кодирование иерархии; правила — изоморфизм с nat и иррефлексивность порядка.⁶ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе: <<система>> здесь — содержательная интерпретация (число-уровень); её формальная опора — индуктивный тип Level и доказанный изоморфизм с nat, причём строгий машинный изоморфизм установлен на отдельной копии типа уровней, изоморфной Core-типу по форме (§ 3.4).}

Rules — правила (закон $L5$). Конституция системы — закон $L5$: он и делает иерархию уровней возможной, задавая, что система выстраивает уровни (§ 3.2). К нему примыкают три правила, доказанные в коде. Первое — изоморфизм с nat: LS переходит ровно в S (§ 3.4), и ряд уровней есть натуральный ряд. Второе — иррефлексивность порядка (hierarchy_irrefl: ни один уровень не ниже самого себя) вместе с конечностью снизу: у иерархии есть основание, и ряд начинается с единицы (§ 3.3). Третье — индукция по уровням: база отвечает основанию, шаг — надстраиванию (§ 3.7). И самая общая конституция — $P4$: восхождение есть процесс, ряд уровней потенциально бесконечен, а не завершён (§ 3.5).

Roles — значимость позиций (закон $L4$). Роль уровня есть его глубина — число надстраиваний, отделяющих его от основания. Функция level_depth сопоставляет каждому уровню это число и тем служит мостом уровень $\to$ число (§ 3.4.5): роль уровня и есть его число. Роль конституируется правилом: глубина определена индукцией базы и надстраивания — тех же правил, что задают иерархию. Есть и второй ролевой слой: сами пути к ряду — кардинальный и иерархический — суть две роли-режима доступа к одному ряду, а не два разных ряда (об этом § 3.8.3).

Elements — носители (закон $L1$ и принцип $P4$). Элементы — сами уровни: базовый L1 и надстроенные LS $l$. По $L1$ каждый уровень тождествен себе (равенство уровней разрешимо). По $P4$ всякий уровень достигается за конечное число надстраиваний от основания — носитель конечен, хотя ряд их потенциально бесконечен.

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

Компонент	Что фиксирует	E/R/R
$L5$; изоморфизм с nat (LS есть S)	конституция системы	Rule
иррефлексивность + конечность снизу	начало ряда (с единицы)	Rule
индукция по уровням; восхождение ($P4$)	порождение ряда	Rule
глубина level_depth (мост к числу)	роль уровня	Role
уровни L1, LS $l$	носители (конечны, $P4$)	Element
законы $L1$–$L5$ (здесь $L5$)	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: уровни — элементы, глубина — роль, $L5$ с изоморфизмом и иррефлексивностью — правила; ни один слой не подменяет другого. Принцип $P1$ (нет самочленства) выполнен здесь в особенно наглядной форме — как доказанная иррефлексивность: ни один уровень не ниже самого себя (hierarchy_irrefl), иерархия строго восходит, без петель, и система не содержит себя в роли собственного уровня. И здесь разбор оборачивается диагностикой. Соблазн увидеть в двух путях — кардинальном и иерархическом — два разных числа (или два измерения числа) есть смешение категорий: путь — это роль, режим доступа, а не элемент-объект; два режима выводят к одному и тому же ряду (§ 3.8.3). Так же не следует смешивать уровень (элемент) и его глубину (роль-число): <<LS есть S>> утверждает совпадение правила следования при изоморфизме, а не тождество двух Coq-объектов (§ 3.4).

Что даёт разбор. Он объясняет, почему два независимых пути сошлись к одному ряду: число есть роль — позиция, задаваемая базой и следованием, — и оба пути назначают эту роль по одним и тем же правилам ($L1$–$L5$), лишь на разных носителях (списки различий там, уровни здесь). Совпадение не случайно: одна система ролей в двух реализациях. Этим Часть II готовит и остальные пути: каждый следующий — новый носитель той же ролевой структуры числа, и следующий, бинарный, добавит ещё один (§ 3.8.4).

Два пути, один ряд

Часть II прошла теперь два пути к натуральному ряду, и стоит назвать, что этим достигнуто.

Кардинальный путь (Глава II.2) вывел $N$ из повторимости акта различения: число как длина списка различий. Иерархический путь (настоящая глава) вывел $N$ из закона порядка: число как уровень иерархии. Деривации независимы — ни одна не пользуется посылками другой, — а итог тождествен: один и тот же натуральный ряд, с одной и той же единицей в начале, с одной и той же операцией следования, с одной и той же потенциальной бесконечностью.

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

Переход к третьему пути

Путей к натуральному ряду ToS насчитывает четыре (§ 3.1). Два пройдены; остаются два.

Третий путь — бинарный, или информационный. Он исходит из того, что всякий акт различения есть выбор из двух — полагание $A$ при $\neg A$, и ничего третьего: акт различения по самому своему устройству двоичен. Из этой двоичности — из того, что единица различения есть один выбор «да или нет», — развернётся свой подход к натуральному ряду: число как длина двоичной записи, как количество двоичного выбора. Это — путь, на котором натуральное число обнаруживает родство с понятием информации.

Третьему пути и посвящена следующая глава.

---

---

Часть: Часть II. Натуральные числа · Том: «Математика»

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

Навигация: ← Глава 2. Счёт как длина списка различий · Глава 4. Бинарный путь: число как количество двоичного выбора →

Footnotes

1. Формально убывание глубины вдоль порядка зафиксировано в TheoryOfSystems_Core_ERR.v леммой level_lt_depth: из $l_1\ll l_2$ следует $‘leve{l}_{d}epth‘l_1<‘leve{l}_{d}epth‘l_2$. Из неё несуществование бесконечно убывающей цепи выводимо (через невозможность бесконечно убывающей последовательности в nat), но как отдельная теорема о цепях это в репозитории пока не оформлено. ↩

2. В текущем TheoryOfSystems_Core_ERR.v этих двух лемм (L1_minimal и level_lt_successor) нет как отдельных именованных утверждений, хотя обе следуют из определения level_lt немедленно. Это — предмет для будущей синхронизации репозитория. ↩

3. Тип Level, как и функция глубины leveldepth ниже, определён в файле TheoryOfSystemsCore_ERR.v Rocq-репозитория ToS; теоремы об отношении порядка уровней — в файле LawsFromDistinction.v. Здесь и далее имена файлов репозитория приводятся для справки. ↩

4. В файле L5_NatFromHierarchy.v: отображения level_to_nat и nat_to_level вместе с двумя леммами кругового обхода — level_nat_level и nat_level_nat — устанавливают их взаимную обратность. ↩

5. В текущем TheoryOfSystems_Core_ERR.v эти две леммы как отдельные именованные утверждения отсутствуют, хотя обе тривиально следуют из определений; их добавление — предмет будущей синхронизации репозитория. Содержательно открытость иерархии вверх обеспечена уже тем, что конструктор LS тотален. ↩

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