Глава 1. Первичность единицы

Часть I построила основную ось Теории Систем: $A=\exists$ как пред-формальный первофакт; Distinction как первый формализуемый след; $L1$–$L5$ как структурные свойства различения и иерархии; $P1$–$P4$ как принципы системного построения; и $E/R/R$ как онтологическую схему системы. Было обозначено и онтологическое ядро тома — мета-мотив процессности и четыре сквозных мотива. Часть II начинает применение этого аппарата. Её предмет — натуральные числа.

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

Стандартная позиция: ноль первичен

Три формы первичности нуля

В стандартной математике нуль занимает первое место в построении натуральных чисел. Это положение проводится по меньшей мере тремя независимыми путями, и стоит рассмотреть каждый, поскольку именно относительно них ToS совершает свой ход.

Аксиоматический путь: Пеано. В аксиоматике Пеано натуральный ряд задаётся базовым элементом и операцией. Базовый элемент — нуль; операция — переход к следующему, последователь. Всякое натуральное число есть либо нуль, либо последователь некоторого натурального числа. В формализации, принятой в Rocq, это записывается индуктивным типом¹

Inductive nat := O | S : nat -> nat.

Здесь O — конструктор без аргументов, и он назван первым. Единица не есть отдельный конструктор: она есть S O — последователь нуля. Двойка есть S (S O), и так далее. В этом построении нуль — исходная точка, а всякое другое число получается из него конечным числом применений последователя. Никакое число не предшествует нулю; нуль не есть последователь, и потому он первое, с чего натуральный ряд начинается.

Теоретико-множественный путь: фон Нейман. В построении натуральных чисел через множества, восходящем к фон Нейману, каждое натуральное число отождествляется с определённым множеством. Нуль есть пустое множество $\varnothing$. Единица есть множество, содержащее пустое: $\{\varnothing \}$. Двойка есть $\{\varnothing ,\{\varnothing \}\}$ — множество, элементами которого служат нуль и единица. В общем виде: следующее число есть множество всех предыдущих.

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

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

Что объединяет три пути

Три пути различны по технике, но согласны в одном: нуль есть точка отсчёта. Он назван первым (Пеано), сопоставлен самому простому объекту (фон Нейман), помещён в начало структуры (категорный путь). Во всех трёх случаях остальные числа определяются через нуль и после него.

Здесь нужна точность. Три пути согласны структурно — натуральный ряд везде задаётся через выделенный начальный (нулевой) элемент и операцию следования, — но онтологически они различны. Только построение фон Неймана действительно теоретико-множественное: там начальный элемент есть пустое множество. Пеано-арифметика и тип nat в Rocq не обязаны опираться на пустое множество: nat — индуктивный тип с нулевым конструктором O, и O здесь есть базовая точка, а не <<ничто>>. Категорный объект натуральных чисел задаётся стрелкой $1\to N$, где $1$ — терминальный объект, тоже не пустой. Поэтому неверно сказать, что все три пути объединены единой теоретико-множественной онтологией <<исходного ничто>>.

Первичность нуля в стандартной математике не есть произвольное соглашение. В теоретико-множественном пути она следует из онтологии пустого множества; в типовом и категорном путях — из выбора базовой точки (нулевого конструктора, терминального объекта) как начала отсчёта. Общее у всех трёх — структурная роль начального элемента, а не одна и та же онтология <<ничто>>.

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

Позиция Теории Систем: единица первична

Первый акт различения есть единица

Исходный объект ToS — не пустое множество, а акт различения. Глава I.2 разобрала его устройство: акт различения полагает положительную сторону и отрицательную сторону, и эти две стороны взаимно исключены и совместно исчерпывающи. Акт не существует без обеих сторон, и стороны не существуют без акта.

Зададимся вопросом, который для теоретико-множественной онтологии не имеет смысла, а для онтологии ToS — имеет: сколько актов различения совершено, когда совершён первый? Ответ прям: один. Не одна сторона — сторон две. Не один объект — объект ещё не рассматривается, рассматривается акт. Совершён один акт — и это «один» есть первое число, появляющееся в системе.

Существенно, что это «один» не есть результат счёта. Счёт — процесс, который сам разбирается ниже, в § 1.6 и в Главе II.2. До всякого счёта — до того, как появится список, длина, кратность, — есть факт совершения акта. Этот факт уже имеет число: единицу. Единица есть кардинальность совершённого — мера того, что акт произведён, взятая прежде, чем эта мера будет как-либо вычислена.

В репозитории это фиксируется простейшим из возможных определений. Каждому акту различения — каждому объекту типа Distinction — сопоставляется число, и это число есть единица:

Definition one_from_distinction (D : Distinction) : nat := 1.
 
Theorem one_is_first_from_existence :
  forall D : Distinction, one_from_distinction D = 1%nat.
Proof. reflexivity. Qed.

{

Определение намеренно тривиально, и его тривиальность содержательна. Оно не вычисляет число акта и не доказывает первичность единицы в строгом смысле — оно регистрирует принятую интерпретацию: решение читать каждый акт различения как одну единицу. Теорема oneisfirstfromexistence доказывается одним словом reflexivity — то есть машинно проверяет это вычисление: в данной формальной интерпретации каждый объект Distinction, безотносительно к тому, что именно он различает, получает числовой отпечаток 1. Сама же онтологическая нагрузка — утверждение <<акт различения есть единица>> — остаётся содержательным тезисом главы, а не следствием кода: код регистрирует выбранное прочтение и проверяет его непротиворечивость, но обосновывается это прочтение онтологией акта различения (§ 1.2), не теоремой. Здесь ToS делает явным то, что в стандартном построении остаётся непроговорённым: прежде чем считать объекты, нужно иметь акт, которым они различены, — и этот акт ToS читает как единицу. }

Единица как акт, а не как множество из одного

Позиция ToS радикальнее, чем кажется при первом чтении, и стоит отделить её от близкого, но иного утверждения.

Стандартная математика тоже располагает единицей и тоже умеет получать её рано. В построении фон Неймана единица есть $\{\varnothing \}$ — множество, содержащее пустое. Это множество из одного элемента. Но получено оно после нуля и через нуль: чтобы образовать $\{\varnothing \}$, нужно уже иметь $\varnothing$. Единица здесь вторична — она есть «множество, в котором один элемент», и этот «один» отсчитан относительно пустоты.

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

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

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

Почему именно единица, а не нуль: структурная асимметрия

Сказанного достаточно, чтобы утверждать: единица в ToS первична. Но остаётся вопрос более тонкий. Акт различения полагает две стороны — положительную и отрицательную. Не симметричны ли они? И если симметричны — то почему первое число есть единица (одна сторона маркирована), а не, скажем, двойка (две стороны), и почему нуль оказывается позади единицы, а не наравне с ней?

Ответ в том, что две стороны акта различения не симметричны. Их асимметрия — структурная. Файл репозитория AsymmetricDistinction.v фиксирует её формально; разберём её точно.

Отрицательное определяется через положительное. Когда из пропозиции $P$ строится различие, его положительная сторона есть сама $P$, а отрицательная сторона есть $\neg P$:

Theorem positive_is_given : forall P : Prop,
  positive (distinction_of P) = P.
Proof. reflexivity. Qed.
 
Theorem negative_depends_on_positive : forall P : Prop,
  negative (distinction_of P) = (~P).
Proof. reflexivity. Qed.

Положительная сторона дана: она есть $P$, и определение к ней прямое. Отрицательная сторона определена через положительную: она есть $\neg P$ — результат логической операции, применённой к $P$. Чтобы задать отрицательное, нужно уже иметь положительное, к которому применяется отрицание; обратное неверно.

Здесь требуется точность, иначе утверждение легко исказить. Асимметрия не временная. Положительная сторона не возникает <<раньше во времени>>, чем отрицательная: обе возникают в одном и том же акте различения, одновременно (Глава I.2: со-определение сторон). Асимметрия определительная: положительное определяется прямо, отрицательное — через положительное. И определительная зависимость сильнее зависимости по со-определению. Положительное и отрицательное равно нуждаются друг в друге, чтобы быть определёнными как стороны (без отличия от чего $P$ не есть различённое $P$); но дано — одно, а выведено отрицанием — другое.

Маркированная сторона. Эту определительную первичность ToS называет маркированностью. Положительная сторона — маркированная: та, через которую определяется другая. Отрицательная — немаркированная. И вот формальный мост от маркированности к числу:

Definition mark   (D : Distinction) (h : positive D) : nat := 1.
Definition unmark (D : Distinction) (h : negative D) : nat := 0.
 
Theorem marked_greater_than_unmarked : forall D p n,
  (unmark D n < mark D p)%nat.
Proof. intros. unfold mark, unmark. lia. Qed.

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

Техническая оговорка о статусе mark и unmark. Прочитать этот формальный мост нужно аккуратно. Функции mark и unmark принимают вторым аргументом не сторону как роль, а доказательство — объект типа positive D или negative D. Для одного и того же различия D доказательства обеих сторон одновременно невозможны: поле exclusive записи Distinction как раз и запрещает positive D /\ negative D. Поэтому теорема markedgreaterthan_unmarked в её буквальной форме — forall D p n, unmark D n < mark D p — сравнивает не две реально совместимые стороны одного различия, а два числовых значения при гипотетически данных доказательствах. Это proof-level конструкция: формально она слабее, чем role-level утверждение <<маркированной роли соответствует $1$, немаркированной — $0$>>.

Точнее это последнее утверждение формализуется не через доказательства, а через роль-сторону — например, так:

Inductive DistinctionSide := Marked | Unmarked.
 
Definition side_value (s : DistinctionSide) : nat :=
  match s with Marked => 1 | Unmarked => 0 end.
 
Theorem marked_role_gt_unmarked_role :
  side_value Unmarked < side_value Marked.
Proof. simpl. lia. Qed.

Здесь сравниваются именно две роли — Marked и Unmarked — как значения одного перечислимого типа, и неравенство $0<1$ выражает приоритет маркированной роли без обращения к доказательствам сторон. mark / unmark при этом сохраняют смысл как proof-level интерпретация того же приоритета: они показывают, какое число получает сторона, когда она предъявлена доказательством. Содержательный аргумент главы — единица метит маркированную (данную) сторону, нуль немаркированную (выведенную) — опирается на role-level различение; mark / unmark суть его proof-level тень.³

Здесь к определительной асимметрии добавляется вторая, более глубокая. Глава I.7 объявила первый сквозной мотив тома — $M_1$, позитивную онтологию: всё онтологически существующее существует позитивно; небытие не есть особый род бытия, существующий наряду с бытием; то, чего нет, не есть особый предмет «отсутствие», а просто не есть. Мотив $M_1$ прямо касается распределения единицы и нуля по сторонам акта. Положительная сторона есть наличие — то, что актом положено. Отрицательная сторона есть «не это»; она вполне реальна как сторона акта (Глава I.2: со-определение сторон), но она не есть самостоятельное наличие, существующее отдельно и наравне с положительным. Единица метит то, что есть; нуль метит то, чего нет. И по $M_1$ первичным может быть только наличие: то, чего нет, не способно быть положенным первым, потому что быть положенным — значит быть наличием. Асимметрия маркированного и немаркированного, таким образом, не только определительная (одно дано, другое выведено), но и онтологическая (одно есть наличие, другое метит его отсутствие). Обе асимметрии указывают в одну сторону: первична единица.

Отсюда же — предупреждение, которое будет существенно в § 1.3. Если нуль метит отсутствие, а отсутствие по $M_1$ не есть особый предмет, то нуль не может быть введён в ToS как объект-наряду-с-числами, формализующий некую сущность «пустоту». Чем он тогда вводится — разбирает следующий после структурной асимметрии раздел; здесь достаточно зафиксировать, что $M_1$ запрещает первичный нуль не как меньшее из чисел, а как онтологическую фигуру.

Различие нельзя обратить. Можно было бы возразить: маркировка положительной стороны — не есть ли это произвол наблюдателя, который с тем же успехом мог бы маркировать отрицательную? Файл AsymmetricDistinction.v отвечает на это формально. Определена операция swap_distinction — перестановка сторон местами; и доказано, что перестановка даёт другое различие, не то же самое:

Theorem distinction_asymmetric : forall P : Prop,
  positive (distinction_of P)
    <> positive (swap_distinction (distinction_of P)).
Proof. (* ... uses classic ... *) Qed.

Перестановка сторон есть переход к различию $\neg P$ вместо $P$ — к другому акту. Стороны не взаимозаменяемы: различие $P$ и различие $\neg P$ — это две разные записи, а не одна, прочитанная двумя способами.⁴ Асимметрия, таким образом, присуща акту, а не наложена на него извне. Маркирована именно положительная сторона — потому что определительная первичность есть свойство устройства различения, а не выбор того, кто на различие смотрит.

«До» и «после»: первый числовой отпечаток

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

Из асимметрии сторон акт различения получает ориентацию — направление от маркированного к немаркированному. Файл AsymmetricDistinction.v вводит для сторон, взятых в их ориентации, имена before и after:

Definition before (D : Distinction) : Prop := positive D.
Definition after  (D : Distinction) : Prop := negative D.
 
Theorem before_after_exclusive : forall D : Distinction,
  ~ (before D /\ after D).
Theorem before_after_exhaustive : forall D : Distinction,
  before D \/ after D.

«До» и «после» суть положительная и отрицательная стороны, взятые со своей ориентацией; они взаимно исключены ($L2$) и совместно исчерпывающи ($L3$) — ровно как стороны акта, которыми они и являются. Один акт различения порождает «до» и «после» — и это порождение есть единица: один акт, одна различённая пара со своим направлением.

Здесь — зерно всей конструкции натурального ряда, к которой Часть II идёт. Один акт различения даёт «до» и «после». Повторение акта — ещё одно различение, теперь уже между «совершённым прежде» и «совершаемым сейчас», — даёт «до — после — после». Формальный отпечаток такого повторения и есть натуральное число; разворачиванию этого отпечатка посвящены Главы II.2–II.5. Единица стоит в начале не как наименьшее из чисел и не как «множество из одного», а как первый акт, от которого повторение ведёт счёт.

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

Что есть ноль

Постановка задачи

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

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

Задача тоньше, чем кажется, и тонкость создаёт именно $M_1$. Самый простой ответ — «нуль есть пустота, отсутствие как таковое» — закрыт: он вернул бы нас к онтологии, где «отсутствие» есть предмет наряду с наличными предметами, а такой онтологии ToS не держит. Значит, нуль нужно ввести так, чтобы он не оказался именем для предмета-пустоты. Как именно — разбирается ниже.

Ноль как граница, а не как предмет

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

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

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

Это и есть статус, согласованный с $M_1$. Нуль вводится не как объект-наряду-с-числами и не как имя пустоты. Он вводится как граничная отметка: предельное значение, относительно которого ряд совершённых различений отсчитывается, но которое само не есть совершённое различение. В репозитории файл PrimalityOfOne.v фиксирует это так:

Definition zero_from_no_distinction : nat := 0.
 
Theorem zero_is_absence :
  zero_from_no_distinction = 0%nat.

{

Здесь нужна точность в прочтении кода. zerofromnodistinction есть числовое значение 0, сопоставленное ситуации <<различений не предъявлено>>; теорема zeroisabsence проверяет, что это значение действительно есть 0. Существенно, чего этот код не утверждает: он не говорит, что во всём универсуме не существует ни одного объекта Distinction. Такое утверждение было бы попросту ложным — тип Distinction населён (например, distinction_of True существует, и файл Distinction.v это фиксирует леммами onedistinctionexists, twodistinctions_exist). Нуль в ToS означает не отсутствие различений вообще, а отсутствие предъявленных различений в данном счётном контексте — в данном списке, на данной стадии. Иначе говоря: нуль не означает, что в мире не совершено ни одного акта различения; он означает, что в рассматриваемом списке или на рассматриваемой стадии не предъявлено ни одного. Числовое значение 0 сопоставлено именно этой локальной границе. }

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

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

Ноль не есть счёт различений

Граничный статус нуля имеет точное формальное следствие, и оно важно для всей Части II: нуль не входит в счёт различений. (В разборе E/R/R это роль-граница, не предмет; § 1.8.7.) Разберём это аккуратно, потому что здесь репозиторий содержит тонкость, которую легко пропустить.

В файле Distinction.v определён предикат, сопоставляющий числу возможность быть реализованным списком различий:

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

Этот предикат технический: он спрашивает лишь, существует ли список различий заданной длины. И для n = 0 ответ положителен — пустой список имеет длину нуль:

Theorem zero_distinctions : distinction_count 0.
Proof. exists nil. reflexivity. Qed.

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

Чтобы выразить счёт актов — счёт в том онтологическом смысле, который держит Часть II, — нужен предикат строже. Файл PrimalityOfOne.v его и вводит:

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

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

Theorem zero_not_a_count : ~ distinction_count_from_one 0.
Proof.
  intros [Ds [_ H]]. inversion H.
Qed.
 
Theorem first_count_is_one : distinction_count_from_one 1.
Proof.
  exists (cons (distinction_of True) nil).
  split. reflexivity. apply le_n.
Qed.

zeronota_count утверждает: нуль не есть счёт различений. Доказательство коротко — условие $1\le 0$ ложно, и inversion это закрывает, — но содержательно оно говорит существенное. Счёт различений, взятый как счёт совершённых актов, начинается с единицы; нуль в него не попадает. А first_count _is_one показывает, с чего он начинается: первый счёт есть единица, и ему отвечает список из одного различия.

Зачем два предиката

Может возникнуть вопрос: зачем репозиторий держит два предиката счёта, distinctioncount и distinctioncountfromone, если они различаются лишь судьбой нуля? Не избыточность ли это? Ответ — нет, и он проясняет устройство всей конструкции.

Два предиката отвечают двум разным вопросам, и оба вопроса законны.

distinction_count отвечает на вопрос технический: какова длина данного списка различий? Длина есть характеристика списка как структуры данных, и пустой список — полноправная структура с длиной нуль. Этот предикат нужен везде, где речь идёт о списках как таковых: о длинах, индексах, конкатенациях. Он не несёт онтологической нагрузки счёта актов; он работает на «слое синтаксиса» в смысле, который Глава I.6 ввела для слоёв формальной работы.

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

Разделение двух предикатов есть формальный отпечаток разделения двух слоёв. На слое синтаксиса нуль есть законная длина пустого списка — здесь работает distinctioncount. На слое онтологии нуль не есть счёт совершённых актов — здесь работает distinctioncountfromone, и он начинается с единицы.

Существенно, что это разделение не есть конфликт. Два предиката не противоречат друг другу — они говорят о разном. Утверждение distinctioncount 0 истинно (длина пустого списка есть нуль) и утверждение $\neg$ distinctioncountfromone 0 истинно (нуль не есть счёт совершённых актов) совместимы без всякого напряжения: первое — о длине структуры, второе — о числе актов. Конфликт возник бы лишь при смешении слоёв — если бы техническую длину пустого списка прочитали как онтологическое утверждение «совершено нуль актов различения». ToS этого смешения не допускает, и два предиката суть формальное средство его не допускать.

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

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

Режим	Что такое нуль	Где это работает
Синтаксис nat	конструктор O, базовая точка типа	стандартный тип nat
Список	длина пустого списка	предикат distinction_count $0$
Онтология ToS	граница ряда совершённых актов, отсутствие предъявленного	не входит в distinction_count_from_one

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

Что нуль наследует от единицы

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

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

Здесь видна полная инверсия относительно стандартной картины, описанной в § 1.1. Там нуль первичен, а единица производна: единица есть S O, последователь нуля, — она определена через нуль. В ToS порядок обоснования обратный: единица первична как первый акт, а нуль производен как граница ряда, который акты образуют. Нуль определяется через единицу — через ряд, началом которого единица служит, — а не единица через нуль.

В стандартной картине единица есть последователь нуля. В ToS нуль есть граница ряда, началом которого служит единица. Порядок обоснования инвертирован: производно не то, что меньше, а то, что определяется через другое.

Эта инверсия порядка обоснования — не порядка величин — есть, по существу, главный тезис главы. Следующий раздел (§ 1.4) разбирает, как она уживается с тем, что в типе nat конструктор O всё-таки стоит синтаксически первым; раздел показывает, что синтаксический порядок и порядок обоснования суть разные вещи и что их расхождение не есть противоречие.

Онтологический порядок против синтаксического: совместимость с nat

Возражение от устройства типа nat

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

ToS формализована в Rocq, и натуральные числа в Rocq суть тип nat стандартной библиотеки. Его определение известно (§ 1.1):

Inductive nat := O | S : nat -> nat.

Здесь O — конструктор без аргументов — назван первым. Единица не есть отдельный конструктор: она есть S O. Синтаксически нуль предшествует единице: чтобы записать единицу, нужно применить S к O, то есть нуль уже должен быть под рукой.

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

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

Почему ToS не переопределяет nat

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

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

Изоморфизм всё равно неизбежен. Допустим, ToS определила бы свой тип — назовём его условно «тип с базовой единицей». Каким бы он ни был, он оказался бы изоморфен nat: дискретный, с начальным элементом и оператором следования, он не может не быть изоморфен стандартному натуральному ряду — это будет показано в Главе II.3 на примере типа Level. Изоморфные типы несут одну и ту же математику. Значит, переопределение nat не дало бы нового математического содержания — оно дало бы тот же nat под другим именем и ценой потери совместимости. Платить такую цену за переименование неразумно.

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

Два порядка

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

Синтаксический порядок конструкторов. В индуктивном типе nat конструктор O назван первым, S — вторым. Это синтаксический порядок: порядок, в котором конструкторы перечислены в определении типа, и порядок, в котором значения типа строятся. Чтобы построить S O, нужно сперва иметь O. В этом смысле — в смысле построения терма — нуль предшествует единице.

Онтологический порядок обоснования. Но есть и другой порядок — порядок обоснования: что через что получает свой смысл. Глава I.6, разбирая слои формальной работы, уже провела это различение для общего случая; здесь оно прилагается к nat. В порядке обоснования первично то, что несёт смысл самостоятельно, а производно то, что получает смысл через другое. И в этом порядке, как показали § 1.2 и § 1.3, первична единица: она есть отпечаток первого акта различения, несущий смысл сам; нуль же есть граница ряда совершённых различений, получающая смысл через этот ряд.

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

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

В репозитории оба порядка присутствуют явно, и их различённость зафиксирована формально. Файл AsymmetricDistinction.v определяет порядок различения — порядок, в котором маркированная сторона идёт прежде немаркированной:

Definition distinction_order : nat * nat := (1, 0).
 
Theorem one_precedes_zero_in_distinction :
  fst distinction_order = 1 /\ snd distinction_order = 0.
Proof. split; reflexivity. Qed.

distinction_order есть пара $(1,0)$: единица на первом месте, нуль на втором. Это — онтологический порядок, порядок обоснования, записанный как объект. Он сосуществует со стандартным числовым порядком $0<1$, в котором нуль меньше единицы и в этом смысле <<раньше>>.

Файл PrimalityOfOne.v фиксирует ту же двойственность — но в иной форме, и форму эту нужно привести точно, чтобы не приписать коду большего, чем в нём есть. В PrimalityOfOne.v записано:

Definition tos_first   := 1%nat.
Definition tos_absence := 0%nat.
 
Theorem tos_ordering : (tos_absence < tos_first)%nat.
Proof. unfold tos_absence, tos_first. lia. Qed.
 
Theorem orderings_dual :
  (tos_absence < tos_first)%nat /\ (0 < 1)%nat.
Proof. unfold tos_absence, tos_first. split; lia. Qed.

Прочтём это аккуратно. tosfirst есть 1, tosabsence есть 0; теорема tosordering утверждает неравенство tosabsence < tosfirst, то есть — поскольку tosabsence есть 0, а tosfirst есть 1, — по существу $0<1$. Теорема orderingsdual в этом файле, строго говоря, не фиксирует две противоположные пары: обе её конъюнкты после раскрытия определений сводятся к одному и тому же неравенству $0<1$. Поэтому формальная запись двойственности двух порядков как пары $(1,0)$ против пары $(0,1)$ содержится именно в AsymmetricDistinction.v — в distinctionorder и oneprecedeszeroindistinction, — а PrimalityOfOne.v регистрирует ту же мысль в более слабой форме: числовой порядок $0<1$ налицо, и онтологическое имя начала (tosfirst) сопоставлено единице, а не нулю.⁵

Содержательно вывод от этого не меняется. В системе присутствуют два порядка: числовой порядок по величине, в котором $0<1$, и онтологический порядок обоснования, в котором единица первична (пара $(1,0)$ в distinction_order). ToS не отменяет числовой порядок $0<1$: нуль по величине меньше единицы, и арифметика этим пользуется. ToS лишь добавляет к нему второй порядок — обоснования, — в котором единица первична, и настаивает, что смешивать эти два порядка нельзя.

Семантический сдвиг, а не переопределение

Теперь возражение из § 1.4.1 получает полный ответ.

ToS пользуется стандартным типом nat. Конструктор O в нём синтаксически первичен — и ToS этого не меняет. Но онтологическое чтение типа ToS задаёт своё: O интерпретируется не как первичная сущность, а как граничная отметка (§ 1.3); S O — как отпечаток первого совершённого акта, первичный в порядке обоснования; S n — как «после $n$ совершённых актов совершён ещё один». Тип взят стандартный; смысл, которым он наделён, задан ToS.

Это и есть семантический сдвиг: не переопределение типа, а переопределение его интерпретации. Файл PrimalityOfOne.v проводит этот сдвиг не через новый индуктивный тип, а через определения и теоремы, фиксирующие чтение стандартного nat — tosfirst, отмечающее единицу как первую распознаваемую величину; tosabsence, читающее нуль как границу; tos_ordering, задающее порядок обоснования. Синтаксис Rocq остаётся нетронутым; меняется семантический слой.

ToS не переопределяет nat — она его переинтерпретирует. Тип остаётся стандартным; вся арифметика Rocq сохраняется. Меняется онтологическое чтение: O — граница, S O — первый акт, и порядок обоснования идёт от единицы. Синтаксический порядок и порядок обоснования различены, и их расхождение есть содержание инверсии, а не препятствие ей.

Этот ход — работа на стандартном синтаксисе с нестандартной семантикой — не есть уловка и не есть частная хитрость настоящей главы. Он повторится в Части II ещё дважды. Глава II.3 возьмёт тип Level, синтаксически тождественный nat, и наделит его иной интерпретацией — иерархической. Глава II.5, подводя итог, сформулирует общий принцип: один и тот же формальный объект допускает несколько онтологических чтений, и ToS последовательно этим пользуется.⁶ Настоящий раздел дал первый и простейший случай этого приёма; и он же снял возражение, с которого начался, — устройство nat не опровергает первичности единицы, потому что говорит о другом порядке.

Историческая традиция: единица как принцип

Зачем здесь история

Инверсия, проведённая в § 1.2–1.4, может на первый взгляд показаться нововведением ToS — технической особенностью одной формальной системы. Настоящий раздел показывает, что это не так. ToS приходит к первичности единицы независимо — из собственной метафизики ($A=\exists$) и собственной онтологии акта различения, не опираясь ни на какую предшествующую традицию. Но к той же первичности — к интуиции, что единица есть начало, а нуль производен или вовсе отсутствует, — независимо приходила европейская мысль о числе на всём своём протяжении, задолго до всякой формализации. Настоящий раздел эти независимые подходы сопоставляет.

Подчеркнём с самого начала, чтобы не было недоразумения относительно жанра раздела: ToS не наследует чужих учений о числе, не заимствует и не продолжает чужих линий мысли. Её путь самостоятелен и выведен в § 1.2–1.4 из устройства акта различения. Историческая часть здесь — не родословная и не апелляция к предшественникам, а сравнение: сопоставление независимо построенной позиции ToS с позициями, к которым прежняя мысль приходила своими путями.

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

Пифагорейская Монада

Самое раннее и самое отчётливое утверждение первичности единицы — пифагорейское. Для пифагорейцев единица — Монада (monas) — была не одним из чисел, а началом числа: тем, из чего числа порождаются и без чего их нет.⁸ Монада не есть «первое число» в ряду; она есть принцип ряда, его источник.

Для настоящей главы существенны две черты этого учения.

Первая: у пифагорейцев нуля как числа не было вовсе. И это не пробел их арифметики, а следствие их онтологии. Число для них есть нечто — определённая множественность, сосчитанная кратность. «Ничто» числом быть не может, ибо числу нечего было бы сосчитать. Отсутствие нуля у пифагорейцев — прямое выражение позиции, которую ToS формулирует через мотив $M_1$: считается наличное, а отсутствие не есть особый предмет счёта.

Вторая: Монада у пифагорейцев порождающа. Числа не лежат готовым набором — они происходят из единицы. Двойка есть первое отступление от единства, и далее ряд разворачивается как порождение. Эта порождающая роль единицы близка к тому, что ToS выразит в Главах II.2–II.5: натуральный ряд не дан, а строится повторением первичного — и первичное есть единица.

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

Неоплатоническое Единое: Плотин и Прокл

Неоплатонизм довёл интуицию первичности единства до предела. У Плотина Единое (to hen) стоит выше самого Бытия: оно есть источник, из которого Бытие исходит, и потому оно прежде всякой определённости, всякой множественности, всякого «есть».⁹ Всё, что есть, есть после Единого и через него.

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

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

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

Фреге: число как свойство понятия

С пифагорейцами и неоплатониками ToS роднит интуиция; с Фреге — нечто более точное: способ определять число, при котором единица и нуль получают свои места не по соглашению, а по существу.

Фреге определил число как свойство понятия¹⁰: число есть характеристика не вещей, а понятия — оно указывает, скольким предметам понятие присуще. Понятию «спутник Земли» присуще число один; понятию «планета Солнечной системы» присуще другое число; и так далее. Число приписывается понятию, через то, что под понятие подпадает.

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

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

Нулю у Фреге отвечает понятие, под которое не подпадает ничто. И — здесь точка, существенная для ToS, — Фреге задаёт такое понятие не как «пустоту вообще», а вполне определённо: понятие «предмет, не тождественный самому себе», то есть понятие $x\ne x$. Под него не подпадает ни один предмет, потому что всякий предмет себе тождествен ($L1$); и число этого понятия есть нуль.

Это определение нуля у Фреге согласуется с ToS точнее, чем может показаться. Нуль здесь возникает не как первичная сущность, а как число логически невозможного понятия — понятия, прямо противоречащего закону тождества. Нуль производен: чтобы его получить, нужно уже располагать законом $L1$ и построить понятие, этот закон нарушающее. Единица же опирается на простое наличие предмета. У Фреге, как и в ToS, единица стоит ближе к наличию, нуль — дальше; и нуль определяется через логическую конструкцию, а не дан прямо.¹¹

Кантор: единица как принцип сборки

Георг Кантор — создатель теории множеств, той самой теоретико-множественной онтологии, относительно которой ToS в § 1.1 заявила своё расхождение.¹² Тем показательнее, что и у Кантора единица сохраняет особый статус — статус принципа, а не рядового элемента.

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

ToS расходится с Кантором в главном — в вопросе о завершённой бесконечности, о множестве как готовом объекте; это расхождение разбирается далее в Части II и развёрнуто в Главе II.5. Но в роли единицы расхождения нет. И у Кантора единица не есть просто наименьшее из чисел — она есть то, чем счёт ведётся и чем множественное сводится к одному. Даже в теоретико-множественной рамке, где нуль первичен синтаксически (как $\varnothing$), единица удерживает функцию принципа. Это показывает, что первичность единицы как принципа не противоречит даже той онтологии, с которой ToS спорит по другим пунктам: спор идёт о бесконечности и о множестве, а не о роли единицы.

Спенсер-Браун: первое различение

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

Джордж Спенсер-Браун в Laws of Form¹³ начинает построение всей логики с единственного указания: проведи различение. Первый акт — проведение различения — не предполагает ничего прежде себя; он есть начало, из которого разворачивается всё остальное. Вся книга строится как развёртывание следствий одного первичного жеста.

Сходство с ToS здесь особенно отчётливо — не аналогия, а совпадение самой постановки. Это не значит, что одно происходит из другого: Глава I.2 уже отметила Спенсера-Брауна среди сходящихся свидетельств о структуре акта различения — именно как независимое свидетельство, не как источник. Для настоящей главы существенно числовое следствие его исходного жеста. Первое различение — одно. Не нуль различений (с нуля у Спенсера-Брауна ничего не начинается — «непроведённое различение» не есть начало, а есть отсутствие начала) и не сразу многое — а одно. Счёт у него, как и в ToS, начинается не с пустоты, а с первого совершённого жеста, и этот первый жест есть единица.

Сопоставлять ToS с Laws of Form как с предшественником, чьё дело ToS продолжает, было бы неверно: ToS не продолжает ничьей линии. Сходство здесь иного рода. Спенсер-Браун своим путём пришёл к тому, что построение начинается с одного первичного различения; ToS своим путём — к записи Distinction и к единице как числовому отпечатку первого акта, разворачиваемому в Главах II.2–II.5 в полную конструкцию натурального ряда. Две постройки независимы; то, что они сходятся в исходной точке, и есть содержание сравнения.

Что даёт это схождение

Шесть свидетельств — пифагорейская Монада, неоплатоническое Единое, Прокл о математике, Фреге о числе понятия, Кантор о единице сборки, Спенсер-Браун о первом различении — принадлежат разным эпохам, разным философским рамкам, во многом несовместимым между собой. Пифагореец и Фреге не согласились бы почти ни в чём; Кантор и ToS расходятся в самом понятии бесконечного. Тем весомее то, в чём они сходятся: единица первична как принцип — как начало, источник, мера, первый акт, — а нуль, где он вообще есть, поздний и производный.

Первичность единицы, к которой ToS приходит независимо из устройства акта различения, оказывается не нововведением, а позицией, с которой совпадает устойчивая интуиция европейской мысли о числе — от пифагорейцев до Спенсера-Брауна. Первичность нуля — исторически поздняя позиция, закрепившаяся вместе с теоретико-множественным основанием. Совпадение независимо построенной позиции ToS с давней и многократно засвидетельствованной интуицией есть указание на то, что инверсия отвечает чему-то в самом предмете.

Здесь нужно предупредить понятное недоразумение. Сказанное не есть довод «истинно, потому что древнее». Историческая распространённость интуиции сама по себе ничего не доказывает — довод в пользу первичности единицы дан в § 1.2–1.4 и опирается на устройство акта различения, а не на чей-либо авторитет. Сравнение свидетельств выполняет иную, более скромную работу: оно показывает, что инверсия ToS не произвольна — что независимо построенная позиция совпала с тем, что мыслящие о числе замечали неоднократно и порознь, задолго до всякой формализации. Обоснование инверсии даёт § 1.2–1.4; сравнение свидетельствует, что обоснованная позиция отвечает устойчивой черте самого предмета, а не особенности одного формализма.

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

Счёт как присутствие, а не наращивание от нуля

Две картины счёта

Разделы § 1.2–1.5 установили инверсию: единица первична, нуль производен. До сих пор это касалось чисел — того, что стоит в начале числового ряда. Настоящий раздел показывает, что инверсия касается и счёта — самого действия, которым числа применяются. Если меняется, что первично, меняется и то, чем счёт является.

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

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

Эта картина согласована с теоретико-множественным построением (§ 1.1) и с синтаксическим порядком nat (§ 1.4): начинаем с O, применяем S, накапливаем. Она привычна; школьный счёт «ноль, один, два, три» закрепляет именно её.

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

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

Что меняется в интуиции

Различие двух картин стоит сделать ощутимым на простом примере.

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

Где в картине присутствия нуль? Он появляется лишь в одном случае — когда нет повода для счёта. «На руке нуль пальцев» означает не «счёт прошёл через нуль и остановился», а «не нашлось ни одного вот этого пальца, который счёт мог бы отметить». Нуль есть отсутствие повода, — ровно граница ряда, как установлено в § 1.3, а не точка, сквозь которую счёт проходит по пути к числам.

В картине наращивания счёт проходит через нуль на пути от пустоты к числу. В картине присутствия счёт начинается с первого различения; нуль не есть проходимая точка, а есть отсутствие повода считать. Считать — значит не накапливать от пустоты, а фиксировать меру наличного.

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

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

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

Согласие с мотивом $M_1${M1}. Картина наращивания неявно придаёт нулю содержательную роль: нуль есть старт, исходное состояние, через которое счёт проходит. Это наделяет «пустоту» позитивной функцией — функцией начала. Но мотив $M_1$ (§ 1.2.3) запрещает именно это: отсутствие не есть особый предмет, способный быть началом. Картина присутствия согласована с $M_1$: началом счёта служит первое наличие — первое совершённое различение, — а не пустота. Считается наличное; пустота не есть то, от чего считают, а лишь имя ситуации, когда считать нечего.

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

Согласие с предикатом счёта. Наконец, картина присутствия — это прямое прочтение предиката distinctioncountfromone (§ 1.3.3). Этот предикат говорит: число $n$ есть в системе постольку, поскольку существует список из $n$ совершённых различий. Он не описывает накопления от нуля — он регистрирует наличие совершённых актов и их число. «Сосчитать» в смысле этого предиката есть в точности «установить, для какого $n$ налицо список из $n$ различений». Картина присутствия — словесное выражение того, что предикат distinctioncountfromone выражает формально.

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

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

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

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

Прежде чем к этому перейти, главе остаётся рассмотреть ещё два предмета, без которых первичность единицы понята не до конца. Первый — делимость единицы: можно ли единицу разделить, и что значит, что нечто разделено (§ 1.7). Второй — запись $0,999\dots =1$, на которой инверсия и операциональная природа делимости проверяются на конкретном и спорном случае: эта запись без указания режима скрывает переход типа — от процесса приближений к его пределу (§ 1.8). К ним глава теперь и переходит.

Делимость как акт

Зачем главе о единице вопрос делимости

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

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

Ответ ToS на этот вопрос даёт не новое учение, а применение уже установленного. Глава I.7 объявила второй сквозной мотив тома — $M_2$, операциональную делимость. Настоящий раздел прилагает $M_2$ к единице. Поэтому он не вводит мотив заново и не повторяет его обоснования — он показывает, что делимость единицы есть частный случай $M_2$, и прослеживает следствия.

Делимость есть совершённое различение

Начать нужно с того, чем делимость является в ToS — потому что здесь ToS расходится с привычным словоупотреблением, и расхождение существенно.

В привычной картине делимость есть свойство объекта. Объект либо делим (его можно разделить на части), либо неделим (нельзя), и это свойство присуще ему само по себе, безотносительно к чему-либо. Спрашивая «делим ли объект?», в этой картине спрашивают о его внутренней природе.

ToS отвечает иначе. Делимость не есть свойство, присущее объекту само по себе. Делимость есть совершённое различение. Объект делим постольку, поскольку внутри него совершён акт различения, разложивший его на стороны. Если такой акт совершён — если относительно $X$ проведено различение, давшее, скажем, $X=⟨A,B⟩$, — то $X$ делим, и делим на $A$ и $B$. Если такой акт не совершён, то $X$ не разложен ни на что — он атомарен.

Сдвиг здесь тот же, что проходит через всю главу: от субстанции к акту. «Делим» в ToS не описывает скрытое устройство объекта, ожидающее обнаружения. «Делим» означает: акт разложения уже совершён. Делимость есть не предрасположенность, а событие — проведённое различение. И как всякое различение в ToS, оно совершается относительно некоторого уровня рассмотрения, на котором проведено (Глава I.4, иерархия уровней $P1$).

Это в точности мотив $M_2$, приложенный к делимости: атомарность относительна, неделимость указывает уровень, на котором объект не разложен, а не абсолютное свойство объекта. ToS не постулирует этот взгляд заново для единицы — она распознаёт в делимости единицы случай $M_2$.

Атом как состояние, а не природа

У операциональной делимости есть прямое следствие для понятия атома, и его стоит проговорить отдельно, потому что оно меняет смысл слова.

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

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

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

Спор атомизма и непрерывности

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

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

ToS расходится с обеими в этой общей предпосылке. Делимость не есть присущее свойство — она есть совершённое различение (§ 1.7.2). А раз так, вопрос «делимо ли сущее в конечном счёте?» теряет тот смысл, который в него вкладывал спор. На каждом данном уровне рассмотрения есть то, что уже разложено (текущие системы), и то, что ещё не разложено (текущие атомы). «В конечном счёте» — то есть безотносительно ко всякому уровню — делимость не определена вовсе, потому что делимость по определению относительна к уровню, на котором различение проведено или не проведено.

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

Стоит быть точным в том, что здесь утверждается. ToS не объявляет спор бессмысленным и не отказывает его участникам в предмете. ToS переописывает предмет: то, что атомист и континуалист считали описанием сущего, есть на деле описание процесса различения сущего. Атомист верно замечает, что на всяком уровне есть неразложенное; континуалист верно замечает, что всякое неразложенное может быть разложено на уровне ниже. Обе верные половины принадлежат не сущему-самому-по-себе, а операциональной структуре различения — и, будучи отнесены к ней, перестают противоречить друг другу.

Уровни рассмотрения единицы

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

Единица в ToS есть число: отпечаток первого акта, мера совершённого (§ 1.2). Число же — не то, что делится. Делится, по § 1.7.2, то, внутри чего совершено различение, — некоторая система. Поэтому строго поставленный вопрос звучит не «делима ли единица», а так: делима ли система, которую единица собой фиксирует? Единица как число не делима ни на каком уровне — делимо или неделимо то, что единица на данном уровне отмечает. И ответ операционален: смотря какую систему единица фиксирует на рассматриваемом уровне.

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

Уровень акта (настоящая глава). Здесь единица есть число первого акта различения, и фиксирует она сам акт, взятый как целое. Внутри этого акта-как-целого никакого различения не совершено — акт взят как одно совершённое. Система, которую единица здесь отмечает (сам акт), не разложена: на этом уровне она атомарна. Не потому неделима, что такова её природа, а потому, что разлагающего акта здесь не проведено.

Уровень списка (Глава II.2). На уровне кардинального пути единица фиксирует список из одного различия. Этот список как система тоже не разложен: внутри единственного его элемента различение не проведено. Существенно отделить две операции, которые легко спутать. Разложить список из одного элемента — значит провести различение внутри него; такого различения здесь нет, и в этом смысле система не делима. Удлинить список — значит присоединить к нему ещё одно различие, перейдя к списку из двух; это не деление единицы и вообще не деление, а переход к другому числу, к двойке. Деление ищет структуру внутри того, что есть; удлинение ставит ещё одно рядом. Единица не делится оттого, что список можно удлинить: удлинение списка есть путь к двойке (Глава II.2), а не разложение единицы.

Уровень отрезка (Часть III). Когда в Части III появятся рациональные числа, единица будет фиксировать отрезок $[0,1]$. Вот здесь система, отмеченная единицей, делима: относительно отрезка проводятся различения, разлагающие его на рациональные части — половину, треть, и так далее. Делим при этом отрезок — система, — а не число «один»: число по-прежнему лишь метит эту систему как целое. Это не противоречит атомарности на уровне акта: акт, отмечаемый единицей там, и отрезок, отмечаемый единицей здесь, — разные системы на разных уровнях, и то, что одна не разложена, а другая разложена, никакого закона не нарушает.

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

Уровень элемента структуры (Части III и далее). Отдельно стоит назвать уровень, на котором символ $1$ выступает элементом алгебраической структуры — нейтральным элементом умножения в кольце или поле. На этом уровне выражения вида $1/2$, $1/3$ совершенно законны: в поле $Q$ или $R$ единица участвует в операции деления, и записи <<половина единицы>>, <<треть единицы>> имеют точный смысл. Это не противоречит сказанному. Делится здесь не первичная единица-счёт — числовой отпечаток одного акта, — а $1$ в роли элемента структуры, меры, границы. Один акт различения не становится двумя оттого, что внутри отмеченной им системы позднее проведено новое различение; но $1$ как элемент поля делится, потому что поле есть структура с заданной операцией деления. Возражение <<как же единица неделима, если есть $1/2$>> снимается именно этим различением: $1/2$ есть деление элемента поля, а не деление единицы-счёта.

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

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

Уровень	Что метит единица	Делимо ли отмеченное
акт (эта глава)	один акт различения	нет: акт взят как одно совершённое целое
список (Гл. II.2)	список из одного различия	не делится как список, но может удлиняться
отрезок (Часть III)	отрезок $[0,1]$	да: отрезок делим на рациональные части
процесс (Часть IV)	сходящийся процесс приближений	да: внутренняя структура процесса различима по стадиям
элемент структуры (Части III и далее)	$1$ как нейтральный элемент кольца / поля	да: $1/2$, $1/3$ — законные операции деления

Во всех пяти строках первичная единица-счёт — числовой отпечаток одного акта — остаётся неделимой; делится отмечаемое — система или структура — по своему уровню. Таблица делает наглядным, что <<единица неделима>> и <<есть $1/2$>> не противоречат друг другу: относятся к разным строкам. Согласованность обеспечена тем же $P1$ — иерархией уровней, — на котором стоит $M_2$: «делимо / неделимо» всегда относится к системе на конкретном уровне, а не к числу и не ко всем уровням сразу. Переходы между уровнями — предмет позднейших частей тома; для настоящей главы существенно лишь, что уровни различены и что число «один», оставаясь одним, фиксирует на каждом уровне свою систему.

Делимо или неделимо не первичная единица-счёт, а система, которую единица на данном уровне фиксирует. Единица как счётный отпечаток одного акта не делится. Система же — акт, список, отрезок, процесс, элемент структуры — делима или нет по своему состоянию различений: акт и список не разложены, отрезок и процесс разложимы, а $1$ как элемент поля участвует в делении. Это не пять разных единиц и не противоречие, а одно счётное число, метящее на разных уровнях разные системы — по мотиву $M_2$, по которому атомарность всегда относительна к уровню.

Этим вопрос делимости единицы исчерпан, и первичность единицы устояла. Делимость отрезка $[0,1]$, процесса сходимости или $1$ как элемента поля не подрывает первичности единицы-счёта: первичность утверждалась о единице как числовом отпечатке первого акта (§ 1.2), и именно эта единица-счёт не делится. Делимы системы и структуры, которые единица метит на иных уровнях, — но их делимость есть их свойство на их уровнях и первого акта не касается.

Остаётся последнее. Операциональная делимость и относительность уровней, разобранные здесь, дают ToS инструмент для случая, который в наивном изложении считается простым, а на деле скрывает невыговоренный переход режима, — для записи $0,999\dots =1$. Им глава и завершается.

Процесс и атом: о записи $0,999\dots${0,999…}

Зачем главе этот случай

Глава завершается разбором одного конкретного случая — записи $0,999\dots$ и привычного утверждения $0,999\dots =1$. Случай выбран не ради полемики со стандартной математикой, а потому, что на нём проверяется всё, что глава установила: первичность единицы, её атомарность на уровне акта, операциональная делимость, относительность уровней рассмотрения. Если эти положения верны, они должны давать ясный ответ на спорный случай — и дают.

Сразу оговорим жанр. Ниже не доказывается, что стандартная математика ошибается — в её собственном режиме, где запись $0,999\dots$ по определению означает действительное число, равенство $0,999\dots =1$ корректно. Доказывается другое и более точное: что за привычным знаком равенства, когда режим не указан, скрыт невыговоренный переход типа — от процесса приближений к его пределу, — и что ToS, делая этот переход явным, получает иную, более различённую картину. Случай $0,999\dots$ интересен ToS как пример того, что происходит, когда онтологическая природа записи остаётся непроговорённой.

Что такое запись $0,999\dots${0,999…}

Прежде чем спрашивать, чему $0,999\dots$ равно, нужно спросить, что эта запись есть. Вопрос обычно пропускают — и напрасно, потому что в нём всё дело.

$0,999\dots$ есть запись — строка символов в позиционной десятичной системе, в которой после запятой стоит цифра $9$, повторяемая без конца. Что эта строка означает, взятая буквально? Она означает указание: возьми $0,9$; затем $0,99$; затем $0,999$; и продолжай. Буквальное содержание записи $0,999\dots$ есть схема порождения приближений — последовательность

$$0,9,0,99,0,999,0,9999,\dots$$

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

На языке ToS такая схема есть процесс: разворачиваемая последовательность актов различения, каждый шаг которой — новое различение. Это законный объект ToS, и он согласован с принципом $P4$: процесс продолжаем без конца, но нигде не возникает завершённой бесконечности — есть бесконечная возможность сделать ещё шаг, а не достигнутый бесконечный объект. Многоточие в записи $0,999\dots$ означает именно это: «продолжай», а не «вот завершённый бесконечный результат».

Запись $0,999\dots$, взятая буквально, означает процесс — схему порождения приближений $0,9,0,99,0,999,\dots$ Многоточие есть знак продолжаемости, не знак завершённой бесконечности. Никакого иного объекта, кроме процесса, эта запись сама по себе не вводит.

Где в записи появляется «число»

Если $0,999\dots$ означает процесс, откуда берётся привычное утверждение, что $0,999\dots$ есть число — и притом число $1$?

Оно берётся из добавочного акта. Стандартный анализ не оставляет $0,999\dots$ процессом — он переназначает эту запись: объявляет, что $0,999\dots$ обозначает не схему приближений, а предел этой схемы, то есть единый объект, к которому приближения сходятся. И затем доказывает, что этот предел равен $1$.

Существенно увидеть, что здесь произошло. Сама строка $0,999\dots$ никакого предела «не содержала» — предел вложен в неё определением. Переход от «$0,999\dots$ есть схема приближений» к «$0,999\dots$ есть предел схемы» не прочитан из записи — он совершён как акт. И акт этот, как правило, не выговаривается: в привычном изложении $0,999\dots =1$ подаётся как обнаруженное тождество, а не как результат решения трактовать запись определённым образом.

Что это именно акт, а не нечто само собой разумеющееся, видно из того, что в стандартной математике само действительное число строится по-разному, и во всех построениях $0,999\dots$ как последовательность и $1$ как число суть разные объекты:

• в построении через фундаментальные последовательности (Коши) действительное число есть класс эквивалентности сходящихся последовательностей рациональных; $0,999\dots$ — одна из последовательностей, $1$ — класс;
• в построении через сечения (Дедекинд) действительное число есть сечение во множестве рациональных; $0,999\dots$ — схема, порождающая приближения, $1$ — сечение;
• в аксиоматическом задании действительное число есть элемент полного упорядоченного поля; $0,999\dots$ — запись, $1$ — элемент.

Во всех трёх случаях, чтобы поставить знак $=$ между $0,999\dots$ и $1$, нужно сперва перевести левую сторону в тот же род объекта, что правая — взять класс эквивалентности, или сечение, или элемент поля. Этот перевод и есть невыговоренный акт. До него $0,999\dots$ и $1$ — объекты разной природы; после него их объявляют одним.

Где запись скрывает переход типа

Теперь видно, в чём именно ToS расходится с наивным прочтением $0,999\dots =1$ — и в чём не расходится со стандартным анализом.

Сначала о том, в чём расхождения нет. В стандартной математике запись $0,999\dots$ по определению обозначает действительное число — предел соответствующей последовательности или её класс эквивалентности. При таком, заранее заданном, прочтении обе стороны равенства $0,999\dots =1$ находятся в одном типе — в $R$, — и равенство корректно. Закон $L1$ — $A=A$ (Глава I.3), требующий, чтобы по обе стороны знака равенства стояло одно и то же в одном и том же типе, — здесь не нарушен: интерпретация записи задана, и оба объекта суть действительные числа. ToS не объявляет стандартное равенство ложным в его собственном режиме.

Расхождение ToS — с наивным чтением, в котором режим не указан. Если взять $0,999\dots$ как процесс порождения рациональных приближений (§ 1.8.2), а $1$ — как единичный атом, число первого акта (§ 1.7), то это объекты разных режимов: слева процесс, справа атом. Между ними нельзя ставить безусловное равенство без предварительного перехода к общему режиму — например, к классу эквивалентности процессов или к пределу. Опасность здесь не в ложности стандартного равенства, а в невысказанном смешении двух уровней: уровня процесса (raw process) и уровня значения или класса (quotient/value level). Запись $0,999\dots =1$, взятая без указания режима, скрывает переход типа — переход от процесса приближений к его пределу или классу эквивалентности.

Без указания режима запись $0,999\dots =1$ скрывает переход типа: от процесса приближений к его классу эквивалентности или пределу. Опасность здесь не в ложности стандартного равенства — в режиме действительных чисел оно корректно, — а в невысказанном смешении process-уровня и quotient/value-уровня. Ошибка, если она возникает, есть ошибка наивного чтения, а не стандартной математики, где интерпретация записи задана.

Режим классов: где равенство законно

Сказанное не означает, что утверждение $0,999\dots =1$ всегда и во всяком смысле ложно. Оно означает, что у этого утверждения есть условие осмысленности, и условие это — выговоренный акт.

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

В выговоренном режиме классов утверждение $0,999\dots =1$ корректно: если оба объекта взяты как классы эквивалентности — процесс отнесён к своему классу, единица к своему, — то эти классы действительно совпадают, и равенство классов истинно. Здесь нет нарушения $L1$, потому что слева и справа стоит объект одного типа: класс. Ошибка возникает не от перехода к классам — ошибка возникает от молчаливого перехода: когда результат, верный в режиме классов, выдают за безусловное тождество, верное вне всякого режима.

ToS, таким образом, не отменяет $0,999\dots =1$ и не объявляет анализ ошибочным. ToS разделяет два утверждения, которые наивная запись без указания режима сливает в одно: «$0,999\dots$ и $1$ суть один и тот же класс эквивалентности процессов» (истинно, в выговоренном режиме $M_3$ — и именно это утверждает стандартный анализ, где запись по определению означает класс или предел) и «$0,999\dots$-как-процесс и $1$-как-атом суть один и тот же объект одного режима» (неверно: процесс и атом принадлежат разным режимам, и равенство между ними поставлено без перехода к общему режиму). Привычное $0,999\dots =1$ опасно не тем, что неверно — в своём режиме оно верно, — а тем, что само по себе не указывает режима, и тем побуждает прочитать верное-в-режиме-классов как безусловное тождество объектов разных режимов.

Чем этот случай важен для ToS

Разбор записи $0,999\dots$ занял в главе место не из-за самого этого равенства, а из-за того, что он впервые показывает в работе различение, на котором будет стоять значительная часть тома, — различение процесса и атома.

{ Случай $0,999\dots$ есть частный и наглядный. Но то же различение встанет в полную величину в Части IV. Там действительное число будет введено не как точка и не как готовый объект, а как процесс — RealProcess, — разворачиваемая схема рациональных приближений. Репозиторий уже содержит ядро этого аппарата: файл src/process/ProcessCore.v определяет RealProcess $:=‘nat‘\to Q$ (процесс над $Q$, индексированный стадиями), constprocess $q$ (постоянный процесс, выдающий $q$ на каждой стадии) и отношение processequiv (обозначаемое ~~), которое связывает два процесса, сходящихся к одному пределу; processequiv доказано отношением эквивалентности (рефлексивным, симметричным, транзитивным). Существенно, что processequiv есть не поточечное равенство: два процесса могут быть process_equiv, расходясь на каждой отдельной стадии.

В этом языке позиция ToS по поводу $0,999\dots$ формулируется точно — и это удобный мост к будущей формализации. Запись $0,999\dots$ отвечает процессу $n\mapsto 1-1/10^{n+1}$; единица отвечает постоянному процессу constprocess $1$. Эти два процесса не равны поточечно — на каждой стадии первый строго меньше второго, — но они processequiv: сходятся к одному пределу. Различение трёх режимов из § 1.8 ложится на это прямо: как сырые процессы $0,999\dots$ и $1$ различны (различие поточечно); как классы по process_equiv они совпадают; в стандартной записи действительных чисел равенство законно, потому что запись уже означает класс или предел. Формальная проверка этой картины — через теоремы вида <<процесс девяток не поточечно равен constprocess $1$>> и <<процесс девяток processequiv const_process $1$>> — относится к Части IV; ProcessCore.v даёт для неё готовый язык, но самих этих теорем о девятках в репозитории пока нет. То, что на примере $0,999\dots$ выглядит как частная тонкость, в Части IV окажется общим устройством действительного числа: действительное есть процесс, и сходимость есть его поведение, а не поточечное равенство процесса точке. }

Здесь же видно, отчего вопрос, остро звучащий в стандартной рамке, в ToS во многом снимается. Острота $0,999\dots =1$ возникает оттого, что действительные числа берутся как готовое множество $\mathbb{R}$, в котором процесс и его предел обязаны быть одним элементом, иначе множество «неполно». ToS не строит $\mathbb{R}$ как готовое множество (причины — $P4$ и производность множеств, $M_3$; развёрнуто — Часть IV). Нет готового $\mathbb{R}$ — нет и принуждения отождествить процесс с атомом. Есть процесс со своим поведением и есть атом; они различны; и это не создаёт никакой неполноты, потому что полнота готового множества ToS и не требуется. Спорный случай перестаёт быть спорным, как только снято допущение, его породившее.

Случай $0,999\dots$ важен ToS как первое появление различения процесса и атома — различения, на котором Часть IV построит действительное число как процесс. В рамке готового множества $\mathbb{R}$ отождествление процесса и предела вынуждено требованием полноты; ToS этого множества как готового объекта не вводит, и вынуждающего требования не возникает. Процесс и атом остаются различны, и $L1$ остаётся в силе.

Разбор E/R/R: единица-первая как система

{ Прежде чем подвести итог, сведём пройденное в разбор E/R/R (Часть I): он закрепляет, почему единица первична, и задаёт тон всей Части II. Заголовок опорного файла размечает прямо: элементы — счёт от различений; роли — единица есть первое различение, нуль есть отсутствие; правила — первое есть единица, нуль из отсутствия, следующее из различения.¹⁵ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе: <<система>> здесь — содержательная интерпретация; one_from_distinction машинно проверяет выбранную регистрацию (каждому различению — отпечаток $1$), а не доказывает первичность, и онтологический порядок <<$1$ прежде $0$>> опирается на distinction_order (§ 1.2, § 1.4).}

{ Rules — правила (законы $L1$–$L5$). Конституция — правило регистрации: первый акт различения отмечается единицей (one_is_first), всякое следующее различение даёт следующее число (succ_from_distinction); нуль — из отсутствия различения (zero_from_absence), а не из счёта. К ним — правило асимметрии: единица предшествует нулю (distinction_order, § 1.2.3), не наоборот. И правило совместимости: инверсия первичности есть переинтерпретация типа nat (два порядка — онтологический и синтаксический), а не его переопределение (§ 1.4).}

Roles — значимость позиций (закон $L4$). Единица — роль первого: отпечаток первого совершённого акта, первый положительный счёт. Нуль — роль границы: отметка отсутствия различений в данном списке или на данной стадии, в счёт актов не входящая (§ 1.3). Это две роли, не два предмета: единица не <<множество из одного>>, а сам акт (§ 1.2.2); нуль не пустота-сущность, а граничная отметка. По $L4$ нуль производен — его наличие требует объяснения отсутствия, а потому он логически позднее.

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

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

Компонент	Что фиксирует	E/R/R
первый акт $=1$; следующее из различения	конституция счёта	Rule
асимметрия <<$1$ прежде $0$>>; нуль из отсутствия	порядок и граница	Rule
инверсия как переинтерпретация nat	два порядка (§ 1.4)	Rule
единица: первый счёт (отпечаток акта)	роль первого	Role
нуль: отметка отсутствия (не счёт)	роль границы	Role
акты различения (ToS_nat)	носители (конечны, $P4$)	Element
законы $L1$–$L5$	универсальный слой	Rule (универс.)

{ Хорошая сформированность. Разметка однозначна: акты — элементы, единица и нуль — роли, регистрация и асимметрия — правила. Соблюдён $P1$: счёт есть счёт актов (элементов), число не числит само себя. И здесь разбор оборачивается диагностикой, и притом исходной для всей Части II. Стандартная позиция <<нуль первичен>> берёт нуль как первичный предмет — пустое множество, из которого строится число (§ 1.1). Это — смешение категорий: нуль есть роль (граница, отсутствие), а не предмет-основание, и единица есть роль (первый счёт), а не <<множество из одного>> (§ 1.2.2). Число рождается из акта — из присутствия различения, — а не из пустоты; читать его как предмет, выстроенный из ничто, значит принять роль за элемент. Тот же сдвиг ToS будет снимать и дальше — для множества, точки, бесконечности (Часть I; Части III–IV).}

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

Итог главы

Глава установила первичность единицы и провела следствия этой первичности.

Единица первична как число первого акта различения — как числовой отпечаток совершённого акта. Она доступна прежде развёрнутого счёта: не как уже построенный элемент числового ряда в полном арифметическом смысле, а как то, что этот ряд позднее формализует как первый положительный счёт (§ 1.2). Нуль производен: он не предмет и не пустота-сущность, а граничная отметка ряда совершённых различений, и в счёт совершённых актов он не входит (§ 1.3). Инверсия первичности — не переопределение типа nat, а его переинтерпретация: синтаксический порядок конструкторов и онтологический порядок обоснования различены, и их расхождение есть содержание инверсии (§ 1.4). Независимо построенная позиция ToS перекликается с устойчивым мотивом европейской и иных традиций мысли о числе — от пифагорейцев до Спенсера-Брауна; это — сходящаяся параллель, а не доказательство (§ 1.5). Считать в ToS — значит фиксировать число совершённых различений, а не наращивать величину от пустоты (§ 1.6). Делимо или неделимо не само число, а то, что число на данном уровне фиксирует: единица как счётный отпечаток одного акта не делится, тогда как символ $1$ в роли элемента $Q$, длины отрезка $[0,1]$ или нейтрального элемента умножения участвует в операциях деления — делится не первичная единица-счёт, а структура, в которой $1$ играет роль меры (§ 1.7). И там, где онтологическая природа записи остаётся непроговорённой — как в $0,999\dots =1$, — наивное чтение смешивает процесс приближений и его предел; ToS снимает это смешение, делая явным переход режима, который привычная запись скрывает (§ 1.8).

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

---

---

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

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

Навигация: ← Глава 7. Онтологическое ядро: сквозные мотивы — Часть I · Глава 2. Счёт как длина списка различий →

Footnotes

1. Тип nat стандартной библиотеки Rocq; конструктор O — нуль, S — последователь. Подробное обсуждение этого типа и его соотношения с конструкцией ToS — в § 1.4. ↩

2. Натуральные числа как начальный объект, или начальная алгебра функтора $1+(-)$; категорный путь будет подробно рассмотрен в части тома, посвящённой категорной организации математики. Здесь он привлекается лишь как третья форма, в которой нуль получает первичный статус. ↩

3. Тип DistinctionSide и sidevalue в текущем репозитории отсутствуют — это предложение по усилению AsymmetricDistinction.v. До его внесения формальным носителем приоритета остаётся пара mark / unmark в её proof-level форме плюс distinctionorder $=(1,0)$. ↩

4. Доказательство distinction_asymmetric опирается на аксиому classic — техническое свидетельство $L3$ в CIC (Глава I.6). Это уместно: утверждение «$P$ и $\neg P$ не совпадают» есть утверждение об определённости различия, а определённость различия и есть то, что $L3$ обеспечивает. Здесь classic работает не как привнесённое допущение, а как формальный след структурного закона акта различения. ↩

5. Это расхождение формы — предмет для синхронизации репозитория. Чтобы orderingsdual в PrimalityOfOne.v фиксировала именно две противоположные пары, её следовало бы переписать через tosconceptualordering $:=(1,0)$ и numberordering $:=(0,1)$, как уже сделано для distinctionorder в AsymmetricDistinction.v. До такой синхронизации книга опирается на distinctionorder как на формальный носитель пары $(1,0)$. ↩

6. Подробное рассмотрение соотношения «один синтаксис — несколько семантик», включая ответ на возражение о том, что работа на стандартном nat лишает ToS оригинальности, — в Главе II.5. Там же — связь с тем, что некоторые трудности теоретико-множественного основания суть симптомы интерпретации, а не синтаксиса. ↩

7. Приём сходящихся параллелей уже применялся в Части I — в Главе I.2 и в историческом разделе Главы I.5. Здесь тот же приём приложен к первичности единицы. Подчеркнём его статус: параллель эвристическая, а не доказательная. ↩

8. Учение о Монаде известно по позднейшим свидетельствам; основные источники — Аристотель, Метафизика I.5, и compilation Теона Смирнского <<Изложение математических предметов, полезных для чтения Платона>>. Прямых пифагорейских текстов не сохранилось, и реконструкция учения о Монаде опирается на доксографическую традицию. ↩

9. Плотин, Эннеады, трактат VI.9 <<О Благе или Едином>>. Прокл прилагает схему нисхождения к математике в Комментарии к первой книге <<Начал>> Евклида (пролог). ↩

10. Г. Фреге, Основания арифметики (Die Grundlagen der Arithmetik, 1884), § 55–57 (число как свойство понятия) и § 74 (определение нуля через понятие $x\ne x$). ↩

11. Совпадение тем заметнее, что отправные точки разные. Фреге работает в логицистской программе и в теоретико-понятийной рамке; ToS — в процессуальной онтологии акта различения. Что две столь разные рамки сходятся в производности нуля и в его связи с нарушением $L1$ — ещё одно сходящееся свидетельство в смысле § 1.5.1. ↩

12. Понятие множества как объединения в одно целое определённых различимых объектов Кантор формулирует в <<Beiträge zur Begründung der transfiniten Mengenlehre>> (1895), § 1. ↩

13. G. Spencer-Brown, Laws of Form (1969); построение начинается с предписания <> в гл. 1. ↩

14. Пример с кварком — иллюстрация операционального взгляда, не утверждение физики. Вопрос о строении кварка принадлежит физике и Тому III; здесь кварк привлечён лишь как наглядный случай объекта, атомарного относительно нынешнего состояния различений. ↩

15. E/R/R-разметка в шапке файла PrimalityOfOne.v; асимметрия <<единица прежде нуля>> — в AsymmetricDistinction.v. Здесь разворачивается по образцу Части I. ↩