От первопорядковой $PA$ через $ACA_0$ и импредикативную $Z_2$ к теоретико-множественной $ZFA$: язык, модели, выразительная сила.
Построение второпорядковой теории начинается с фиксации первопорядковой базы. К стандартному языку добавляется второй сорт переменных — переменные по множествам индивидной области ($X, Y, Z, \dots$). В сигнатуру вводится предикат принадлежности $x \in X$, где $x$ — индивид, а $X$ — множество. Равенство между множествами при этом обычно не берут примитивным: запись $X = Y$ считается сокращением для $\forall n\,(n \in X \leftrightarrow n \in Y)$, так что экстенсиональность выполняется по определению языка, а не постулируется отдельной аксиомой (стандартное соглашение о языке $L_2$; Симпсон, SOSOA, §I.2).
Такое расширение языка порождает строгую иерархию формул. На нижнем уровне находятся чисто первопорядковые формулы. База расширяется классом арифметических формул — в обозначениях арифметической иерархии это классы $\Sigma^0_k$ и $\Pi^0_k$ (их не следует путать с $\Sigma^1_k$ аналитической иерархии): они могут содержать переменные-множества в качестве параметров, но не допускают квантификации по множествам. Выше располагается аналитическая иерархия — собственно второпорядковые формулы с кванторами по множествам ($\Sigma^1_k$, $\Pi^1_k$, …).
Фундаментальный шаг в построении теории — добавление схемы свёртывания, гарантирующей существование множеств, заданных формулами. Если ограничить эту схему арифметическими формулами, получается теория $ACA_0$. Свёртывание здесь узко предикативно: определение множества не опирается на кванторы по множествам и не требует «перебирать» универсум, к которому принадлежит само определяемое множество.
В более широком смысле предикативной математики (Вейль, 1918; Феферман, 1964; Шютте, 1965) допустимые системы простираются до $ATR_0$, чей доказательный ординал $\Gamma_0$ и принято считать границей предикативности, — существенно выше $ACA_0$ (ординал $\varepsilon_0$). $ACA_0$ — лишь нижняя ступень этого диапазона, хотя именно она часто служит точкой входа в обратную математику. Сам предикативный анализ Вейля вынесен в отдельный уровень формализации в материале «Уровни формализации математического анализа».
На этом этапе мы уходим от первопорядковой схемы индукции и добавляем единую аксиому индукции по множествам:
Благодаря наличию схемы свёртывания для арифметических формул, эта единственная аксиома автоматически влечёт за собой выполнимость индукции для всех арифметических формул. Так осуществляется переход от $PA$ к теории $ACA_0$ — переход консервативный: всякое арифметическое предложение, доказуемое в $ACA_0$, доказуемо уже в $PA$; отсюда и общий доказательный ординал $\varepsilon_0$.
Замена счётной схемы аксиом на одну-единственную аксиому — не техническая деталь, а смена логической формы самого принципа: схема в $PA$, аксиома в $Z_2$, теорема в $ZFC$. Эти формы, их взаимосвязи и точки, где равносильность ломается, разобраны в материале «О математической индукции».
Схему свёртывания можно расширить на вообще все формулы языка второго порядка, перейдя к импредикативной теории второго порядка $Z_2$. Важно отметить, что на данном этапе всё это по сути остаётся теорией первого порядка, но с двумя сортами переменных и предикатом принадлежности.
Будучи формальной системой, $Z_2$ в полной мере наследует «родовые пятна» первопорядковой арифметики. К ней применимы теоремы Гёделя о неполноте; по нисходящей теореме Лёвенгейма — Сколема у неё есть счётные модели — и ни одна из них не стандартна: второй сорт счётной модели заведомо не исчерпывает континуальный $\mathcal{P}(\mathbb{N})$. По теореме компактности существуют и модели с нестандартным числовым сортом.
Полнота исчисления здесь тоже первопорядковая: она достигается на общих (хенкиновских) моделях, где второй сорт — произвольное семейство, замкнутое относительно схемы свёртывания, а не настоящий булеан. Как из непротиворечивой теории строится такая модель, показано в материале «Конструкция Хенкина».
Принципиальный концептуальный сдвиг происходит при переходе к рассмотрению моделей. Мы можем наряду с формальной $Z_2$ рассматривать класс её стандартных моделей, в которых переменные по множествам интерпретируются элементами настоящего булеана натурального ряда $\mathcal{P}(\mathbb{N})$. Такая комбинация теории и ограничения на класс моделей является теоретико-модельной второпорядковой арифметикой.
Формальный дедуктивный аппарат у этих двух подходов общий, поэтому множество выводимых конечными доказательствами теорем совпадает. Однако в полной семантике стандартная модель уникальна с точностью до изоморфизма — это категоричность второпорядковой арифметики (по существу теорема Дедекинда, 1888), доказываемая в метатеории вроде $ZF$. Фиксация стандартной модели порождает полное, но неперечислимое множество истинных утверждений — полную теорию стандартной модели $\mathrm{Th}_2(\mathbb{N})$. Более того, $\mathrm{Th}_2(\mathbb{N})$ не определима в самом языке второго порядка — это второпорядковый вариант теоремы Тарского о неопределимости истины; для её определения нужен уже третий порядок. Человек способен выявлять истины, невыводимые формально в $Z_2$, исключительно за счёт выхода за пределы языка и использования внешних методов более сильных метатеорий (например, $ZFC$).
В $Z_2$ вещественные числа кодируются множествами натуральных (дедекиндовы сечения $\mathbb{Q}$, последовательности Коши и т. п.), поэтому квантор по множествам даёт после релятивизации и квантор «для любого вещественного $x$»: $\forall X\,(\mathrm{IsReal}(X) \to \dots)$. Одним множеством кодируется и целая последовательность вещественных чисел, так что счётные семейства тоже остаются внутри языка. Классический анализ — непрерывные функции, сходимость, борелевские множества — в $Z_2$ формализуется без перехода к высшим порядкам.
Ограничение $Z_2$ другое: теория не умеет непосредственно квантовать по произвольным множествам вещественных чисел (элементам $\mathcal{P}^2(\mathbb{N})$). Для несчётных семейств подмножеств $\mathbb{R}$, функциональных пространств в полном объёме и «третьего порядка» семантики нужны теории $PA_n$ с $n \ge 3$ (в литературе их чаще обозначают $Z_n$).
Насколько скромных средств хватает на анализ, точно измеряет обратная математика. Базовая теория меры Лебега строится уже над $RCA_0$, а счётная аддитивность меры на открытых множествах равносильна над $RCA_0$ системе $WWKL_0$ — «слабой слабой» лемме Кёнига: всякое поддерево $2^{<\mathbb{N}}$ положительной меры имеет бесконечный путь (Yu–Simpson, 1990). Это строго ниже $WKL_0$:
Иными словами, для меры Лебега не нужна даже $ACA_0$ — не говоря о полной $Z_2$.
Как и $Z_2$, теории $PA_n$ можно рассматривать в формальном (дедуктивном) или теоретико-модельном ключе.
Глобальной альтернативой наращиванию порядков является переход к теории с урэлементами ($ZFA$, она же $ZFU$; не путать с $ZFA$ в смысле анти-фундирования Акцеля). В этом случае $\mathbb{N}$ берётся как множество урэлементов, и над ним строится стандартная кумулятивная иерархия множеств. Это обеспечивает полную свободу для формулировок и доказательств любых фактов функционального анализа и топологии.
Атомарность базовой теории нужна здесь исключительно для того, чтобы заблокировать синтаксическую возможность писать $x \in \alpha$, где $\alpha$ — урэлемент. Таким образом теория отвязывается от специфики конкретного способа теоретико-множественного конструирования чисел.
Тот же приём — атомы вместо конструкции — применён на верхнем уровне в материале «Уровни формализации математического анализа», где кумулятивная иерархия строится уже над $\mathbb{R}$ как над множеством атомов; там же по шагам видно, что именно даёт и чего стоит каждый шаг вверх по выразительной силе.
В столбце «аксиоматика/теория» используются два разных понятия полноты. Аксиоматическая неполнота (Гёдель): у формальной системы есть неразрешимые предложения. Семантическая полнота теории: каждое предложение либо истинно, либо ложно в стандартной модели — это тривиально для любой фиксированной структуры и является следствием категоричности, а не достижением. Ни одна рекурсивная аксиоматика не совпадает с $\mathrm{Th}_2(\mathbb{N})$ — поэтому для теоретико-модельных строк ключевое свойство именно «не аксиоматизируема».
| Тип теории | Объекты и язык | Семантика и модели | Аксиоматика / теория | Выразительная сила |
|---|---|---|---|---|
| Первопорядковая ($PA$) | 1 сорт переменных (числа) | Модели первого порядка; нестандартные модели существуют (компактность)Лёвенгейм–Сколем даёт сверх того модели любой бесконечной мощности | Неполна (Гёдель) Перечислима |
Арифметика, рекурсивные функции, конечные объекты |
| $ACA_0$ | 2 сорта; схема свёртывания для арифметических ($\Sigma^0_k$) формул — без кванторов по множествам, но с параметрами обоих сортов; аксиома индукции (одна) | Общие (хенкиновские) модели; нестандартные модели существуют$\omega$-модели $ACA_0$ — в точности тьюринговы идеалы, замкнутые относительно скачка; наименьший из них — арифметические множества | Неполна (Гёдель) Перечислимаконсервативна над $PA$, ординал $\varepsilon_0$; узко предикативна, полный предикативный диапазон — до $ATR_0$ ($\Gamma_0$) |
Вещественные числа, непрерывные функции, борелевские множества; теоремы Больцано–Вейерштрасса, монотонной сходимости и др. эквивалентны $ACA_0$ над $RCA_0$ |
| Импредикативная ($Z_2$) | 2 сорта; полная схема свёртывания (любая формула); полная схема индукции — следствие свёртывания и одной аксиомы индукции | Общие (хенкиновские) модели; нестандартные модели существуют | Неполна (Гёдель) Перечислима |
Проективная иерархия, дескриптивная теория множеств; кванторы по отдельным вещественным и по их последовательностям, но не по произвольным семействам |
| Теоретико-модельная ($\mathrm{Th}_2(\mathbb{N})$) | 2 сорта; квантификация по $\mathcal{P}(\mathbb{N})$ в полном объёме | Стандартная семантика (полный булеан); единственна с точностью до изоморфизма (категорична) | Не аксиоматизируема Категорична → теория полнакаждое предложение решено в $\mathbb{N}$; ни одна рекурсивная теория не совпадает с $\mathrm{Th}_2(\mathbb{N})$ |
Истинная арифметика + классический анализ |
| $n$-порядковая ($\mathrm{Th}_n(\mathbb{N})$) | $n$ сортов переменных (числа, множества, множества множеств, …) | $\mathcal{P}^n(\mathbb{N})$; категорична для каждого фиксированного $n$ | Не аксиоматизируема Категорична → теория полнааналогично $\mathrm{Th}_2(\mathbb{N})$ |
Кванторы по семействам подмножеств $\mathbb{R}$, функциональные пространства, общая топология |
| $ZFA$ (с урэлементами) | Урэлементы ($\mathbb{N}$) + кумулятивная иерархия | Модели теории множеств с атомами | Неполна (Гёдель) Перечислимазависит от аксиоматики |
Современная математика без привязки к конструкции чисел |
Об $ACA$ и $ACA_0$. Нижний индекс 0 обозначает ограниченную индукцию: $ACA_0$ имеет только аксиому индукции (одну формулу в языке второго порядка), тогда как $ACA$ без индекса добавляет полную схему индукции второго порядка. Разница не косметическая: при одной и той же схеме свёртывания $ACA_0$ консервативна над $PA$ и имеет ординал $\varepsilon_0$, а у $ACA$ ординал уже $\varepsilon_{\varepsilon_0}$. Системы без индекса восходят к классическому предикативному анализу (Вейль, 1918; Крайзель, Феферман, Шютте, 1960-е); варианты с ограниченной индукцией и сам индекс 0 введены Фридманом (Friedman, Systems of second order arithmetic with restricted induction, 1976), а стандартом обратной математики их сделала книга Симпсона (SOSOA, 2-е изд., 2009; см. также Стилуэлл, 2018).
mathem.at · Н. И. Казимиров