Логика · Арифметика · Теория доказательств
Один и тот же принцип — «доказано для базы и для шага ⇒ доказано для всех» — принимает существенно разные логические формы в зависимости от языка и базовой теории: счётную схему аксиом в арифметике Пеано, единственную аксиому второго порядка в анализе, теорему в теории множеств. Здесь — путеводитель по этим формам, их взаимосвязям и границам; полные формулировки и доказательства — в PDF.
Индукция выглядит по-разному не потому, что математики каждый раз придумывают что-то новое, а потому, что выразительные возможности языка меняются: там, где нельзя квантифицировать по множествам, приходится довольствоваться схемой аксиом — отдельной аксиомой на каждую формулу.
В первопорядковом языке арифметики можно сформулировать пять на первый взгляд разных принципов. Часть из них равносильна друг другу уже в чистой логике, без единой арифметической аксиомы; другая часть требует минимальных фактов о последователе; связь с последним принципом — самая тонкая и метаматематически глубокая. Три сокращения, на которых всё держится:
Три горизонтальные группы диаграммы устроены принципиально по-разному: левая пара стрелок — факт чистой логики (с точностью до трихотомии порядка); средняя пара использует лишь минимальные факты о последователе \(S\); правая пара опирается уже на индукцию \(I\Delta_0\) и доказывается заметно сложнее (Paris–Kirby). Подробности каждого перехода — ниже и в PDF.
Ключевое наблюдение: эти три принципа равносильны друг другу уже в чистом исчислении предикатов — без единой арифметической аксиомы, — если только \(<\) — строгий линейный порядок (нужна лишь трихотомия: для любых \(x,y\) верно ровно одно из \(x{<}y\), \(x{=}y\), \(y{<}x\)).
(a) \(I^*_{\lnot\varphi}\iff D_\varphi\). Схема \(I^*\) для формулы \(\lnot\varphi\) имеет вид \(A\to B\), где \(A\equiv\forall x(\forall y{<}x\,\lnot\varphi(y)\to\lnot\varphi(x))\), \(B\equiv\forall x\,\lnot\varphi(x)\). По закону контрапозиции \(A\to B\iff\lnot B\to\lnot A\) — чистая тавтология. Раскрывая отрицания по де Моргану и двойственности кванторов, \(\lnot B\) — это \(X\ne\varnothing\), а \(\lnot A\) после ещё одной контрапозиции внутри — это в точности \(\lnot(\forall x\in X\,\exists y\in X\,(y{<}x))\), то есть заключение \(D_\varphi\).
(b) \(D_\varphi\iff L_\varphi\) — при трихотомии \(\lnot(y{<}x)\) означает «\(y{=}x\) или \(x{<}y\)», то есть ровно \(x\leqslant y\); формулы \(D\) и \(L\) после раскрытия внутреннего отрицания совпадают буквально.
Поскольку класс формул замкнут относительно \(\varphi\mapsto\lnot\varphi\), отсюда следует равносильность полных схем \(I^*\iff D\iff L\). Ни число \(0\), ни операция \(+1\) в доказательстве не используются — только линейность \(<\).
Связь \(I\) с тройкой \(I^*,L,D\) устроена иначе: она неотделима от последователя \(S\) и потому не может быть чисто логическим фактом. Нужны три элементарных аксиомы о согласовании \(<\) и \(S\) (обозначим их (O1)–(O3); вместе с рекурсивными уравнениями для \(+,\times,S\) они образуют теорию \(\mathsf{PA}^{\mathrm{rec}}_-\) — арифметику Робинсона в исходной рекурсивной форме):
Лемма. Из (O1)–(O3): \(\mathrm{Ind}(X)\to\mathrm{Prog}(X)\). Пусть \([0,x)\subseteq X\). По (O3) либо \(x{=}0\) (тогда \(x\in X\) по первому конъюнкту \(\mathrm{Ind}(X)\)), либо \(x{=}Sz\): тогда по (O2) \(z{<}Sz{=}x\), значит \(z\in[0,x)\subseteq X\), и по второму конъюнкту \(\mathrm{Ind}(X)\) получаем \(Sz{=}x\in X\).
\(I^*\Rightarrow I\). Из \(\mathrm{Ind}(X)\) по Лемме получаем \(\mathrm{Prog}(X)\); применяя \(I^*\), получаем \(\mathrm{Tot}(X)\). Аксиома (O3) используется здесь единственный раз — в разборе «\(x\) есть \(0\) или последователь».
\(I\Rightarrow I^*\) (без (O3)!). Пусть \(\mathrm{Prog}(X)\). Определим \(Y=\{x\mid[0,x)\subseteq X\}\) — максимальный начальный интервал внутри \(X\). Тогда \(Y\subseteq X\) сразу по определению \(\mathrm{Prog}(X)\). Далее \(\mathrm{Ind}(Y)\): база \(0\in Y\) — по (O1) \([0,0)=\varnothing\subseteq X\); шаг — если \(z\in Y\), то \(z\in X\) (по \(Y\subseteq X\)), и по (O2) \([0,Sz)=[0,z)\cup\{z\}\subseteq X\), то есть \(Sz\in Y\). Применяя \(I\) к \(Y\), получаем \(\mathrm{Tot}(Y)\), а вместе с \(Y\subseteq X\) — искомое \(\mathrm{Tot}(X)\).
Асимметрия здесь содержательна: направление \(I^*\Rightarrow I\) существенно использует все три аксиомы, причём именно (O3) — в разборе случаев; направление \(I\Rightarrow I^*\) обходится (O1)–(O2) и вовсе не использует (O3). Модель ниже показывает, что это не случайность.
Возьмём носителем ординал \(\omega+\omega\) — две последовательные копии \(\mathbb N\) с обычным порядком, но последователь определим отдельно внутри каждой копии: \(S(n)=n{+}1\) в первой, \(S(\omega{+}n)=\omega{+}n{+}1\) во второй. Функция \(S\) всюду определена и инъективна, (O1)–(O2) выполнены — но элемент \(\omega\) не есть \(S(y)\) ни для какого \(y\): это ровно то место, где ломается (O3).
Множество \(X\) = «первая копия \(\mathbb N\)» удовлетворяет \(\mathrm{Ind}(X)\) (содержит 0, замкнуто относительно \(S\)), но \(X\ne\omega{+}\omega\) — значит \(I\) для этого \(X\) не выполнено. При этом \(\omega+\omega\) — честный ординал (вполне упорядоченное множество), так что трансфинитная индукция верна в нём для произвольных подмножеств носителя — а значит \(I^*\) (и вместе с ним \(L\), \(D\)) здесь выполняются, причём в подлинно втором порядке, без всяких оговорок про схему.
Нет: существуют нестандартные модели \(\mathsf{PA}\), в которых полная схема \(I\) (а с ней и \(I^*,L,D\) как схемы) выполнена, но сама модель, если смотреть на неё извне, вполне упорядоченной не является — в ней есть (неопределимые в языке \(\mathsf{PA}\)) подмножества без наименьшего элемента. Противоречия нет: как схема аксиом, \(I^*\) гарантирует наименьший элемент лишь для подмножеств, определимых формулой языка \(\mathsf{PA}\); на «неправильные» подмножества нестандартной модели схема просто не распространяется. В примере выше \(I^*\) законно потребована для абсолютно всех подмножеств именно потому, что \(\omega+\omega\) по построению стандартна.
Связь \(B\) с \(I\) не сводится ни к чистой логике, ни к минимальной арифметике последователя. Внутри слабой базовой теории \(\mathsf{PA}^-\) (аксиомы дискретного упорядоченного полукольца без индукции) схема \(B\) сама по себе не влечёт \(I\). Но относительно базовой индукции \(I\Delta_0\) связь восстанавливается и образует строгую иерархию (Paris–Kirby, 1978):
а на уровне полных схем — \(I\iff B\) относительно базы \(I\Delta_0\). Доказательство этого перехода заметно сложнее двух предыдущих и не приводится здесь целиком — полностью оно разобрано в PDF.
Ниже — набор утверждений, чья доказуемость существенно завязана на силу индукции: одни требуют лишь самой слабой её формы, другие независимы от полной схемы \(I\) арифметики Пеано. Статус указан в терминах подсистем арифметики (\(I\Sigma_n\), \(I\Delta_0\)) и обратной математики (\(\mathsf{RCA}_0\), \(\mathsf{WKL}_0\), \(\mathsf{ACA}_0\), \(\mathsf{ATR}_0\)).
| Утверждение | Статус доказуемости |
|---|---|
| Принцип Дирихле (Pigeonhole) |A|>|B| ⇒ нет инъекции A→B | не в \(I\Delta_0\) Paris–Wilkie–Woods, Ajtai (1988): не доказуем даже для \(\Delta_0\)-определимых функций — демонстрирует крайнюю слабость \(I\Delta_0\). |
| Лемма Кёнига о бесконечном пути бесконечное конечно-ветвящееся дерево содержит бесконечный путь | ≡ \(\mathsf{WKL}_0\) для бинарных деревьев (⇔ компактность отрезка); ≡ \(\mathsf{ACA}_0\) для произвольных — строго сильнее. Разница возникает не из индукции (схема одна и та же в обеих системах), а из схемы свёртывания. |
| Коммутативность и ассоциативность \(+\), \(\times\) | Доказуемы в \(\mathsf{PA}\) индукцией. Без неё (в \(\mathsf{PA}^{\mathrm{rec}}_-\)) существуют нестандартные модели с некоммутативным сложением — как и в арифметике ординалов, где \(\omega{+}1\ne1{+}\omega\). |
| Конечные множества по Дедекинду B⊊A конечно ⇒ |B|<|A|; станд. конечно ⇔ дед.-конечно | Первое — прямое следствие индукции. Направление «станд. конечно ⇒ дед.-конечно» — тоже. Обратное требует счётного выбора \(\mathsf{AC}_\omega\) (лишь следствие, не равносильность); без выбора в \(\mathsf{ZF}\) — недоказуемо (модели Френкеля–Мостовского, первая модель Коэна дают бесконечные дед.-конечные множества). |
| Теорема Рамсея \(RT^2_2\) конечный случай — «теорема о вечеринке», R(k,m); бесконечный — RT²₂ | Конечный случай — индукция по \(k{+}m\). Бесконечный — прямое следствие принципа \(L\); точная сила \(\mathsf{RCA}_0{+}I\Sigma_2\), но сам \(RT^2_2\) не влечёт \(I\Sigma_2\) (Cholak–Jockusch–Slaman, 2001). |
| Тотальность функции Аккермана | не в \(I\Sigma_1\) (теорема Парсонса: \(I\Sigma_1\)-доказуемо-рекурсивные функции = примитивно рекурсивные) → доказуема в \(I\Sigma_2\) — соответствует месту функции Аккермана на уровне \(\omega\) быстрорастущей иерархии. |
| Теорема Гудстейна (1944) и принцип Пэриса–Харрингтона (1977) истинные \(\Pi_2\)- и комбинаторные предложения языка \(\mathsf{PA}\) | не в \(\mathsf{PA}\) (Kirby–Paris, 1982; Paris–Harrington, 1977) — но доказуемы уже трансфинитной индукцией вдоль \(\varepsilon_0\) в \(\mathsf{ATR}_0\). Ординал \(\varepsilon_0\) — доказательно-теоретический ординал \(\mathsf{PA}\) (Генцен, 1936): граница, которую схема \(I\) не может формализовать сама по себе. |
Последняя строка отмечает предел мощности локальной/возвратной индукции \(I\iff I^*\): при всей продемонстрированной выше силе, они не замкнуты относительно всех истинных арифметических утверждений. Принцип Пэриса–Харрингтона примечателен ещё и тем, что стал первым примером натуральной (не метаматематической по формулировке) теоремы, чья независимость от \(\mathsf{PA}\) была обнаружена одновременно с самой теоремой.