Глава 3. Одна диагональ: halting, Райс, Кантор, Колмогоров

Один двигатель: неподвижная точка

Сердце части — утверждение, на первый взгляд несоразмерное своим следствиям:

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

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

Её форма проста. Если отображение $\phi :A\to (A\to B)$ точечно сюръективно (каждая функция $A\to B$ есть $\phi (a)$ для некоторого $a$), то у всякого эндоморфизма $f:B\to B$ есть неподвижная точка:

$$\phi :A\to (A\to B)\text{точечно сюръективно}⟹\forall f:B\to B,\exists b,f(b)=b.$$

Контрапозиция и есть рабочий инструмент: если у какого-то $f$ неподвижной точки НЕТ, точечной сюръекции быть не может. А простейший эндоморфизм без неподвижной точки — булево отрицание:

$$\forall b\in \text{BB}:b\ne \text{negb}b.$$

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

Это первая master-структура части: неразрешимость есть одна теорема о неподвижной точке. Ниже — её четыре грани; зеркальная, положительная master-структура (один дискриминант) ждёт в 15.4.

Программа: нет универсального решателя остановки

Предположим противное — есть тотальный решатель $D(p,q)$, отвечающий «да / нет» на вопрос «останавливается ли программа $p$ на входе $q$?». Построим диагональную программу $\Delta$: на входе $p$ она спрашивает $D(p,p)$ и делает противоположное — останавливается ровно тогда, когда $D$ говорит «не остановится»:

$$\Delta (p)\text{останавливается}⟺D(p,p)=\mathrm{false}.$$

Подставим $\Delta$ себе. Получаем $\Delta (\Delta )\text{останавливается}⟺\Delta (\Delta )\text{не останавливается}$ — ровно искомая неподвижная точка отрицания, которой нет. Значит тотального решателя $D$ не существует.²

Сравним с 15.1. Там ограниченная остановка была разрешима (Element). Здесь запрещён не отдельный прогон, а тотальный решатель «для всех программ сразу». Диагональ запрещает именно реификацию role-limit в Element-решатель — не «мы не сумели вычислить», а «такого Element-объекта нет».

Множество: булево пространство не перечислимо (Кантор)

Та же конструкция над множествами. Никакое $g:A\to (A\to \text{BB})$ не сюръективно: предикат

$$d(a):=\text{negb}(g(a)(a))\text{отличается от каждого }g(a)\text{в точке }a,$$

ведь $d(a)=\text{negb}(g(a)(a))\ne g(a)(a)$. Значит $d$ не есть ни одно $g(a)$ — перечисления всех предикатов $A\to \text{BB}$ нет. Это снова $b\ne \text{negb}b$, теперь по диагонали $a\mapsto g(a)(a)$.³

Важнейшее различение (честная цена). Эта диагональ — над пространством булевых предикатов $A\to \text{BB}$ — вполне конструктивна: ни закона исключённого третьего, ни выбора, ни одной аксиомы. А знаменитая «несчётность континуума» (завершённой вещественной прямой) — утверждение другое и более сильное: оно опирается на классический слой (L3, classic) вместе с L4 и живёт отдельно. Наша система их не смешивает: диагональ-над-предикатами 0-аксиомна, а несчётность завершённого континуума платит классическую цену.⁴

Семантика: нет решателя нетривиальных свойств (Райс)

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

Райс — это «halting в общем виде»: не только остановка, но любое нетривиальное свойство поведения нефинитизируемо в тотальный решатель. Граница та же: тривиальное (вырожденное) — Element; содержательно-семантическое — role-limit.

Сложность: колмогоровская грань (Берри/Чейтин)

Четвёртая грань — сложность объекта (его кратчайшее описание). У неё, как и у остановки, две стороны. Element-сторона — несжимаемость счётом: при любом бюджете $n$ коротких программ конечно, поэтому какой-то объект не описывается в пределах $n$ — чистая голубятня, 0 аксиом. Role-limit-сторона — тотальный решатель критерия сложности (модель-относительный $K$-оракул): когда модель допускает самоотрицающий свидетель Берри / Чейтина («наименьшее число, не описываемое менее чем в $k$ символах» — само себя описавшее), он запрещён той же диагональю.⁶

Честная область. Колмогоровская $K$ здесь модель-относительна: полная инвариантность $K$ к выбору машины НЕ заявляется (это за границей формализованного). Утверждение точно: при фиксированной модели описания тотальный решатель критерия сложности — role-limit, побеждаемый тем же $b\ne \text{negb}b$, что halting и Кантор. Колмогоров — четвёртая грань.

Одна диагональ — четыре грани (и далее)

Соберём грани в одно. Все четыре — частные случаи одного движка (diagonal_ defeats_ decider), укоренённого в теореме Лавера:

Грань	Role-limit (запрещено диагональю)	Машинный анкер
программа	тотальный решатель остановки	no_halting_decider
множество	сюръекция $A\to (A\to \text{BB})$ (Кантор)	cantor_no_surjection
семантика	решатель нетривиального свойства (Райс)	rice_role_limit
сложность	решатель критерия сложности (Берри / Чейтин)	kolmogorov_ role_ limit_ drawn
\multicolumn{3}{@{}p{0.93\textwidth}@{}}{Element-контраст (число): дискриминант rational_split разрешим (discriminant_element_drawn) — мост к 15.4.}

Эти грани собраны в один машинный итог: число (Element), программа, множество и сложность — одна граница, четыре лица, единый движок $b\ne \text{negb}b$.⁷ Разрешимая грань (число, дискриминант) намеренно стоит в той же теореме — она и есть зеркало, которое разворачивает 15.4.

Грани сверх четырёх. «И далее» означает не новые грани в капстоуне этой главы (он собирает именно четыре CS-грани, one_boundary_four_faces), а ту же диагональную схему, расширенную на классические парадоксы: нет универсального множества (Рассел), нет предиката истины (Тарский), невозможны «лжец» и «Греллинг». Это та же диагональ над Prop (двойник $(\neg P)\ne P$ вместо $b\ne \text{negb}b$), со своими машинными доказательствами в отдельных файлах.⁸ Так диагональ объединяет не только невычислимость, но и парадоксы рассуждения — мост к таксономии парадоксов Архитектуры Рассуждения.

Разбор E/R/R и что глава подготовила

Правила (L5). Диагональ есть правило, запрещающее реифицировать role-limit в Element-решатель; атомарное правило — $b\ne \text{negb}b$ (и его Prop-двойник $(\neg P)\ne P$); теорема Лавера называет, почему это правило держит для всех граней сразу.

Роли (L4). Решатель / оракул — роль-оракул; «останавливается», «сложен», «истинно», «в диагональном множестве» — role-limit-предикаты. Их Element-двойники (ограниченная остановка, тривиальное свойство, несжимаемость-счётом, дискриминант) разрешимы — это другая роль.

{

Элементы (L1$+$P4). Конкретные программы, конечные прогоны, само булево отрицание, счётный аргумент голубятни. Не элемент: тотальный оракул остановки, тотальный $K$-решатель, предикат истины, универсальное множество — диагональ запрещает каждый.}

Компонент	Что фиксирует	E/R/R-категория
диагональ; $b\ne \text{negb}b$; $(\neg P)\ne P$; теорема Лавера	запрет реификации role-limit	Правило (L5)
решатель-оракул; «halts / сложен / истинно» как role-limit-предикаты	роли и пределы	Роль (L4)
программы; прогоны; negb; счёт голубятни	конечно-актуальные носители	Элемент (L1$+$P4)

Диагностика P4. Каждая грань — одна и та же категориальная ошибка: попытка реифицировать role-limit (процесс / предел) в завершённый Element-решатель. Теорема Лавера есть точная формулировка невозможности; четыре грани — её костюмы. Граница не «мешает вычислять» — она называет масштаб: что схватывается решателем, а что есть предел.

Что глава подготовила. Предъявлена первая master-структура части: неразрешимость — одна диагональ, корень — неподвижная точка (Лавер), четыре грани (halting / Кантор / Райс / Колмогоров) плюс парадоксы (Рассел / Тарский). Всё — 0-аксиомно и машинно проверено; единственная классическая цена — несчётность завершённого континуума, и она вынесена отдельно. Дальше — зеркало: глава 15.4 предъявит положительную master-структуру — один дискриминант редукционного атласа, рисующий разрешимую (Element) сторону одним терминирующим критерием.

---

---

Часть: Часть XV. Вычисления и граница финитизации · Том: «Математика»

Понятия: Парадокс

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

Footnotes

1. src/cs/LawvereFixedPoint.v (0 аксиом): point_surjective, lawvere_fixed_point; теорема cs_ diagonals_ are_lawvere формально собирает корень — lawvere_fixed_point, negb_no_fixpoint и канторовскую грань; halting / Райс / Колмогоров используют тот же $\text{negb}$-движок через diagonal_ defeats_ decider. Семя — HaltingRoleLimit.negb_no_fixpoint ($b\ne \text{negb}b$). Универсальный движок — src/cs/BoundaryDecidability.diagonal_defeats_decider: если против каждого решателя есть самоотрицающий свидетель, критерий role-limit-нарисован. ↩

2. src/cs/HaltingRoleLimit.v (0 аксиом): no_halting_decider (нет решателя самоприменения при самопрограммируемости SelfProgrammable), no_total_halting_oracle. Element-двойник — bounded_halting_decidable из 15.1. ↩

3. src/cs/HaltingRoleLimit.cantor_no_surjection (0 аксиом); как частный случай Лавера — LawvereFixedPoint.cantor_via_lawvere, nat_fun_not_enumerable. ↩

4. Несчётность завершённого континуума — ProcessDiagonal.binary_processes_not_enumerable, ProcessContinuumHypothesis.process_continuum_hypothesis: слой L3 (classic)$+$L4, отдельный и более сильный (ср. Часть IV). Контраст честен: cantor_no_surjection и halting classic НЕ требуют — это и есть «Element-сторона конструктивна». ↩

5. src/cs/RiceRoleLimit.v (0 аксиом): trivial_property_element_drawn (тривиальное — Element, разрешимо), RiceDiagonal и rice_diagonal_exists (самоотрицающий свидетель), rice_role_limit, rice_no_semantic_decider. ↩

6. src/cs/KolmogorovRoleLimit.v (0 аксиом): incompressible_exists (Element / счёт — при бюджете $n$ есть необъяснимый объект), kolmogorov_ role_ limit_ drawn доказывает role-предельность критерия Complex при диагонали Берри / Чейтина (частный случай diagonal_ defeats_ decider); это не теорема об инвариантности $K$ и не универсальная машина в полной общности. ↩

7. Формальный капстоун раздела — src/cs/ KolmogorovRoleLimit. one_boundary_ four_faces, расширяет BoundaryDecidability. one_boundary_ three_faces; 0 аксиом. ↩

8. src/cs/RussellViaLawvere.v (russell_ no_universal_set, liar, grelling, paradoxes_ one_diagonal; семя not_no_fixpoint: $(\neg P)\ne P$); src/cs/TarskiUndefinability.v (tarski_ no_truth_predicate, tarski_ from_lawvere). 0 аксиом. ↩