Введение

Отрасль математической логики

Обратная математика — это программа в математической логике, направленная на определение того, какие аксиомы необходимы для доказательства теорем математики. Её определяющий метод можно кратко описать как «движение от теорем к аксиомам», в отличие от обычной математической практики вывода теорем из аксиом. Это можно представить как выделение необходимых условий из достаточных. Программа обратной математики была предвосхищена результатами в теории множеств, такими как классическая теорема об эквивалентности аксиомы выбора и леммы Зорна в теории множеств ZF. Однако целью обратной математики является изучение возможных аксиом для обычных теорем математики, а не возможных аксиом для теории множеств. Обратная математика обычно проводится с использованием подсистем арифметики второго порядка, где многие её определения и методы вдохновлены предыдущими работами в конструктивном анализе и теории доказательств. Использование арифметики второго порядка также позволяет применять многие методы из теории рекурсии; многие результаты в обратной математике имеют соответствующие результаты в вычислимом анализе. В обратной математике высшего порядка основное внимание уделяется подсистемам арифметики высшего порядка и связанному с ними более развитому языку. Программа была основана и развита Стивеном Симпсоном. Стандартным справочником по этой теме является , а введением для неспециалистов — . Введение в обратную математику высшего порядка, а также основополагающая работа, — .

Общие принципы

В обратной математике начинают с языка рамки и базовой теории — основной аксиоматической системы, которая слишком слаба для доказательства большинства интересующих теорем, но всё же достаточно мощна для разработки определений, необходимых для формулирования этих теорем. Например, для изучения теоремы «Каждая ограниченная последовательность вещественных чисел имеет супремум» необходимо использовать базовую систему, которая оперирует вещественными числами и последовательностями вещественных чисел. Для каждой теоремы, которую можно сформулировать в базовой системе, но нельзя доказать в ней, цель состоит в том, чтобы определить конкретную аксиоматическую систему (более сильную, чем базовая), необходимую для доказательства этой теоремы. Чтобы показать, что система S необходима для доказательства теоремы T, требуются два доказательства. Первое доказательство показывает, что T доказуема из S; это обычное математическое доказательство с обоснованием возможности его проведения в системе S. Второе доказательство, известное как обращение, показывает, что сама T влечёт S; это доказательство проводится в базовой системе. Например, базовая теория обратной математики высшего порядка, называемая , доказывает те же предложения, что и RCA0, вплоть до языка. Как отмечалось в предыдущем абзаце, аксиомы полноты второго порядка легко обобщаются на рамку высшего порядка. Однако теоремы, выражающие компактность основных пространств, ведут себя совершенно по-разному в арифметике второго и высшего порядка: с одной стороны, при ограничении счётными покрытиями / языком арифметики второго порядка, компактность единичного интервала доказуема в WKL0 из следующего раздела. С другой стороны, при рассмотрении несчётных покрытий / языка арифметики высшего порядка, компактность единичного интервала доказуема только из (полной) арифметики второго порядка. Другие леммы о покрытиях (например, Линделёфа, Витали, Бесиковича и т. д.) демонстрируют такое же поведение, и многие основные свойства интеграла Лебега-Стильтьеса эквивалентны компактности базового пространства.

Пять основных подсистем арифметики второго порядка

Арифметика второго порядка — это формальная теория натуральных чисел и множеств натуральных чисел. Многие математические объекты, такие как счетные кольца, группы и поля, а также точки в эффективных польских пространствах, могут быть представлены как множества натуральных чисел, и посредством этого представления могут изучаться в арифметике второго порядка. Обратная математика использует несколько подсистем арифметики второго порядка. Типичная теорема обратной математики показывает, что конкретная математическая теорема T эквивалентна конкретной подсистеме S арифметики второго порядка относительно более слабой подсистемы B. Эта более слабая система B известна как базовая система для данного результата; чтобы результат обратной математики имел смысл, эта система сама не должна быть способна доказать математическую теорему T. описывает пять конкретных подсистем арифметики второго порядка, которые он называет «Большой пятеркой», часто встречающихся в обратной математике. В порядке возрастания силы эти системы обозначаются аббревиатурами RCA0, WKL0, ACA0, ATR0 и ΠCA0. Следующая таблица суммирует системы «Большой пятерки» и перечисляет соответствующие системы в арифметике высшего порядка. с.40 Любую частичную функцию можно расширить до полной функции. Различные теоремы в комбинаторике, такие как определенные формы теоремы Рамсея.

ω-модели и β-модели

Модель ω в ω представляет собой множество неотрицательных целых чисел (или конечных ординалов). Модель ω — это модель фрагмента арифметики второго порядка, чья часть первого порядка является стандартной моделью арифметики Пеано, но чья часть второго порядка может быть нестандартной. Более точно, модель ω задается выбором подмножеств множества натуральных чисел. Переменные первого порядка интерпретируются обычным образом как элементы этого множества, а операции + и · сохраняют свои обычные значения, в то время как переменные второго порядка интерпретируются как элементы множества всех подмножеств натуральных чисел. Существует стандартная модель ω, в которой множество подмножеств принимается равным множеству всех подмножеств целых чисел. Однако существуют и другие модели ω; например, RCA0 имеет минимальную модель ω, в которой множество подмножеств состоит из рекурсивных подмножеств натуральных чисел. Модель β — это ω-модель, которая согласуется со стандартной ω-моделью относительно истинности Σ₀- и Π₀-предложений (с параметрами). Не-ω-модели также полезны, особенно в доказательствах теорем об относительной непротиворечивости.