Глава 2. Глубина = рунг всеведения

Где стоит глава

Глава 1 показала, что сторона предела-роли — восходящая башня роль-типов: строго растущая (диагональ на каждом этаже), порождающая (без вершины), индексированная ординалом-процессом $\omega$. Но «выше» там значило лишь шире — больше предикатов. Настоящая глава добавляет второе измерение: этажи не только шире, они глубже. Вопрос, заданный на этаже, требует определённой меры «завершённой бесконечности» — и эта мера растёт с высотой.

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

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

Что глава фиксирует и что нет

Честно очертим вклад. Доказано точно и без аксиом: нижний этаж разрешим (рунг 0), этаж предикатов над ℕ отвечает ровно принципу ограниченного всеведения, и эта градация схлопывается под Законом Исключённого Третьего — то есть конструктивна¹.

{ Заимствовано, не ново: сами восходящие импликации между рунгами ($\text{LPO}\to \text{WLPO}\to \text{LLPO}$ и прочие) — стандартная конструктивная обратная математика (Бишоп, Исихара). Не доказано здесь: строгость рунгов — то, что импликации необратимы, что рунги действительно различны, — требует теоретико-модельных конструкций (реализуемость, модели Крипке) и в нашем основании не строится; это честно указывается и на этом мы останавливаемся². Наш собственный вклад скромен и точен: разместить этажи башни на этой лестнице и зафиксировать машинно конструктивность самой градации.}

Нулевой этаж: разрешимость без всеведения

Нулевой этаж — носитель ℕ. Здесь вопрос о равенстве двух элементов разрешим: для любых $m,n$ можно за конечное число шагов установить, равны они или нет³. Никакого всеведения не требуется: ответ даёт конечная процедура, чистый Элемент. Это рунг 0 — основание лестницы, сторона Элемента границы финитизации.

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

Этаж предикатов — это ровно LPO

Поднимемся на этаж выше: предикаты над ℕ — булевы нити $g:N\to \{\text{да},\text{нет}\}$. О такой нити естественно спросить: срабатывает ли она когда-нибудь, или не срабатывает никогда? То есть:

$$(\exists n:g(n)=\text{да})\text{или}(\forall n:g(n)=\text{нет}).$$

Это не безобидный вопрос. Чтобы ответить «никогда», нужно обозреть весь бесконечный процесс нити — завершить бесконечность. Утверждение, что на этот вопрос всегда есть ответ, носит имя: принцип ограниченного всеведения (LPO).

Вопрос этажа предикатов — «срабатывает или никогда» — есть в точности LPO.

И это не аналогия, а тождество: способность решать вопрос на этом этаже эквивалентна LPO — ни больше, ни меньше⁴. Так этаж 1 получает точный рунг: ${\Sigma }_1^0$-всеведение, ровно один шаг завершённой бесконечности над разрешимым основанием.

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

Лестница всеведения

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

$$\text{LLPO}\prec \text{WLPO}\prec \text{LPO}\prec {\text{LPO}}_{\omega }.$$

LLPO — сверхслабый принцип развилки («если два события не могут сработать оба, то одно не срабатывает никогда»); WLPO решает истинностное значение «никогда» без свидетеля; LPO — наш этаж 1, решение со свидетелем; а ${\text{LPO}}_{\omega }$ — каскадный рунг: «бесконечно ли много нитей срабатывает, или лишь конечно много» — граница границ.

Восходящие импликации доказаны: более высокий рунг влечёт нижний⁵. В частности, каскад строго требовательнее одиночного вопроса: ${\text{LPO}}_{\omega }\to \text{LPO}$ доказано напрямую⁶. Так лестница градуирует сторону предела-роли: чем выше по башне поднимается вопрос, тем выше его рунг всеведения.

Градация конструктивна (и видна лишь через P4{P4})

Теперь — наблюдение, ради которого глава написана.

Возьмём Закон Исключённого Третьего. Под ним вопрос этажа 1 решается даром: «или нить где-то срабатывает, или нет» — это просто экземпляр «или $A$, или не $A$»⁷. То же и выше по лестнице: классически держатся все рунги. Значит, под Законом Исключённого Третьего лестница плоская — все принципы суть теоремы, глубины нет.

Глубина этажей видна только без Закона Исключённого Третьего. Это конструктивный, P4-феномен: классическая логика его не различает.

Вот точный смысл того, что «P4-оптика тоньше классической». Это не новая теорема и не спор с классикой; это известный мета-факт — классически плоско, конструктивно градуировано, — сделанный машинно явным. Для нас он важен принципиально: глубина процессной иерархии есть свойство процессов, читаемое только процессным взглядом. Тот, кто принимает завершённую бесконечность даром (через Закон Исключённого Третьего), не видит, что разные этажи требуют разной её меры, — для него всё уже завершено. P4, отказываясь от даровой завершённости, делает меру видимой.

E/R/R-разбор: лестница как система

Лестница рунгов сама есть система, и разбор её по E/R/R — в порождающем порядке Rules $\to$ Roles $\to$ Elements — проясняет, чем «глубина» отличается от «ширины».

Rules (L5). Удерживающие правила — восходящие импликации между рунгами (более высокий влечёт нижний; доказаны конструктивно) и схлопывающее правило: Закон Исключённого Третьего влечёт каждый рунг. К ним примыкает граница метода: строгость рунгов (необратимость) правилами этого уровня не устанавливается — для неё нужна модель, и здесь мы останавливаемся.

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

Elements (L1 + P4). Носители — булевы нити $g:N\to \{\cdots \}$ и конечные префиксы, которые можно обозреть. Под P4 актуальны только конечные префиксы; ответ «срабатывает» актуализуется конечной ступенью (Элемент), а ответ «никогда» остаётся пределом-ролью — именно за него и взимается рунг всеведения.

Проверка сформированности. Каждый компонент — в одной категории: импликации и схлопывание — Rules, рунг-как-мера — Role, нити и префиксы — Elements. Самоприменения нет: правило, сортирующее рунги, стоит над ними и не есть один из рунгов.

Что даёт разбор. Он показывает, что «глубина» иерархии — не вторая «ширина», а отношение к завершённой бесконечности: этаж тем глубже, чем больше её требует его вопрос. И он объясняет, почему глубина невидима классически: оракул L3 уравнивает все меры, стирая само отношение, которым глубина измеряется.

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

---

---

Часть: Часть XVIII. Процессная иерархия · Том: «Математика»

Навигация: ← Глава 1. Восходящая башня роль-типов · Глава 3. Детерминированность вверх по иерархии →

Footnotes

1. Файл HierarchyDepthLadder вместе с RoleLimitLadder; машинно проверено, 0 аксиом. Принципы всеведения здесь — гипотезы-предложения (Prop), а не аксиомы: ни один из них не объявлен истинным; доказаны лишь импликации между ними и их схлопывание под Законом Исключённого Третьего. ↩

2. Утверждать необратимость импликаций без модели нельзя; привлечение Закона Исключённого Третьего, напротив, сплющило бы лестницу. Поэтому строгость рунгов цитируется как известный результат, а не доказывается. ↩

3. level0_decidable: равенство на нулевом этаже разрешимо. 0 аксиом. ↩

4. level1_decision_is_LPO: разрешимость вопроса «срабатывает или никогда» на этаже предикатов равносильна LPO. Машинно проверено, 0 аксиом. ↩

5. Свод role_limit_ladder: ${\text{LPO}}_{\omega }\to \text{LPO}\to \text{WLPO}\to \text{LLPO}$ (и $\text{LPO}\to$ принцип Маркова). Машинно проверено, 0 аксиом. ↩

6. lpo_omega_lpo: умение решить «конечно или бесконечно много срабатываний» влечёт умение решить «срабатывает ли одна нить». 0 аксиом. ↩

7. lem_decides_level1: Закон Исключённого Третьего влечёт разрешимость вопроса этажа 1 (то есть LPO). 0 аксиом. Аналогично весь верх лестницы: классически держится и ${\text{LPO}}_{\omega }$. ↩