Глава 2. Счёт как длина списка различий

Глава II.1 установила, чем первична единица: она есть число первого акта различения, отпечаток совершённого. Но первичность единицы — ещё не натуральный ряд. Установить, что счёт начинается с единицы, и построить из этой единицы весь ряд натуральных чисел — две разные задачи. Первая решена; вторая — предмет настоящей главы и трёх последующих.

ToS приходит к натуральному ряду не одним путём, а четырьмя — кардинальным, иерархическим, информационным и структурным. Что путей именно четыре и что все они ведут к одному и тому же — не случайность; смысл этой множественности раскроется в Главе II.5. Настоящая глава открывает первый путь — кардинальный. Он самый прямой: если единица есть один акт различения, то число $n$ есть $n$ актов различения, и формой, в которой $n$ актов берутся как одно число, служит список. Кардинальный путь превращает интуицию § 1.6 — счёт как фиксация числа совершённых различений — в работающую формальную конструкцию.

От одного акта к нескольким

Что значит «несколько актов»

Единица есть один акт различения (§ 1.2). Чтобы построить из неё числовой ряд, нужно понять, что значит несколько актов — и понять это точно, потому что здесь скрыт нетривиальный шаг.

«Два акта различения» — что это? Соблазнительно ответить: два акта — это просто акт и ещё акт, положенные рядом. Но такой ответ недостаточен, и недостаточность его поучительна. Чтобы у нас было два акта, а не один, нужно, чтобы первый акт и второй были различены — иначе они слились бы в один, и счёт не сдвинулся бы с единицы. А различить первый акт и второй — значит совершить ещё одно различение: различение между «актом, уже совершённым» и «актом, совершаемым теперь».

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

Повторимость акта

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

Повторимость нужно понять верно, иначе она исказится в одну из двух сторон.

Повторимость не есть тождественное воспроизведение. Повторить акт — не значит получить буквально тот же самый акт. Второй акт отличен от первого уже тем, что он второй — что он совершён относительно положения, в котором первый акт уже есть. Повторение акта различения само создаёт различие — различие порядка, различие «прежде» и «теперь». Если бы повторение давало тождественный акт, никакого «двух» не возникло бы; возникает оно именно потому, что повторённый акт занимает иное место в порядке, чем исходный.

Повторимость не есть и наличие готового запаса актов. Сказать «акт повторим» не значит сказать, что где-то уже лежат все будущие повторения — бесконечный запас актов, ожидающих использования. Готового запаса нет. Повторимость есть возможность совершить ещё один акт, а не наличие всех актов сразу. Это различение — между возможностью продолжения и наличием завершённого — существенно, и оно вернётся в § 2.7 как первое рабочее применение принципа $P4$. Пока достаточно отметить: акт повторим означает «совершив $n$ актов, можно совершить $(n+1)$-й», а не «все акты уже совершены».

Рекурсия счёта

Соединив сказанное, получаем структуру, лежащую в основании счёта.

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

Эту рекурсию предстоит проследить до её формальной структуры. Рекурсия счёта несёт в себе три черты сразу: актов несколько (множественность); они упорядочены — есть первый, второй, $n$-й (порядок, $L5$); и все они вместе берутся как одно число (единство). Структура, в которой эти три черты соединены, не выбирается из набора возможных — она вынуждена тем, что рекурсия счёта уже собой представляет. Проследив, к чему рекурсия приводит, глава обнаружит эту структуру; обнаружится список. К нему глава теперь и переходит — не выбирая его, а прослеживая деривацию до него.

Список как форма множественности

От рекурсии к структуре

Глава не выбирает форму для множественности актов — она прослеживает деривацию. Рекурсия счёта (§ 2.1.3) уже есть некоторая структура; задача в том, чтобы распознать её, дать ей точное имя, а не подобрать ей удачное вместилище.

Что рекурсия счёта собой несёт, установлено в § 2.1: акты совершаются один за другим (повторимость, § 2.1.2); каждый следующий упорядочен относительно предыдущих — второй есть второй относительно первого ($L5$, § 2.1.1); и всё совершённое берётся как одно число (§ 2.1.3). Эти черты не пожелания, которые форме надлежит удовлетворить, — это то, чем рекурсия счёта уже является. Структура, отвечающая им, тем самым не выбирается: она вынуждена. Глава лишь доходит до неё по деривации и называет.

Структура, к которой деривация приводит, есть список. Ниже это показано в несколько шагов: сначала — что множество, привычная математике форма множественности, не годится для первичного кардинального пути (§ 2.2.2); затем — что список деривации отвечает (§ 2.2.3); далее тот же итог подтверждается разбором обеих структур аппаратом E/R/R (§ 2.2.4); наконец — что список отвечает деривации не приблизительно, а в точности (§ 2.2.6). Разбор множества здесь не сравнение конкурентов, из которого список выходит победителем, а проверка: убедиться, что обнаруженное деривацией есть именно список и ничто другое.

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

Множество — форма, в которую математика привычно собирает многое. Сосчитать множество — найти его мощность; натуральное число в теоретико-множественном построении и есть мощность, либо определённое множество (§ 1.1). Привычка подсказывала бы взять множество и здесь. Но для первичного кардинального пути ToS множество не подходит — и не подходит по трём независимым основаниям. Подчеркнём сразу: речь не о том, что ToS изгоняет множество из математики. Множество остаётся вполне законным математическим объектом; оно не годится лишь на роль первичной формы кардинального пути — той структуры, в которой счёт впервые осуществляется. Чем множество является в ToS — режимом рассмотрения, производным от списка (мотив $M_3$, Глава I.7), — сказано ниже; здесь же показывается, отчего оно не может стоять в основании счёта.

Множество статично. Множество есть собрание, все элементы которого даны сразу: $\{a,b,c\}$ не «строится» от $a$ к $c$ — оно есть готовая совокупность. Это онтология готового. Но деривация ToS на первичном уровне готового не содержит — в её основании акт и его повторение (Глава I.7, процессность). Множество навязало бы актам различения статус готовой совокупности, которого деривация им не даёт.

Множество не несёт порядка. В множестве $\{a,b,c\}$ нет первого, второго, третьего элемента — $\{a,b,c\}$ и $\{c,a,b\}$ суть одно множество. Порядок множеству безразличен. Но рекурсия счёта (§ 2.1.1) упорядочена по самому своему устройству: второй акт есть второй относительно первого, и без этого «относительно» не возникает самого «двух». Структура, к которой ведёт деривация, несёт порядок ($L5$); множество его не несёт — и потому деривации не отвечает.

Множество в ToS производно. Глава I.7 ввела мотив $M_3$: множества в ToS не первичны — они суть режим рассмотрения, способ взять нечто, отвлёкшись от порядка и кратности. Натуральное число — объект, к которому деривация приходит прежде режима; строить его через множество значило бы поставить производное прежде того, из чего оно производно. Порядок обоснования был бы нарушен.

Три основания указывают в одно: множество не есть структура, в которой кардинальный путь может начаться. Не потому, что множество «плохо» — как режим рассмотрения оно вполне законно (§ 1.8.5, $M_3$), — а потому, что рекурсия счёта несёт порядок и процессуальность, а множество как первичная форма не несёт ни того, ни другого. Множество исключено не из математики ToS и не как допустимый объект — оно исключено лишь как первичная форма кардинального пути. Позже, как режим рассмотрения списка, оно в ToS законно возникает; но в основании счёта стоять не может.

Почему деривация приводит к списку

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

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

Список несёт порядок. В списке есть первый элемент, второй, $n$-й; список $[a,b,c]$ и список $[c,a,b]$ — разные списки. Порядок не приписан списку извне как дополнительная структура — он есть часть того, что список есть. И этот порядок — ровно $L5$: закон порядка, выведенный в Главе I.3, здесь получает свою рабочую форму. Когда мы говорим «три различия», список удерживает не только их число, но и то, что они идут первым, вторым, третьим, — а это, как показал § 2.1, и есть условие самого «трёх».

Список не вводит готовой совокупности. Список из $n$ элементов не предполагает «множества всех элементов» как отдельной сущности — он есть просто результат $n$ актов присоединения. Никакого перехода к режиму $M_3$, никакого обращения к производному. Список остаётся на том же уровне первичности, что и акт, чьим отпечатком он служит.

Множество есть статическая совокупность готового, безразличная к порядку и производная по $M_3$; для удержания упорядоченной последовательности совершаемых актов оно несёт не ту структуру. Список последователен, упорядочен ($L5$) и не вводит готовой совокупности. Поэтому формой кардинального пути служит список, а не множество.

Список и множество в разборе E/R/R

Сказанное можно увидеть отчётливее, если разобрать список и множество аппаратом, который Глава I.4 дала для всякой системы, — разбором E/R/R. Глава I.4 установила: всякая система имеет три неотделимых аспекта — Elements (элементы, субстрат системы), Roles (роли, позиции, которые элементы занимают) и Rules (правила, удерживающие систему как систему), — и что онтологически они порождают себя в порядке Rules $\to$ Roles $\to$ Elements. Приложим этот разбор к списку и к множеству; ничего нового об E/R/R здесь не вводится — лишь применяется уже данное.

Список как система E/R/R. Список различий, разобранный по трём аспектам, даёт следующее. Rules — правило следования: каждый элемент, кроме первого, стоит непосредственно после одного определённого элемента. Это правило и есть рабочая форма $L5$ — закона порядка. Roles — позиции, которые правило следования открывает: «первая», «вторая», «$n$-я»; роль здесь расчленена, позиций столько же, сколько элементов, и каждая отлична от прочих своим местом в следовании. Elements — сами различия, занимающие эти позиции. Три аспекта налицо и неотделимы: правило следования без позиций было бы пустой схемой, позиции без различий — незаполненными, различия без позиций — грудой без порядка. Список есть полная система E/R/R: все три аспекта в нём работают.

Множество как система E/R/R. Множество тех же различий по трём аспектам даёт иное. Elements — те же различия. Roles — но здесь роль одна и нерасчленённая: «член множества»; все элементы несут одну и ту же роль, никакая позиция не отлична от другой. Rules — и здесь нужна точность. Было бы неверно сказать, что у множества нет аспекта Rules вообще: у множества есть свои правила — правило членства (что значит быть элементом) и правило экстенсионального отождествления (два множества равны, когда у них одни и те же элементы), а в развёрнутых теориях — и правила образования. Аспект Rules у множества не исчезает. Исчезает одно определённое правило — правило следования, то, которое в списке удерживает порядок: <<каждый элемент, кроме первого, стоит после одного определённого>>. Сравнив с разбором списка, видим точно, что произошло: у множества погашено не Rules вообще, а именно правило следования; вместо него остаются правила членства и экстенсионального отождествления. И вместе с правилом следования — по порождающему порядку Rules $\to$ Roles $\to$ Elements — гаснет расчленённость Roles: нет правила следования — нет и упорядоченных позиций, остаётся одна общая роль <<член>> и субстрат под ней.

Что отсюда видно. Множество не есть система, чужеродная списку. Но было бы неточно сказать, что множество есть тот же список: один и тот же набор значений получается из разных списков — $(a,b,c)$, $(c,b,a)$, $(a,a,b,c)$ все дают одно множество $\{a,b,c\}$. Точнее сказать, что множество есть support списка — результат забывания того, чем эти списки различаются: порядка и кратности. Переход удобно представить двумя ступенями:

$$\text{List}(A)⟶\text{Multiset}(A)⟶\text{Set}(A).$$

Первая ступень забывает порядок (список $\to$ мультимножество), вторая — кратность (мультимножество $\to$ множество). Именно это означал мотив $M_3$ (§ 1.8.5): множество как режим рассмотрения списка, отвлекающийся от порядка и кратности. Разбор E/R/R даёт первой ступени точную форму: переход от списка к мультимножеству есть гашение правила следования — того аспекта Rules, который удерживал порядок.

И тогда видно, почему деривация счёта приводит именно к списку. Рекурсия счёта (§ 2.1) существенно несёт правило следования: второй акт есть второй по следованию за первым. Структура, к которой ведёт деривация, обязана иметь правило следования. Список это правило имеет; множество — есть та же структура с погашенным правилом следования (правила членства и отождествления при этом остаются). Деривация, требующая следования, приводит к списку — к системе, в которой правило следования работает; множество ей отвечать не может не оттого, что оно «беднее» вообще, а оттого, что в нём погашено ровно то правило, которое деривация требует.

В разборе E/R/R список есть полная система: Elements — различия, Roles — упорядоченные позиции, Rules — правило следования ($L5$). Множество есть тот же список с погашенным правилом следования, отчего расчленённость ролей сводится к одной общей роли «член»; это и есть режим $M_3$. Деривация счёта несёт правило следования и потому приводит к полной системе — к списку.

Список как отпечаток повторимого акта

Стоит увидеть, насколько точно список отвечает рекурсии счёта из § 2.1.3 — настолько точно, что список можно назвать прямым отпечатком повторимого акта.

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

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

Что список устроен рекурсивно — свойство не только содержательное, но и формальное: в этой рекурсивности коренится принцип индукции, к которому глава придёт в § 2.6. Пока отметим лишь, что деривация доведена до своей структуры: рекурсия счёта есть список. Остаётся придать списку точную формальную запись — и через неё определить, что значит «число $n$ есть в системе». Это предмет следующих двух разделов.

Технический предикат: distinction_count

Список различий и длина как акт подсчёта

Деривация привела к списку как структуре множественности актов (§ 2.2). Придадим этому точную запись.

Акт различения записан в ToS как Distinction (Глава I.2). Список актов различения есть, соответственно, объект типа list Distinction — список, элементами которого служат различия. Такой список есть отпечаток некоторого числа совершённых актов: списку из $n$ различий отвечают $n$ совершённых различений, взятых в их порядке.

Кардинальный путь ведёт к числу через длину такого списка — и здесь нужна точность, иначе в построение проникнет чуждая ToS предпосылка. Длина списка не есть свойство, присущее списку как готовому объекту, — нечто, что в списке «лежит» и что остаётся лишь «считать». Готового, в котором свойства лежат заранее, ToS на первичном уровне не знает (Глава I.7, процессность; § 1.7.2: всякая характеристика есть совершённое различение). Длина списка есть результат акта — акта подсчёта: акта, который проходит список различие за различием и регистрирует, сколько совершённых актов в нём встречено. Длина не присуща списку — она получается, когда акт подсчёта совершён.

Это прямое продолжение § 1.6: считать — значит фиксировать число совершённых различений. Длина списка различий и есть это зафиксированное число: сколько совершённых актов регистрирует подсчёт, пройдя список. Понятие длины, таким образом, не привносит в ToS ничего нового — оно есть приложение счёта-как-фиксации к списку. Формально подсчёт записывается функцией length; но функция эта не «считывает присущее списку число», а производит число как итог прохождения списка. Через длину списка различий — через этот итог подсчёта — и вводится первое формальное понятие настоящей главы.

Определение distinction_count

ToS вводит предикат, связывающий натуральное число $n$ со списками различий, подсчёт которых даёт $n$. Формально он записывается так:¹

Definition distinction_count (n : nat) : Prop :=
  exists Ds : list Distinction, length Ds = n.

Прочитаем определение. distinctioncount — это предикат на натуральных числах: каждому $n$ он сопоставляет высказывание (Prop). Высказывание это таково: существует список различий, длина которого равна $n$. Предикат distinctioncount;$n$ истинен, если такой список существует, и ложен в противном случае.

Существенно, чем это определение не является. Оно не есть переопределение натурального числа: $n$ здесь — уже готовое натуральное число типа nat, и предикат лишь что-то о нём высказывает. Оно не есть и утверждение «число $n$ равно длине списка»: предикат не приравнивает $n$ к длине, а спрашивает о существовании списка нужной длины. distinction_count — именно предикат: характеристика, которой число либо обладает, либо нет.

Нуль и пустой список

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

Истинно ли distinction_count;$0$? По определению это значит: существует ли список различий, подсчёт которого даёт нуль? Такой список есть — это пустой список, список без единого элемента. Формально это засвидетельствовано:

Lemma zero_distinctions : distinction_count 0.
Proof. exists []. reflexivity. Qed.

Доказательство предъявляет пустой список ([]). Но здесь важно верно прочесть, что именно происходит при его подсчёте, — иначе нуль будет понят неправильно.

Подсчёт есть акт прохождения списка с регистрацией встреченных совершённых актов (§ 2.3.1). А длина есть итог совершённого подсчёта. Применим это к пустому списку.

Запрос «какова длина пустого списка?» есть запрос об итоге подсчёта, и запрос этот законен: его предмет — пустой список — есть сформированная система (E/R/R, § 2.2.4), полноправная структура типа list Distinction, к которой подсчёт применим. Достаточное основание ($L4$) для акта подсчёта здесь есть: основанием служит то, что предмет запроса является списком. Подсчёт законно совершается — и при прохождении пустого списка не встречает ни одного элемента. Поэтому его итог есть $0$: не положительная длина ряда совершённых актов, а граничный результат корректно совершённого подсчёта, фиксирующий, что встреченных различий не было.

Что же тогда есть нуль? Нуль здесь не есть число совершённого; он есть значение подсчёта, завершившегося без встречи элемента. Подсчёт состоялся (основание было — предмет есть список), прошёл список до конца и не встретил ни одного акта — и его итогом стал $0$. Это в точности нуль Главы II.1: не предмет и не свойство, не положительный счёт совершённого, а граничная отметка — результат подсчёта, проявляющий отсутствие встреченных различий (§ 1.3.2). Пустой список не несёт «положительной длины»; он есть отпечаток того, что не совершено ничего, и нуль есть итог подсчёта, этот факт зарегистрировавшего.

Здесь стоит ответить на вопрос, который сам собой возникает: почему запрос длины к пустому списку даёт нуль, а не ошибку? Различие двух исходов не случайно, и оно проясняет природу нуля. Ошибкой запрос завершается тогда, когда он бессмыслен — когда обращается к качеству, которого у предмета нет даже в принципе. Спросить длину у того, что вообще не список, — у акта, у числа, — значит задать вопрос, не имеющий логической связи с предметом; такой вопрос не «не получил значения», он не имел права быть заданным, и ответ на него — ошибка. Запрос же длины к пустому списку не таков. Пустой список есть список — сформированная система, для которой подсчёт определён. Запрос к нему осмыслен и выполним: подсчёт законно совершается и доходит до конца. Его итог — $0$ — есть полноправный результат, а не отказ: подсчёт прошёл список и зарегистрировал, что встреченных элементов не было. Оттого пустой список даёт нуль, а не ошибку: подсчёт определён и выполнен (значит не ошибка), но встреченных различий не было (значит не положительное значение, а граничный нуль). Ошибка лежала бы за границей осмысленного запроса; нуль стоит внутри нея — как законный итог подсчёта, не встретившего ни одного акта.

Здесь полезно прямо назвать формальный факт, на который всё опирается. Функция length тотальна: всякому списку-терму, включая nil, она сопоставляет терм типа nat, и length nil вычислительно редуцируется к 0 — оттого zero_distinctions и доказуема. Это не побочное обстоятельство, которое онтологии приходится «обходить», — напротив, это и есть формальная сторона сказанного: подсчёт пустого списка определён и его результат есть $0$. Онтологическое чтение лишь называет этот $0$ — не «измеренной положительной длиной», а граничным итогом подсчёта, не встретившего элементов. Синтаксис возвращает терм 0; онтология читает этот 0 как границу ряда положительных длин, а не как положительный счёт совершённого.

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

Уровень	Что такое $0$
тип nat	конструктор O, базовая точка типа
функция length	результат подсчёта пустого списка (length nil редуцируется к 0)
онтология ToS	граница положительного счёта — итог подсчёта, не встретившего ни одного совершённого акта

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

Отсюда видно, что истинность distinction_count;$0$ не означает, будто нуль есть число совершённых актов различения. Глава II.1 (§ 1.3) установила обратное: нуль не есть счёт совершённых актов. Противоречия здесь нет — и увидеть, почему, важно для всей главы.

distinctioncount;$0$ истинно, и истинно законно: список nil существует, подсчёт его определён и length nil есть 0. Но что этим засвидетельствовано — не «существует список, чей подсчёт дал положительную длину нуль», а «существует список, подсчёт которого законно завершился, не встретив ни одного элемента, и итог этого подсчёта есть нуль». Засвидетельствовать граничный итог подсчёта — не то же самое, что сосчитать совершённое. Пустой список не есть список, в котором «совершено нуль актов» как некое содержательное событие, — пустой список есть список, в котором не совершено ничего. Совершённого различения в нём нет; есть лишь подсчёт, прошедший список и не встретивший элементов, с итогом нуль. distinctioncount честно этот итог фиксирует — но фиксирует именно граничный результат подсчёта, а не положительный счёт совершённого.

Технический слой

Сказанное помещает distinction_count на вполне определённое место — на то, что Глава I.6 назвала техническим слоем формальной работы.

distinctioncount отвечает на технический вопрос: для каких $n$ существует список различий, подсчёт которого даёт $n$? Это вопрос о списках и об итогах их подсчёта — о том, какие итоги подсчёта вообще достижимы. Вопрос законный и нужный: без подсчёта списков не обойтись. Но это не вопрос о счёте совершённых актов различения. distinctioncount не несёт онтологической нагрузки счёта совершённого — он регистрирует итог подсчёта, в том числе итог «не встречено ничего», отвлекаясь от того, что список различий есть отпечаток совершённых актов.

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

distinction_count — технический предикат: он сообщает, для каких $n$ существует список различий, подсчёт которого даёт $n$. Для нуля он истинен — но истинен потому, что подсчёт пустого списка законно даёт результат $0$, а не потому, что нуль есть число совершённых актов. Это регистрация формы данных, не счёт совершённого. Кардинальный путь требует предиката иного — такого, который считает совершённые акты и потому начинается с единицы.

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

Онтологический предикат: distinctioncountfrom_one

Чего недостаёт техническому предикату

Технический предикат distinction_count (§ 2.3) сообщает, для каких чисел существует список различий нужной длины. Кардинальному пути этого недостаточно, и недостача — ровно в одном: технический предикат считает длину списка, а кардинальный путь должен считать совершённые акты различения.

Различие не словесное. Подсчёт пустого списка законно даёт результат $0$ (§ 2.3.3): подсчёт определён, прошёл список и не встретил ни одного элемента. Совершённых актов в пустом списке нет: пустой список есть отпечаток того, что не совершено ничего. Технический предикат distinction_count засчитывает нулю быть граничным итогом подсчёта пустого списка; кардинальный путь, считая совершённые акты, не находит в пустом списке ни одного совершённого акта и потому начинается с единицы — с первого совершённого различения. Глава II.1 (§ 1.3) установила это как онтологическое положение; теперь оно должно получить формальный предикат, который ему отвечает.

Определение distinctioncountfrom_one

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

Definition distinction_count_from_one (n : nat) : Prop :=
  exists Ds : list Distinction, length Ds = n /\ 1 <= n.

Предикат distinctioncountfromone отличается от технического distinctioncount одним добавленным условием — $1\le n$. Прочитаем: число $n$ удовлетворяет предикату, если существует список различий длины $n$ и при этом $n$ не меньше единицы. Первое условие — то же, что у технического предиката: существование списка нужной длины. Второе — $1\le n$ — и есть формальная запись того, что счёт совершённого начинается с единицы.

Здесь нужна точность относительно того, что этот предикат формально собой представляет. По записи distinctioncountfrom_one отличается от технического предиката только конъюнктом $1\le n$ — ничем более. Он не проверяет, что элементы списка суть именно <<совершённые акты>>; не хранит истории их совершения; не различает стадий; не требует, чтобы акты были попарно различны. Формально это — фильтр положительности: предикат, отсекающий нулевую границу и пропускающий всякое $n\ge 1$, для которого существует список нужной длины. Поэтому его онтологический смысл — счёт совершённых актов различения — не содержится в одной лишь формальной записи; он задаётся интерпретацией главы, прочитывающей список различий как отпечаток совершённых актов. Формальная запись и онтологическое чтение здесь работают вместе: запись отделяет положительный счёт от нулевой границы, а интерпретация наделяет этот положительный счёт смыслом счёта совершённого.

Добавленное условие невелико по виду и существенно по смыслу. Оно проводит границу, установленную в Главе II.1: нуль — не счёт совершённых актов, а граница ряда (§ 1.3). Технический предикат этой границы не проводил и засчитывал нуль; distinctioncountfrom_one её проводит. Это и позволяет читать его онтологически — как предикат, отвечающий не на вопрос о длинах списков вообще, а на вопрос <<сколько актов различения совершено>>. Подчеркнём ещё раз: само это онтологическое чтение — работа интерпретации, а формальный вклад предиката состоит в условии $1\le n$, отделяющем положительный счёт от нулевой границы.

Нуль выпадает, единица входит

Посмотрим, что предикат distinctioncountfrom_one говорит о двух граничных случаях — о нуле и о единице. О каждом устанавливается ровно то, чего требует онтология Главы II.1; формальная запись этих утверждений приводится ниже.

Нуль не есть счёт.

Theorem zero_not_a_count :
  ~ distinction_count_from_one 0.
Proof.
  intro H. destruct H as [_ [_ Hge]]. lia.
Qed.

Теорема zeronotacount утверждает: предикат distinctioncountfromone не выполнен для нуля. Доказательство коротко: если бы нуль удовлетворял предикату, в числе условий было бы $1\le 0$ — а это ложно, и тактика lia закрывает случай. Содержательно теорема говорит: нуль не есть счёт совершённых актов различения. Не «список длины нуль не существует» — он существует (§ 2.3.3), — а именно: нуль не есть число совершённого, потому что совершённого в нуле нет.

Единица есть первый счёт.

Theorem first_count_is_one :
  distinction_count_from_one 1.
Proof.
  exists [distinction_of True].
  split; [reflexivity | lia].
Qed.

{

Теорема firstcountis_one утверждает: предикат выполнен для единицы. Доказательство предъявляет список из одного различия — [distinction_of True], список с единственным элементом, — и проверяет два условия: длина его равна единице (reflexivity), и $1\le 1$ (lia). Оба выполнены. Единица есть первый счёт совершённых актов: ей отвечает список из одного совершённого различия. }

Два результата вместе очерчивают начало кардинального пути точно так, как его описала Глава II.1: нуль выпадает из счёта совершённого, единица есть первое число этого счёта. То, что в § 1.3 было онтологическим положением, здесь стало доказанной парой теорем.

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

Предикат	Формальная запись	Что считает	Нуль
distinction_count	exists Ds, length Ds = n	техническую длину списка	допускает
distinction_count_from_one	exists Ds, length Ds = n /\ 1 <= n	положительный счёт актов (при онтологическом чтении)	исключает

Таблица делает явной природу различия: формально оно сводится к одному конъюнкту $1\le n$, а содержательно — к границе между подсчётом списков вообще и счётом совершённого, начинающимся с единицы.

Что значит «число есть в системе»

Предикат distinctioncountfrom_one позволяет сказать точно, что означает в ToS присутствие натурального числа.

Число $n$ есть в системе ToS постольку, поскольку существует список из $n$ совершённых различий и $n\ge 1$. Не «число $n$ дано как элемент готового множества» и не «число $n$ постулировано аксиомой» — а: число $n$ есть, поскольку реализуемо как отпечаток $n$ совершённых актов различения.

Это — онтологический ход, и стоит назвать его прямо. Бытие числа в ToS есть бытие через реализацию. Число не лежит готовым; число есть постольку, поскольку может быть предъявлен список различий, который его реализует. Существование числа поставлено в зависимость от возможности его реализации актами различения — ровно как существование всего в ToS поставлено в зависимость от акта ($A=\exists$, Глава I.1).

Отсюда видно, в каком смысле кардинальный путь есть путь к натуральному ряду, а не его постулирование. Путь не объявляет $\mathbb{N}$ готовым — он показывает, как каждое натуральное число получает бытие в ToS: через реализацию списком совершённых различий. Остаётся показать, что этот путь проходим для всякого натурального числа — что нет числа, которое не реализовалось бы. Это и есть содержание следующего раздела.

distinctioncountfromone — предикат кардинального пути: формально он есть фильтр положительности (существование списка длины $n$ при $n\ge 1$), а при онтологическом чтении главы — счёт совершённых различий. Число $n$ удовлетворяет ему, если существует список из $n$ различий и $n\ge 1$. Нуль ему не удовлетворяет (zeronotacount), единица удовлетворяет (firstcountis_one). Быть числом в ToS значит быть реализуемым как отпечаток совершённых актов различения.

Реализуемость каждого числа

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

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

В самом деле: предикат distinctioncountfromone мог бы оказаться выполнен лишь для некоторых чисел. Доказанное в § 2.4 покрывает пока единицу (firstcountisone). А остальные? Реализуема ли двойка — то есть существует ли список ровно из двух различий? А число сто? А число, записанное тысячей цифр? Кардинальный путь будет путём к натуральному ряду лишь тогда, когда показано: никакое натуральное число не выпадает — для всякого $n\ge 1$ список из $n$ различий реализуем.

Это и предстоит показать. Утверждение, к которому идёт раздел, таково: для любого $n\ge 1$ предикат счёта от единицы выполнен. ToS устанавливает его как теорему; формально она записывается так:

Theorem positive_nat_is_distinction_count : forall n,
  (1 <= n)%nat -> distinction_count_from_one n.

Прочитаем: каково бы ни было натуральное число $n$, если $n\ge 1$, то $n$ удовлетворяет предикату счёта от единицы — список из $n$ различий реализуем. Раздел разбирает, как это устанавливается и что отсюда следует.

Шаг наращивания: ещё одно различение

Реализуемость каждого числа держится на одном простом шаге — шаге наращивания. Он есть формальный отпечаток повторимости акта (§ 2.1.2): совершив некоторое число актов, можно совершить ещё один.

Присоединение нового различия к списку ToS записывает так:

Definition add_distinction (Ds : list Distinction) (D : Distinction) :=
  D :: Ds.
 
Theorem add_distinction_increments : forall Ds D,
  length (add_distinction Ds D) = S (length Ds).

Первая из приведённых записей, add_distinction, ставит новое различие $D$ в начало списка $Ds$ — технически это D :: Ds, присоединение к голове. Это требует оговорки о порядке. В прозе главы акты совершаются <<первый, второй, третий>> в хронологическом смысле; но D :: Ds помещает новый акт не в конец, а в голову списка. Поэтому список различий здесь удобнее читать как стек: голова хранит последний совершённый акт, хвост — более ранние. Это не влияет на длину — а кардинальному пути нужна именно длина, — но важно для интерпретации порядка: <<первый элемент списка>> при таком чтении есть последний по времени акт. Если же где-то понадобится хронологическое чтение слева направо, его даёт альтернативная операция присоединения в конец списка (snoc); кардинальный путь настоящей главы в ней не нуждается, поскольку опирается на длину, а не на направление порядка.

Теорема adddistinctionincrements проверяет очевидное и существенное: подсчёт наращённого списка даёт на единицу больше, чем подсчёт исходного. Присоединить различие — значит увеличить счёт на один. Это и есть формальная запись того, что совершить ещё один акт различения значит сделать счёт на единицу большим.

Чем различаются повторения акта. Здесь стоит снять одно возможное недоумение. В формальных доказательствах списки различий строятся из одного и того же канонического элемента: firstcountisone предъявляет [distinction_of True], а succisnewdistinction присоединяет distinction_of True к уже имеющемуся списку. Список из трёх различий есть, таким образом, [distinction_of True; distinction_of True; distinction_of True] — три вхождения одного значения. Значит, новизна акта кодируется здесь не различием содержания: два элемента списка могут быть одним и тем же каноническим различением. Их различие как актов задаётся позицией — occurrence в списке: первое вхождение и второе вхождение суть разные повторения акта, даже когда их внутреннее содержание совпадает. Это согласуется с Главой II.1 (§ 1.3, где новизна акта задавалась не различием значения, а повторением) и прямо опирается на Закон Порядка $L5$: именно порядок и позиция, а не содержание элемента, делают список из трёх повторений списком из трёх, а не из одного. Счёт считает вхождения, и потому повторимость одного акта — а не разнообразие содержаний — есть то, на чём держится кардинальный путь.

Отсюда — ключевой шаг кардинального пути: если число $n$ реализуемо, то реализуемо и число $n+1$. ToS устанавливает это так:

Theorem succ_is_new_distinction : forall n,
  distinction_count_from_one n ->
  distinction_count_from_one (S n).

succisnew_distinction говорит: из реализуемости $n$ следует реализуемость $n+1$. Доказательство прямое — взять список, реализующий $n$, и присоединить к нему ещё одно различие; наращённый список реализует $n+1$. Содержательно теорема говорит то, что Глава II.1 назвала бы переходом к следующему числу: следующее число есть нынешнее плюс ещё один совершённый акт. Операция следования — не приписывание извне, а совершение нового различения.

От единицы ко всякому числу

Теперь обе части налицо. Единица реализуема — это firstcountisone (§ 2.4.3): список из одного различия предъявлен. И всякий переход от $n$ к $n+1$ сохраняет реализуемость — это succisnewdistinction (§ 2.5.2). Соединение этих двух и даёт реализуемость каждого числа.

ToS устанавливает соединение теоремой positivenatisdistinction count; её доказательство устроено так. Берётся произвольное $n\ge 1$. Если $n$ есть единица — реализуемость дана прямо (firstcountisone). Если $n$ больше единицы — оно есть $n^{\prime }+1$ для некоторого $n^{\prime }\ge 1$; по предположению $n^{\prime }$ реализуемо, и тогда по succisnewdistinction реализуемо и $n$. Так реализуемость, имея началом единицу, дотягивается до всякого $n\ge 1$.

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

Здесь необходима оговорка о статусе доказанного. Формальная теорема positivenatisdistinctioncount работает внутри уже имеющегося типа nat: она берёт произвольное n : nat и показывает, что при $n\ge 1$ для него существует список различий длины $n$. Поэтому теорема не создаёт тип натуральных чисел заново и не строит nat из Distinction; она показывает, что каждое положительное значение уже данного типа nat реализуемо как длина списка различий. Результат — реализационный, а не типообразующий: ToS не утверждает, будто выводит сам тип nat, а утверждает, что кардинальный путь проходим для всякого положительного nat. Это снимает возможное возражение <<вы пользуетесь nat, чтобы построить nat>>: nat как тип берётся готовым из Rocq; вклад ToS — не построение этого типа, а онтологическое прочтение его положительных значений как отпечатков совершённых различий.

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

Каждое число — но не «все числа сразу»

Реализуемость каждого числа нужно прочесть точно, иначе из неё вычитают больше, чем в ней есть. Теорема говорит: для всякого $n\ge 1$ список из $n$ различий реализуем. Она не говорит, что все эти списки реализованы сразу — что где-то есть готовая совокупность, содержащая разом списки всех длин.

Различие здесь существенно, и оно прямо связано с тем, как ToS понимает бесконечность. «Реализуемо каждое число» означает: какое число ни возьми, для него список реализуем — акт его построения может быть совершён. Это утверждение о каждом отдельном числе, взятом порознь. «Реализованы все числа сразу» означало бы иное: будто все списки уже построены и собраны в один завершённый объект. Первое ToS утверждает; второго — не утверждает, и не случайно.

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

Почему ToS не делает второго шага — не собирает все числа в готовую завершённую совокупность — и почему этот отказ не есть нехватка, а есть прямое следствие принципа $P4$, разбирает § 2.7. Прежде же нужно рассмотреть индуктивную форму, на которую опёрлось доказательство настоящего раздела, — и показать, что в ToS она не аксиома, а вырастает из устройства счёта. Это — предмет § 2.6.

Откуда индукция

Индукция как опора предыдущего раздела

Доказательство реализуемости каждого числа (§ 2.5.3) имело определённую форму: начало — единица реализуема — и сохраняемый переход — из реализуемости $n$ следует реализуемость $n+1$. Из этих двоих был получен вывод о всяком $n\ge 1$. Эта форма рассуждения — начало плюс переход, дающие заключение обо всём ряде — есть математическая индукция.

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

Что утверждает индукция

Напомним форму принципа индукции, не воспроизводя его школьной подачи. Принцип говорит: чтобы некоторое свойство было верно для всякого натурального числа, достаточно двух вещей — чтобы оно было верно для первого числа (база), и чтобы из его верности для $n$ следовала верность для $n+1$ (шаг). База и шаг вместе влекут заключение: свойство верно для всего ряда.

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

Индукция есть форма повторимого акта

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

Числовой ряд в ToS не дан готовым (§ 2.5.4). Он строится — повторением акта различения (§ 2.1). Построение это имеет ровно две составляющие, и других у него нет. Первая: есть первый акт — единица (§ 1.2). Вторая: всякий совершённый акт повторим — за ним можно совершить ещё один, и это есть переход от $n$ к $n+1$ (§ 2.5.2, succisnew_distinction). Первый акт и повторимость — вот и всё, из чего сложен ряд.

Сопоставим это с принципом индукции. База индукции — свойство верно для первого числа. Первая составляющая построения — есть первый акт. Шаг индукции — из верности для $n$ следует верность для $n+1$. Вторая составляющая построения — акт повторим, за $n$ совершается $n+1$. База индукции отвечает первому акту; шаг индукции отвечает повторимости акта. Это не сходство и не аналогия — это одно и то же, выраженное двумя способами: индукция говорит о построении ряда то же, что говорит о нём ToS, разбирая повторение акта.

Принцип индукции не привнесён в числовой ряд извне. База индукции есть первый акт различения; шаг индукции есть повторимость акта. Индукция — словесная запись того самого построения ряда повторением акта, которое ToS прослеживает с § 2.1. Потому в ToS индукция не аксиома: она содержится в устройстве счёта.

Здесь необходима оговорка о формальном слое — иначе сказанное можно понять сильнее, чем оно есть. Машинное доказательство теоремы positivenatisdistinctioncount (§ 2.5.3) использует стандартную индукцию по nat — тактику induction, опирающуюся на встроенный в Rocq принцип индукции для типа nat. То есть в формальном слое ToS не выводит сам принцип индукции из Distinction: принцип индукции по nat берётся готовым вместе с типом nat. Машинная теорема показывает иное — что при стандартной индукции по nat реализуемость положительных чисел через списки различий сохраняется на каждом шаге. Онтологическое объяснение настоящего раздела отвечает не на формальный, а на содержательный вопрос: почему именно индуктивная форма — база плюс сохраняемый шаг — соответствует устройству счёта в ToS. Ответ (индукция есть запись построения ряда повторением акта) остаётся в силе как онтологическое обоснование применимости индуктивной формы; он не есть и не претендует быть формальным выводом принципа индукции из акта различения. Формальный слой пользуется индукцией по nat; онтологический слой объясняет, отчего эта форма здесь уместна.

Почему две посылки властны над всем рядом

Теперь получает ответ и вопрос § 2.6.2: откуда у базы и шага — двух конечных посылок — власть над всем бесконечным рядом?

Власть эта берётся оттуда же, откуда берётся сам ряд. Ряд есть не что иное, как первый акт, повторённый, и повторённый снова, и так далее (§ 2.5.3). Всякое число ряда достигается из единицы конечным числом повторений — иначе оно не было бы в ряду. А база и шаг суть в точности первый акт и одно повторение. Поэтому: что верно для базы (для первого акта) и сохраняется шагом (одним повторением), то сохраняется и вдоль всякой конечной цепочки повторений — то есть верно для всякого достигнутого числа. База и шаг властны над всем рядом не по особому могуществу принципа, а потому, что ряд весь и состоит из применений базы и шага. Индукция «дотягивается» до всякого числа ровно так, как до него дотягивается само построение (§ 2.5.3): шаг за шагом, и каждое число достигается за конечное их число.

Видно и то, чего индукция не даёт — и это важно для § 2.7. Индукция позволяет заключить о всяком числе ряда, ибо всякое достижимо конечной цепочкой. Она не даёт и не предполагает завершённого обхода всего ряда сразу: заключение «для всякого $n$» получается не прохождением бесконечного ряда до конца, а тем, что для любого предъявленного $n$ конечная цепочка база–шаг–…–шаг до него доводит. Индукция работает «по запросу для каждого», а не «разом для всех». Это различение — то же, что в § 2.5.4 («каждое число, но не все сразу»), — и оно прямо подводит к принципу $P4$.

Индукция и формальная запись

Стоит сказать, как сказанное соотносится с формальной стороной дела.

В Rocq натуральные числа — тип nat, и принцип индукции для него доступен как nat_ind — он входит в устройство индуктивного типа. Может показаться, что тем самым индукция в ToS всё же принята вместе с типом nat, а не выведена. Но это смешение двух слоёв, уже различённых в § 1.4 и § 2.3.3.

На слое формальной записи индукция действительно дана вместе с индуктивным типом nat: так устроен Rocq. На слое онтологии ToS вопрос иной — не «доступен ли принцип в Rocq», а «почему он верен, что в самом предмете ему отвечает». И ответ дан выше: индукция верна потому, что числовой ряд строится повторением акта, а база и шаг суть первый акт и повторение. Rocq предоставляет индукцию как готовый инструмент; ToS объясняет, почему этот инструмент приложим — почему числовой ряд таков, что индукция по нему правомерна. Индуктивное устройство типа nat в Rocq есть формальное отображение того, что ToS установила содержательно: ряд порождается первым актом и его повторением.

Что Rocq даёт индукцию вместе с типом nat — факт слоя формальной записи. Почему индукция правомерна — вопрос онтологии, и ToS на него отвечает: ряд строится первым актом и повторением, а индукция есть запись этого построения. Формальная доступность принципа не отменяет того, что в ToS он обоснован, а не постулирован.

На этом кардинальный путь почти завершён: показано, что значит присутствие числа (§ 2.4), что реализуемо всякое число (§ 2.5) и что индукция, на которую это опёрто, вырастает из устройства счёта (§ 2.6). Остался один вопрос — и он уже дважды был отложен. Реализуемо каждое число, но не «все сразу»; индукция властна над всяким числом, но не обходит ряд завершённо. Что это значит для бесконечности натурального ряда — и почему ToS говорит о ней именно так — разбирает следующий раздел.

$P4${P4} и бесконечность

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

Дважды на протяжении главы возникало одно и то же ограничение, и дважды разбор его был отложен. § 2.5.4: реализуемо каждое число, но не «все числа сразу». § 2.6.4: индукция властна над всяким числом, но не обходит ряд завершённо. В обоих случаях ToS утверждала нечто про любой отдельный член ряда и воздерживалась утверждать про ряд как целое.

Воздержание это требует объяснения. Натуральный ряд бесконечен — так скажет всякий, и ToS не возражает. Но что значит «бесконечен»? Если кардинальный путь построил каждое число и не построил «все числа сразу», то бесконечен ли построенный ряд — и в каком смысле? Настоящий раздел отвечает, и ответ опирается на принцип, который до сих пор в Части II не звучал явно, — на $P4$.

Возражение: не есть ли «для всякого $n${n}» обращение к завершённой бесконечности

Поставим возражение в полную силу, потому что оно естественно и на нём проверяется вся конструкция.

Кардинальный путь доказал теорему вида «для всякого $n\ge 1$ список из $n$ различий реализуем» (§ 2.5). Слова «для всякого $n$» пробегают, казалось бы, весь натуральный ряд. А пробежать весь ряд — значит обойти бесконечную совокупность чисел. Не означает ли тогда само утверждение «для всякого $n$», что бесконечная совокупность всех натуральных чисел уже налична как завершённый объект, — иначе по чему бы пробегало «всякий»? И если так, то ToS, заявляя в § 2.5.4 об отказе от «всех чисел сразу», на деле этот отказ нарушает: ведь квантор «для всякого» будто бы уже требует завершённой бесконечности.

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

Универсальная квантификация как схема, не как объект

Смешаны квантор и совокупность. Возражение читает «для всякого $n$» так, будто это обход наличной совокупности — будто, чтобы высказать «для всякого $n$ верно $P$», нужно иметь совокупность всех $n$ и пройти её. Но универсальная квантификация устроена не так.

В ToS, как и в строгой конструктивной трактовке вообще, утверждение «для всякого $n$ верно $P(n)$» есть не высказывание о завершённой совокупности, а схема: обязательство, что для любого предъявленного $n$ может быть предъявлено доказательство $P(n)$. Утверждение «для всякого $n$» не описывает обойдённую бесконечность — оно обещает ответ на запрос: какое $n$ ни назови, доказательство $P(n)$ будет построено.

И ToS показала в точности это (§ 2.6.4): для любого предъявленного $n$ конечная цепочка база – шаг – … – шаг доводит до $P(n)$. Никакого обхода бесконечной совокупности здесь нет — есть конечная цепочка, своя для каждого запроса. «Для всякого $n$» истинно не потому, что бесконечная совокупность пройдена, а потому, что для любого запроса конечный ответ гарантирован. Квантор есть схема «по запросу», не объект «вся совокупность».

Утверждение «для всякого $n$» не описывает завершённую совокупность всех чисел и не требует её. Оно есть схема: для любого предъявленного $n$ доказательство может быть построено — конечной цепочкой, своей для каждого $n$. Квантор «для всякого» — обещание ответа на запрос, а не обход наличной бесконечности.

{ Здесь нужна точность относительно формальной стороны. В Rocq утверждение forall n : nat, P n есть зависимый функциональный тип над nat: его обитатель — функция, которая по произвольному входу n : nat возвращает доказательство P n. Поэтому было бы неточно сказать, что квантор вовсе не имеет области: домен у него есть — это тип nat, и nat как тип в Rocq уже задан. Точная формулировка иная: forall n : nat, P n не требует перечисления всех n и не предполагает nat пройденным до конца как завершённую совокупность; он требует единой конструкции — функции, — работающей для произвольного предъявленного n. Различие <<схема против объекта>>, проведённое выше, есть, таким образом, различие между обходом завершённой совокупности и единой процедурой по запросу — а не утверждение, будто у квантора нет домена. Домен nat есть; чего нет — так это требования предъявить nat как пройденную актуальную тотальность. Квантор есть тип функций <<по любому $n$ построить $P(n)$>>, и именно поэтому он совместим с почленным, непройденным-до-конца построением ряда. }

Тем самым возражение § 2.7.2 снято. «Для всякого $n$» не предполагает «всех чисел сразу»: оно совместимо с почленным построением ряда, ибо само есть лишь обещание, что построение дотянется до любого затребованного члена.

Бесконечность как возможность, не как совокупность: $P4${P4}

Сказанное — частный случай общего принципа ToS, и теперь его можно назвать. Это $P4$, выведенный в Главе I.4 из закона $L5$.

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

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

Натуральный ряд бесконечен в этом, и только в этом, смысле. Его построение есть процесс в смысле $P4$: всякая стадия — конечный список различий (§ 2.3), и на всякой стадии налично конечное число совершённых актов. Не существует последней стадии — за всяким совершённым актом можно совершить ещё один (§ 2.5.2), — и потому построение ряда неограниченно продолжаемо. Но «неограниченно продолжаемо» не значит «завершено»: возможность сделать ещё шаг есть всегда, а вот стадии, на которой был бы налично весь ряд, — нет, ибо всякая стадия конечна.

Приложим это к итогам главы. «Реализуемо каждое число» (§ 2.5) читается теперь точно: для любого затребованного числа построение может быть доведено до него — на некоторой конечной стадии оно актуально. «Не все числа сразу» (§ 2.5.4) читается так же точно: нет стадии, на которой был бы налично весь ряд, — ибо всякая стадия по $P4$ конечна. Эти два утверждения не в противоречии, как могло казаться: они суть две стороны одного потенциального понимания бесконечности. Ряд бесконечен как неисчерпаемая возможность счёта, не как исчерпанный итог его.

Стоит уточнить, что именно ToS отрицает, говоря об отсутствии завершённой бесконечности — и в какой форме это отрицание формализовано. ToS не утверждает абсолютно, будто <<совокупности всех натуральных чисел не бывает ни в каком смысле>>. Утверждается точнее: натуральный ряд не есть completed actuality — нет стадии, на которой весь ряд был бы актуально предъявлен. Формально несовместимость завершённой бесконечности с $P4$ разобрана в файле P4CompletedInfinity.v репозитория, и разобрана условно: соответствующая теорема выводит противоречие не из одного лишь существования бесконечного ряда, а из трёх посылок вместе — из предиката завершённого членства (CompletedInfSet, <<всякое $n$ принадлежит $S$>>), из стадийной ограниченности по $P4$ (P4_stage_bounded) и из моста (bridge), переводящего членство в ряду в актуальную предъявленность на конечной стадии. Иными словами: completed infinity противоречит $P4$ при условии моста, связывающего членство с актуальностью на стадии. Это и есть точная форма отрицания: ToS отвергает не квантор <<для всякого $n$>> (он, как показано в § 2.7.3, законен и без завершённой совокупности), а именно совмещение завершённого членства со стадийной актуальностью — то есть представление всего ряда как наличного на некоторой стадии.

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

Что отсюда следует для дальнейшего

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

Прежде всего, она объясняет, отчего натуральный ряд в ToS есть ряд $1,2,3,\dots$ и ничего сверх него. В нём нет «числа $\infty$», нет завершающего члена, нет совокупности-целого, наличной как актуальность над числами. Бесконечность ряда не есть ещё один его объект — она есть свойство построения: его неограниченная продолжаемость. Это прямое следствие $P4$, и оно отделяет ToS от построений, в которых натуральный ряд берётся как completed actuality — как совокупность, актуально предъявленная целиком (§ 1.1).

Далее, потенциальное понимание бесконечности — то самое, что позволило Главе II.1 разобрать запись $0,999\dots$ (§ 1.8). Там $0,999\dots$ было разобрано как процесс — продолжаемая схема приближений, не завершённый объект; и согласие этого с $P4$ было отмечено, но $P4$ ещё не назван. Теперь он назван: $0,999\dots$ как процесс и натуральный ряд как потенциальная бесконечность стоят на одном принципе. Подчеркнём, как и в Главе II.1, точный смысл этого. ToS не отрицает стандартного равенства $0,999\dots =1$ в режиме действительных чисел, где запись по определению означает предел или класс эквивалентности. Речь о различении режимов: сырой процесс приближений, постоянный процесс и класс эквивалентности процессов — разные режимы, и безусловное равенство уместно лишь по переходе к общему режиму. Часть IV развернёт это формально через тип RealProcess (файл ProcessCore.v: RealProcess $:=‘nat‘\to Q$) и отношение process_equiv — эквивалентность процессов по пределу, доказанное отношением эквивалентности и не сводящееся к поточечному равенству. Бесконечность как процесс — общая черта чисел ToS, а не особенность одного спорного случая.

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

Кратность одного

Двойственная природа числа в кардинальном пути

Кардинальный путь построен (§ 2.1–2.7). Прежде чем закрыть главу, стоит вглядеться в одну черту построенного — черту, которая в ходе работы оставалась неявной, а теперь может быть названа.

Число $n$ в кардинальном пути есть список из $n$ совершённых различий (§ 2.4). В этом определении соединены два, казалось бы, противоположных указания. С одной стороны, число $n$ есть множественность: $n$ различий, $n$ совершённых актов, $n$ элементов списка — многое. С другой стороны, число $n$ есть единство: одно число, один отпечаток, одна система-список, взятая как целое. Число кардинального пути двойственно: оно есть многое, собранное в одно.

Двойственность эта не противоречие и не натяжка. Она прямо следует из того, как путь построен. Множественность — оттого, что число есть список нескольких различий (§ 2.2). Единство — оттого, что все эти различия суть повторения одного акта (§ 2.1.2) и собраны в один список как одну систему E/R/R (§ 2.2.4). Многое числа есть многое повторений; единство числа есть единство повторяемого акта и единство собирающего списка. Число есть кратность одного: одно, взятое столько-то раз, и эти разы, собранные обратно в одно.

Разбор E/R/R: число-список как система

{ Разбор E/R/R этого пути глава уже провела — в § 2.2.4, для списка как системы: Rules — правило следования ($L5$); Roles — упорядоченные позиции; Elements — различия. Сведём его теперь в таблицу, добавив доказанные предикаты счёта (§ 2.3–2.4) и потенциальную бесконечность (§ 2.7), и проверим сформированность. Оговорка о статусе: <<система>> здесь — содержательная интерпретация над стандартным списком; формальные предикаты distinctioncount и distinctioncountfromone доказаны (Distinction.v, PrimalityOfOne.v), но онтологическое чтение несёт проза.}

Компонент	Что фиксирует	E/R/R
правило следования ($L5$); рекурсия счёта	конституция списка	Rule
длина = акт подсчёта; distinction_count ($+$ фильтр $1\le n$)	счёт и положительность	Rule
$P4$: ряд потенциально бесконечен	потенциальность	Rule
длина = число; позиции <<первая>>, <<$n$-я>>	роль-количество	Role
различия (повторения одного акта); список	носители (конечны, $P4$)	Element
законы $L1$–$L5$ (здесь $L5$)	универсальный слой	Rule (универс.)

{ Хорошая сформированность. Разметка однозначна: различия — элементы, длина и позиции — роли, правило следования — правило. Соблюдён $P1$: длина считает различия (элементы), а не самоё себя. Диагностика этой главы уже проведена в § 2.2.4 и есть случай общей: список (полная система с правилом следования) против множества (та же система с погашенным правилом следования) — кардинальный путь требует именно списка, ибо счёт несёт следование, которое множество гасит. И граничный случай ровен: пустой список даёт длину нуль — корректный итог подсчёта, не встретившего элементов, а не <<ошибку>> и не <<непроявленность>> (§ 2.3.3). Честная граница: distinctioncountfrom_one есть фильтр положительности ($1\le n$), а не проверка <<совершённости>> актов; индукция — стандартная по nat, не выведенная из различения (§ 2.6).}

Что даёт разбор. Это первый из четырёх путей: число есть роль-количество — длина списка повторённых различий, — и эта же ролевая структура (начало и следование) повторится на уровнях (Глава II.3), битах (Глава II.4) и позициях (Глава II.5), которая и сведёт четыре пути воедино. Кардинальный путь даёт ей первое воплощение и закрепляет двойственность числа — кратность одного (§ 2.8.1): многое повторений, собранное в одну систему-список.

Независимое схождение с давней мыслью

Понимание числа как кратности одного не ново для европейской мысли — и здесь, как и в § 1.5, уместно сопоставление. Сделать его нужно точно: ToS пришла к кратности одного своим путём, из своей деривации (§ 2.1–2.7), и не наследует ничьей традиции. Совпадение, которое будет отмечено, есть схождение независимых путей, а не происхождение ToS из предшественников. И статус этого совпадения нужно назвать прямо: оно — не доказательство и не родословная, а эвристическая поддержка. Что мотив кратности одного возникает в нескольких независимых традициях, повышает правдоподобие того, что собственная деривация ToS попала в нечто, присущее предмету, а не в артефакт своего формализма; но строгого веса доказательства такое схождение не несёт и нести не может.

Лейбниц. В одном ряду с ToS оказывается давнее определение: число есть то, что относится к единице как линия к линии, — множество единиц, единое собрание повторённого одного.³ Это определение берёт число ровно двойственным: единица как то, что повторяется, и число как собранная кратность её повторений. ToS приходит к тому же из своего основания: единица — первый акт (§ 1.2), число — собранная кратность его повторений (§ 2.8.1). Совпадение точное — и тем более показательное, что пути к нему разные: там — определение числа через отношение к единице, здесь — деривация числа из акта различения.

Брауэр. Независимо обнаруживается схождение и с интуиционистским пониманием числа.⁴ В нём натуральное число есть не объект готового множества, а построение — результат мысленного шага, повторённого определённое число раз; и весь числовой ряд есть не завершённая совокупность, а свободно продолжаемое разворачивание этих шагов. ToS, идя своей дорогой, приходит к тому же: число реализуемо построением списка (§ 2.4), а ряд бесконечен лишь потенциально, как продолжаемость построения (§ 2.7). Здесь схождение касается не только кратности одного, но и понимания бесконечности — и снова это схождение независимых путей: интуиционизм исходит из устройства математической интуиции, ToS — из устройства акта различения.

Гуссерль. Ещё одно схождение — с описанием того, как число возникает для сознания: число там есть итог акта собирания — акта, который многое схватывает как одно, не упраздняя многого.⁵ Кратность не стирается в единстве и единство не распадается в кратность — акт собирания держит обе стороны. ToS приходит к тому же составом своего списка: список есть многое различий, собранное в одно как система (§ 2.2.4), — и собирание это есть акт, не готовая данность. И снова дороги независимы: там — описание акта сознания, здесь — деривация структуры списка.

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

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

Итог главы

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

Путь начался с перехода от одного акта к нескольким: «несколько актов» возможно потому, что акт различения повторим, и счёт сам есть деятельность различения (§ 2.1). Деривация повторимого, упорядоченного счёта привела — не выбором, а вынужденно — к списку как форме множественности: множество, лишённое порядка и производное по $M_3$, деривации не отвечает, тогда как список несёт порядок ($L5$) и в разборе E/R/R оказывается полной системой, тогда как множество — той же системой с погашенным правилом следования (§ 2.2). Длина списка различий была определена не как присущее свойство, а как итог акта подсчёта; для пустого списка подсчёт законно даёт результат нуль — граничный итог подсчёта, не встретившего ни одного элемента (§ 2.3). Технический предикат подсчёта был отделён от онтологического предиката счёта от единицы — distinctioncountfrom_one, — для которого нуль не есть счёт, а единица есть первый счёт (§ 2.4). Показано, что реализуемо каждое натуральное число — единица реализуема, и переход от $n$ к $n+1$ сохраняет реализуемость (§ 2.5). Принцип индукции, на который это опёрто, оказался не аксиомой, а словесной записью самого построения: база отвечает первому акту, шаг — повторимости (§ 2.6). И бесконечность ряда, по принципу $P4$, есть бесконечность потенциальная — неограниченная продолжаемость построения, не завершённая совокупность (§ 2.7). Наконец, число построенного пути предстало как кратность одного — двойственность многого повторений и единства повторяемого, — в чём ToS независимо сходится с давней линией мысли (§ 2.8).

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

Но это лишь один из путей. ToS приходит к натуральному ряду не единожды, а четырежды (§ 2.1), и кардинальный путь — только первый. Следующая глава открывает второй — путь иерархический: число как уровень в иерархии, порождаемый не приставлением ещё одного различия, а восхождением по ступеням организации. Тот же натуральный ряд будет получен из иной деривации — из закона $L5$ и порождаемой им структуры уровней. Что один и тот же ряд достижим несколькими независимыми путями — не избыточность, а указание на устойчивость предмета; смысл этого ToS соберёт в Главе II.5.

---

---

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

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

Навигация: ← Глава 1. Первичность единицы · Глава 3. Иерархический путь: число как уровень →

Footnotes

1. Предикат distinctioncount, как и тип Distinction и теоремы о нём (zerodistinctions и далее), определён в файле Distinction.v Rocq-репозитория ToS. Здесь и далее имена файлов репозитория приводятся для справки. ↩

2. Предикат distinctioncountfromone и относящиеся к нему теоремы (firstcountisone, zeronotacount, adddistinction, succisnewdistinction, positivenatisdistinction_count) определены в файле PrimalityOfOne.v Rocq-репозитория ToS. Здесь и далее в главе имена файлов репозитория приводятся для справки. ↩

3. Определение числа через отношение к единице восходит к евклидовой традиции (Начала, книга VII, определения 1–2: единица и число как множество единиц); Лейбниц развивает понимание числа как собрания единиц в ряде работ по основаниям арифметики и комбинаторике. ↩

4. Л. Э. Я. Брауэр развивает понимание натурального числа как мысленного построения и числового ряда как свободно продолжаемого разворачивания в работах по основаниям интуиционистской математики, начиная с диссертации <> (1907). ↩

5. Э. Гуссерль анализирует возникновение понятия числа из акта собирающего схватывания (kollektive Verbindung) в Философии арифметики (Philosophie der Arithmetik, 1891). ↩