Введение

Математическая система
В математической логике арифметика второго порядка представляет собой совокупность аксиоматических систем, формализующих натуральные числа и их подмножества. Она является альтернативой аксиоматической теории множеств в качестве основания для значительной, но не всей математики. Предшественник арифметики второго порядка, включающий параметры третьего порядка, был предложен Давидом Гильбертом и Полом Бернейсом в их книге «Grundlagen der Mathematik». Стандартная аксиоматизация арифметики второго порядка обозначается Z2. Арифметика второго порядка включает в себя, но значительно сильнее, чем её аналог первого порядка – арифметика Пеано. В отличие от арифметики Пеано, арифметика второго порядка допускает квантификацию по множествам натуральных чисел, а также по самим числам. Поскольку действительные числа могут быть представлены как (бесконечные) множества натуральных чисел известными способами, и поскольку арифметика второго порядка допускает квантификацию по таким множествам, возможно формализовать действительные числа в арифметике второго порядка. По этой причине арифметика второго порядка иногда называется «анализом». Арифметика второго порядка также может рассматриваться как слабая версия теории множеств, в которой каждый элемент является либо натуральным числом, либо множеством натуральных чисел. Хотя она намного слабее теории множеств Цермело — Френкеля, арифметика второго порядка может доказать практически все результаты классической математики, выразимые на её языке. Подсистема арифметики второго порядка — это теория на языке арифметики второго порядка, каждая аксиома которой является теоремой полной арифметики второго порядка (Z2). Такие подсистемы необходимы для обратной математики — исследовательской программы, изучающей, какая часть классической математики может быть выведена в определенных слабых подсистемах различной мощности. Значительная часть базовой математики может быть формализована в этих слабых подсистемах, некоторые из которых определены ниже. Обратная математика также проясняет степень и характер неконструктивности классической математики.

Синтаксис

Язык арифметики второго порядка двухсортный. Первый сорт термов, и в частности переменных, обычно обозначаемых строчными буквами, состоит из индивидов, которые интерпретируются как натуральные числа. Другой сорт переменных, называемых "переменными множеств", "переменными классов" или даже "предикатами", обычно обозначается прописными буквами. Они относятся к классам/предикатам/свойствам индивидов и могут рассматриваться как множества натуральных чисел. Как индивиды, так и переменные множеств могут быть подвергнуты универсальной или экзистенциальной квантификации. Формула, не содержащая связанных переменных множеств (то есть не содержащая кванторов над переменными множеств), называется арифметической. Арифметическая формула может содержать свободные переменные множеств и связанные индивидуальные переменные. Индивидуальные термы формируются из константы 0, унарной функции S (функции следования) и бинарных операций + и ⋅ (сложения и умножения). Функция следования прибавляет 1 к своему аргументу. Отношения = (равенство) и < (сравнение натуральных чисел) связывают два индивида, в то время как отношение ∈ (принадлежность) связывает индивида и множество (или класс). Таким образом, в обозначениях язык арифметики второго порядка задается сигнатурой. Например, является корректно сформированной формулой арифметики второго порядка, которая является арифметической, имеет одну свободную переменную множества X и одну связанную индивидуальную переменную n (но не содержит связанных переменных множеств, как того требует арифметическая формула), в то время как является корректно сформированной формулой, которая не является арифметической, поскольку содержит одну связанную переменную множества X и одну связанную индивидуальную переменную n.

Семантика

Возможно несколько различных интерпретаций кванторов. Если арифметика второго порядка изучается с использованием полной семантики логики второго порядка, то кванторы множеств варьируются по всем подмножествам области значений индивидуальных переменных. Если арифметика второго порядка формализуется с использованием семантики логики первого порядка (семантики Хенкина), то любая модель включает в себя область определения для переменных множеств, и эта область может быть собственным подмножеством полного множества степеней области индивидуальных переменных.

Полная система

Формальная теория арифметики второго порядка (на языке арифметики второго порядка) состоит из основных аксиом, аксиомы выделения по формуле для каждой формулы φ (арифметической или любой другой), и аксиомы индукции второго порядка. Эту теорию иногда называют полной арифметикой второго порядка, чтобы отличать её от её подсистем, определяемых ниже. Поскольку полная семантика арифметики второго порядка подразумевает существование любого возможного множества, аксиомы выделения по формуле могут рассматриваться как часть дедуктивной системы при использовании полной семантики арифметики второго порядка.

Модели

В этом разделе описывается арифметика второго порядка с семантикой первого порядка. Таким образом, модель языка арифметики второго порядка состоит из множества M (которое является областью значений индивидуальных переменных) вместе с константой 0 (элементом M), функцией S, отображающей M в M, двух бинарных операций + и · на M, бинарного отношения < на M и семейства D подмножеств M, которое является областью значений переменных множеств. Исключение D дает модель языка арифметики первого порядка. Если D является полным множеством степеней M, то модель называется полной моделью. Использование полной семантики второго порядка эквивалентно ограничению моделей арифметики второго порядка полными моделями. Фактически, аксиомы арифметики второго порядка имеют только одну полную модель. Это следует из того факта, что аксиомы Пеано вместе с аксиомой индукции второго порядка имеют только одну модель при семантике второго порядка.

Определяемые функции

Функции первого порядка, доказуемо тотальные в арифметике второго порядка, совпадают ровно с теми, которые представимы в системе F. Почти эквивалентно, система F является теорией функционалов, соответствующих арифметике второго порядка, подобно тому, как система Т Гёделя соответствует арифметике первого порядка в интерпретации Диалектики.

Арифметическое понимание

Многие из хорошо изученных подсистем связаны со свойствами замкнутости моделей. Например, можно показать, что каждая ω-модель полной арифметики второго порядка замкнута относительно прыжка Тьюринга, но не каждая ω-модель, замкнутая относительно прыжка Тьюринга, является моделью полной арифметики второго порядка. Подсистема ACA0 включает в себя достаточно аксиом, чтобы отразить понятие замкнутости относительно прыжка Тьюринга. ACA0 определяется как теория, состоящая из основных аксиом, схемы аксиом арифметического выделения (иными словами, аксиомы выделения для каждой арифметической формулы φ) и аксиомы обычной индукции второго порядка. Было бы эквивалентно включить всю схему аксиом арифметической индукции, другими словами, включить аксиому индукции для каждой арифметической формулы φ. Можно показать, что множество S подмножеств ω определяет ω-модель ACA0 тогда и только тогда, когда S замкнуто относительно прыжка Тьюринга, редуцируемости Тьюринга и соединения Тьюринга. Индекс 0 в ACA0 указывает, что не каждый экземпляр схемы аксиом индукции включен в эту подсистему. Это не имеет значения для ω-моделей, которые автоматически удовлетворяют каждому экземпляру аксиомы индукции. Однако это важно при изучении не-ω-моделей. Система, состоящая из ACA0 плюс индукция для всех формул, иногда называется ACA без индекса. Система ACA0 является консервативным расширением арифметики первого порядка (или аксиом Пеано первого порядка), определяемой как основные аксиомы, плюс схема аксиом индукции первого порядка (для всех формул φ, не содержащих никаких классовых переменных, связанных или несвязанных), на языке арифметики первого порядка (который не допускает классовых переменных вообще). В частности, она имеет тот же теоретико-доказательный ординал ε0, что и арифметика первого порядка, благодаря ограниченной схеме индукции.

Рекурсивное понимание

Подсистема RCA0 является более слабой системой, чем ACA0, и часто используется в качестве базовой системы в обратной математике. Она состоит из: основных аксиом, схемы индукции Σ01 и схемы понимания Δ01. Первый термин понятен: схема индукции Σ01 представляет собой аксиому индукции для каждой формулы Σ01 φ. Термин "понимание Δ01" более сложен, поскольку не существует формул Δ01. Вместо этого схема понимания Δ01 утверждает аксиому понимания для каждой формулы Σ01, логически эквивалентной формуле Π01. Эта схема включает, для каждой формулы Σ01 φ и каждой формулы Π01 ψ, аксиому:

Множество следствий первого порядка из RCA0 совпадает с множеством следствий подсистемы IΣ1 арифметики Пеано, в которой индукция ограничена формулами Σ01. В свою очередь, IΣ1 является консервативным расширением примитивной рекурсивной арифметики (PRA) для формул. Более того, доказательно-теоретический ординал IΣ1 равен ωω, как и у PRA. Можно показать, что коллекция S подмножеств ω определяет ω-модель RCA0 тогда и только тогда, когда S замкнута относительно редуцируемости Тьюринга и Тьюрингова объединения. В частности, коллекция всех вычислимых подмножеств ω дает ω-модель RCA0. Это и является обоснованием названия этой системы: если существование множества может быть доказано с помощью RCA0, то это множество является рекурсивным (т.е. вычислимым).

Более слабые системы

Иногда требуется система, ещё более слабая, чем RCA0. Одна из таких систем определяется следующим образом: сначала язык арифметики дополняется символом экспоненциальной функции (в более сильных системах экспоненту можно определить через сложение и умножение стандартным приёмом, но когда система становится слишком слабой, это становится невозможным) и базовые аксиомы – очевидными аксиомами, определяющими возведение в степень индуктивно на основе умножения; затем система состоит из (обогащённых) базовых аксиом, плюс Δ01-понимание, плюс Δ00-индукция.

Более сильные системы

По ACA0, каждая формула арифметики второго порядка эквивалентна формуле Σ1n или Π1n для всех достаточно больших n. Система понимания Π11 — это система, состоящая из основных аксиом, плюс обычная аксиома индукции второго порядка и аксиома понимания для каждой (полужирной) формулы Π11 φ. Это эквивалентно пониманию Σ11 (с другой стороны, понимание Δ11, определенное аналогично пониманию Δ01, слабее).

Проективная определённость

Проективная детерминация — это утверждение о том, что любая двухместная игра с полной информацией, ходы в которой являются натуральными числами, длиной ω и проективным множеством выигрышей, является детерминированной, то есть у одного из игроков есть выигрышная стратегия. (Первый игрок выигрывает игру, если ход принадлежит множеству выигрышей; в противном случае выигрывает второй игрок.) Множество является проективным тогда и только тогда, когда (как предикат) оно выразимо формулой на языке арифметики второго порядка, допускающей вещественные числа в качестве параметров, поэтому проективная детерминация выразима как схема на языке Z2. Многие естественные утверждения, выразимые на языке арифметики второго порядка, независимы от Z2 и даже ZFC, но доказуемы из проективной детерминации. Примеры включают коаналитическое свойство совершенного подмножества, измеримость и свойство Баира для множеств, униформизацию и т. д. В сравнении со слабой базовой теорией (такой как RCA0), проективная детерминация влечет за собой аксиому понимания и обеспечивает по существу полную теорию арифметики второго порядка — естественные утверждения на языке Z2, которые независимы от Z2 с проективной детерминацией, найти сложно. ZFC + {существует n кардиналов Вуддина: n — натуральное число} является консервативным расширением Z2 с проективной детерминацией, то есть утверждение на языке арифметики второго порядка доказуемо в Z2 с проективной детерминацией тогда и только тогда, когда его перевод на язык теории множеств доказуем в ZFC + {существует n кардиналов Вуддина: n ∈ N}.

Кодирование математики

Арифметика второго порядка непосредственно формализует натуральные числа и множества натуральных чисел. Однако она способна формализовать другие математические объекты косвенно, посредством методов кодирования, что было впервые отмечено Вейлем. Целые числа, рациональные числа и действительные числа могут быть формализованы в подсистеме RCA0, вместе с полными сепарабельными метрическими пространствами и непрерывными функциями между ними. Исследовательская программа обратной математики использует эти формализации математики в арифметике второго порядка для изучения аксиом существования множеств, необходимых для доказательства математических теорем. Например, теорема о промежуточном значении для функций от действительных чисел к действительным числам доказуема в RCA0, в то время как теорема Болцано — Вейерштрасса эквивалентна ACA0 относительно RCA0. Упомянутое кодирование хорошо работает для непрерывных и тотальных функций при условии наличия теории основания более высокого порядка и слабой леммы Кёнига. Как и следовало ожидать, в случае топологии кодирование не лишено проблем.