От первопорядковой $PA$ через $ACA_0$ и импредикативную $Z_2$ к теоретико-множественной $ZFA$: язык, модели, выразительная сила.
Построение второпорядковой теории начинается с фиксации первопорядковой базы. К стандартному языку добавляется второй сорт переменных — переменные по множествам индивидной области ($X, Y, Z, \dots$). В сигнатуру вводится предикат принадлежности $x \in X$, где $x$ — индивид, а $X$ — множество. Также автоматически постулируется аксиома экстенсиональности (равенства) для множеств.
Такое расширение языка порождает строгую иерархию формул. На нижнем уровне находятся чисто первопорядковые формулы. База расширяется классом арифметических формул — в обозначениях арифметической иерархии это классы $\Sigma^0_k$ и $\Pi^0_k$ (их не следует путать с $\Sigma^1_k$ аналитической иерархии): они могут содержать переменные-множества в качестве параметров, но не допускают квантификации по множествам. Выше располагается аналитическая иерархия — собственно второпорядковые формулы с кванторами по множествам ($\Sigma^1_k$, $\Pi^1_k$, …).
Фундаментальный шаг в построении теории — добавление схемы свертывания, гарантирующей существование множеств, заданных формулами. Если ограничить эту схему арифметическими формулами, получается теория $ACA_0$. Свёртывание здесь узко предикативно: определение множества не опирается на кванторы по множествам и не требует «перебирать» universum, к которому принадлежит само определяемое множество.
В более широком смысле предикативной математики (Вейль, Феферман, Шютте) допустимые системы простираются до $ATR_0$ (ординал доказательности $\Gamma_0$) — существенно выше $ACA_0$ (ординал $\varepsilon_0$). $ACA_0$ — лишь нижняя ступень этого диапазона, хотя именно она часто служит точкой входа в обратную математику.
На этом этапе мы уходим от первопорядковой схемы индукции и добавляем единую аксиому индукции по множествам:
Благодаря наличию схемы свёртывания для арифметических формул, эта единственная аксиома автоматически влечёт за собой выполнимость индукции для всех арифметических формул. Так осуществляется переход от $PA$ к теории $ACA_0$.
Схему свертывания можно расширить на вообще все формулы языка второго порядка, перейдя к импредикативной теории второго порядка $Z_2$. Важно отметить, что на данном этапе всё это по сути остается теорией первого порядка, но с двумя сортами переменных и предикатом принадлежности.
Будучи формальной системой, $Z_2$ в полной мере наследует «родовые пятна» первопорядковой арифметики: для нее справедливы теоремы Гёделя о неполноте и теорема Лёвенгейма — Скулема о существовании счетных нестандартных моделей.
Принципиальный концептуальный сдвиг происходит при переходе к рассмотрению моделей. Мы можем наряду с формальной $Z_2$ рассматривать класс ее стандартных моделей, в которых переменные по множествам интерпретируются элементами настоящего булеана натурального ряда $\mathcal{P}(\mathbb{N})$. Такая комбинация теории и ограничения на класс моделей является теоретико-модельной второпорядковой арифметикой.
Формальный дедуктивный аппарат у этих двух подходов общий, поэтому множество выводимых конечными доказательствами теорем совпадает. Однако в рамках $ZF$ стандартная модель уникальна с точностью до изоморфизма (тотальная категоричность). Фиксация стандартной модели порождает полное, но неперечислимое множество истинных утверждений — элементарную теорию стандартной модели $\mathrm{Th}_2(\mathbb{N})$. Человек способен выявлять истины, невыводимые формально в $Z_2$, исключительно за счет выхода за пределы языка и использования внешних методов более сильных метатеорий (например, $ZFC$).
В $Z_2$ вещественные числа кодируются множествами натуральных (дедекиндовы сечения $\mathbb{Q}$, последовательности Коши и т.п.), поэтому второпорядковые кванторы по множествам — это как раз кванторы «для любого вещественного $x$» ($\forall X\;(IsReal(X) \to \dots)$). Классический анализ — непрерывные функции, сходимость, борелевские множества — в $Z_2$ формализуется без перехода к высшим порядкам.
Ограничение $Z_2$ другое: теория не умеет непосредственно квантовать по множествам вещественных чисел (элементам $\mathcal{P}^2(\mathbb{N})$). Для произвольных семейств подмножеств $\mathbb{R}$, функциональных пространств в полном объёме и «третьего порядка» семантики нужны теории $PA_n$ с $n \ge 3$. Базовая теория меры Лебега на $\mathbb{R}$ (включая счётную аддитивность) по результатам обратной математики формализуется уже в слабых подсистемах вроде $WWKL_0$, слабее $ACA_0$; $Z_2$ для этого более чем достаточна.
Как и $Z_2$, теории $PA_n$ можно рассматривать в формальном (дедуктивном) или теоретико-модельном ключе.
Глобальной альтернативой наращиванию порядков является переход к теории с урэлементами ($ZFA$). В этом случае $\mathbb{N}$ берется как множество урэлементов, и над ним строится стандартная кумулятивная иерархия множеств. Это обеспечивает полную свободу для формулировок и доказательств любых фактов функционального анализа и топологии.
Атомарность базовой теории нужна здесь исключительно для того, чтобы заблокировать синтаксическую возможность писать $x \in \alpha$, где $\alpha$ — урэлемент. Таким образом теория отвязывается от специфики конкретного способа теоретико-множественного конструирования чисел.
В столбце «аксиоматика/теория» используются два разных понятия полноты. Аксиоматическая неполнота (Гёдель): у формальной системы есть неразрешимые предложения. Семантическая полнота теории: каждое предложение либо истинно, либо ложно в стандартной модели — это тривиально для любой фиксированной структуры и является следствием категоричности, а не достижением. Ни одна рекурсивная аксиоматика не совпадает с $\mathrm{Th}_2(\mathbb{N})$ — поэтому для теоретико-модельных строк ключевое свойство именно «не аксиоматизируема».
| Тип теории | Объекты и язык | Семантика и модели | Аксиоматика / теория | Выразительная сила |
|---|---|---|---|---|
| Первопорядковая ($PA$) | 1 сорт переменных (числа) | Модели первого порядка; нестандартные модели существуют (Лёвенгейм–Сколем) | Неполна (Гёдель) Перечислима |
Арифметика, рекурсивные функции, конечные объекты |
| $ACA_0$ | 2 сорта; схема свёртывания для арифметических ($\Sigma^0_k$) формул; аксиома индукции (одна) | Семантика Хенкина; нестандартные модели существуютпо Гёделю / Лёвенгейму–Скулему | Неполна (Гёдель) Перечислимадоказательная сила = $PA$, ordinal $\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 обозначает ограниченную индукцию (Симпсон 2009): $ACA_0$ имеет только аксиому индукции (одну формулу в языке второго порядка), тогда как $ACA$ (без индекса) — исторически более ранняя система (Феферман, 1977) — добавляет полную схему индукции второго порядка. Системы без нижнего индекса имеют существенно бо́льший доказательный ordinal при той же схеме свёртывания. В обратной математике (Стилуэлл, Симпсон) стандартом стали именно варианты с индексом 0.
mathem.at · Н. И. Казимиров
English version