Обратная математика

Для проверки этой статьи нужны дополнительные цитаты . Помогите улучшить эту статью , добавив ссылки на надежные источники . Неподтвержденный материал может быть оспорен и удален. Найти источники:  «Обратная математика» – новости  · газеты  · книги  · ученый  · JSTOR ( октябрь 2016 г. ) ( Узнайте, как и когда удалять это сообщение )

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

Обратная математика — это программа в математической логике , которая стремится определить, какие аксиомы требуются для доказательства теорем математики. Ее определяющий метод можно кратко описать как «возвращение от теорем к аксиомам », в отличие от обычной математической практики вывода теорем из аксиом. Ее можно концептуализировать как вылепливание необходимых условий из достаточных .

Программа обратной математики была предвосхищена результатами в теории множеств, такими как классическая теорема о том, что аксиома выбора и лемма Цорна эквивалентны над теорией множеств ZF . Целью обратной математики, однако, является изучение возможных аксиом обычных теорем математики, а не возможных аксиом для теории множеств.

Обратная математика обычно выполняется с использованием подсистем арифметики второго порядка , ^[1] где многие из ее определений и методов вдохновлены предыдущей работой в конструктивном анализе и теории доказательств . Использование арифметики второго порядка также позволяет использовать многие методы из теории рекурсии ; многие результаты в обратной математике имеют соответствующие результаты в вычислимом анализе . В обратной математике более высокого порядка основное внимание уделяется подсистемам арифметики более высокого порядка и связанному с ними более богатому языку. ^{[ необходимо разъяснение ]}

Программа была основана Харви Фридманом  (1975, 1976) ^[2] и выдвинута Стивом Симпсоном . Стандартная ссылка на предмет — Simpson (2009), в то время как введение для неспециалистов — Stillwell (2018). Введение в обратную математику высшего порядка, а также основополагающая статья — Kohlenbach (2005). Подробное введение, охватывающее основные результаты и методы, — Dzhafarov & Mummert (2022) ^[3]

В обратной математике все начинается с языка-фреймворка и базовой теории — базовой системы аксиом, которая слишком слаба, чтобы доказать большинство теорем, которые могут вас заинтересовать, но все еще достаточно мощна, чтобы разработать определения, необходимые для формулировки этих теорем. Например, чтобы изучить теорему «Каждая ограниченная последовательность действительных чисел имеет супремум », необходимо использовать базовую систему, которая может говорить о действительных числах и последовательностях действительных чисел.

Для каждой теоремы, которая может быть сформулирована в базовой системе, но не доказуема в базовой системе, целью является определение конкретной системы аксиом (более сильной, чем базовая система), которая необходима для доказательства этой теоремы. Чтобы показать, что система S требуется для доказательства теоремы T , требуются два доказательства. Первое доказательство показывает, что T доказуема из S ; это обычное математическое доказательство вместе с обоснованием того, что оно может быть выполнено в системе S. Второе доказательство, известное как обращение , показывает, что само T подразумевает S ; это доказательство выполняется в базовой системе. ^[1] Обращение устанавливает, что никакая система аксиом S′ , которая расширяет базовую систему, не может быть слабее S, при этом все еще доказывая  T.

Большинство исследований в области обратной математики сосредоточены на подсистемах арифметики второго порядка . Совокупность исследований в области обратной математики установила, что слабые подсистемы арифметики второго порядка достаточны для формализации почти всей математики на уровне бакалавриата. В арифметике второго порядка все объекты могут быть представлены либо как натуральные числа , либо как наборы натуральных чисел. Например, чтобы доказать теоремы о действительных числах, действительные числа могут быть представлены как последовательности Коши рациональных чисел , каждая из которых последовательности может быть представлена ​​как набор натуральных чисел.

Системы аксиом, которые чаще всего рассматриваются в обратной математике, определяются с помощью схем аксиом, называемых схемами понимания . Такая схема утверждает, что существует любой набор натуральных чисел, определяемый формулой заданной сложности. В этом контексте сложность формул измеряется с помощью арифметической иерархии и аналитической иерархии .

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

Другим эффектом использования арифметики второго порядка является необходимость ограничения общих математических теорем формами, которые могут быть выражены в рамках арифметики. Например, арифметика второго порядка может выразить принцип «Каждое счетное векторное пространство имеет базис», но не может выразить принцип «Каждое векторное пространство имеет базис». На практике это означает, что теоремы алгебры и комбинаторики ограничены счетными структурами, в то время как теоремы анализа и топологии ограничены сепарабельными пространствами . Многие принципы, подразумевающие аксиому выбора в их общей форме (например, «Каждое векторное пространство имеет базис»), становятся доказуемыми в слабых подсистемах арифметики второго порядка, когда они ограничены. Например, «каждое поле имеет алгебраическое замыкание» не доказуемо в теории множеств ZF, но ограниченная форма «каждое счетное поле имеет алгебраическое замыкание» доказуема в RCA ₀ , самой слабой системе, обычно используемой в обратной математике.

Недавнее направление исследований обратного порядка в математике высшего порядка , начатое Ульрихом Коленбахом в 2005 году, фокусируется на подсистемах арифметики высшего порядка . ^[4] Благодаря более богатому языку арифметики высшего порядка использование представлений (иначе называемых «кодами»), распространенных в арифметике второго порядка, значительно сокращено. Например, непрерывная функция в пространстве Кантора — это просто функция, которая отображает двоичные последовательности в двоичные последовательности, и которая также удовлетворяет обычному определению непрерывности «эпсилон-дельта».

Обратная математика высшего порядка включает в себя версии высшего порядка схем понимания (второго порядка). Такая аксиома высшего порядка утверждает существование функционала, который определяет истинность или ложность формул заданной сложности. В этом контексте сложность формул также измеряется с использованием арифметической иерархии и аналитической иерархии . Аналоги высшего порядка основных подсистем арифметики второго порядка обычно доказывают те же предложения второго порядка (или большое подмножество), что и исходные системы второго порядка. ^[5] Например, базовая теория обратной математики высшего порядка, называемая RCA^ω
₀, доказывает те же предложения, что и RCA ₀ , с точностью до языка.

Как отмечено в предыдущем абзаце, аксиомы понимания второго порядка легко обобщаются на рамки высшего порядка. Однако теоремы, выражающие компактность базовых пространств, ведут себя совершенно по-разному в арифметике второго и высшего порядка: с одной стороны, при ограничении счетными покрытиями/языком арифметики второго порядка компактность единичного интервала доказуема в WKL ₀ из следующего раздела. С другой стороны, при наличии несчетных покрытий/языка арифметики высшего порядка компактность единичного интервала доказуема только из (полной) арифметики второго порядка. ^[6] Другие леммы о покрытии (например, принадлежащие Линделёфу , Витали , Безиковичу и т. д.) демонстрируют такое же поведение, и многие основные свойства калибровочного интеграла эквивалентны компактности базового пространства.

Арифметика второго порядка — формальная теория натуральных чисел и множеств натуральных чисел. Многие математические объекты, такие как счетные кольца , группы и поля , а также точки в эффективных польских пространствах , могут быть представлены в виде множеств натуральных чисел, и по модулю этого представления можно изучать в арифметике второго порядка.

Обратная математика использует несколько подсистем арифметики второго порядка. Типичная теорема обратной математики показывает, что конкретная математическая теорема T эквивалентна конкретной подсистеме S арифметики второго порядка над более слабой подсистемой B. Эта более слабая система B известна как базовая система для результата; для того, чтобы результат обратной математики имел смысл, эта система сама по себе не должна быть способна доказать математическую теорему ^T. [ ^{необходима цитата} ]

Стив Симпсон описывает пять конкретных подсистем арифметики второго порядка, которые он называет Большой пятеркой , и которые часто встречаются в обратной математике. ^{[7] [8]} В порядке возрастания силы эти системы названы аббревиатурами RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ и Π¹
₁-CA ₀ .

В следующей таблице обобщены системы «большой пятерки» ^[9] и перечислены соответствующие системы в арифметике высшего порядка. ^[5] Последние обычно доказывают те же предложения второго порядка (или большое подмножество), что и исходные системы второго порядка. ^[5]

Подсистема	Означает	Порядковый	Примерно соответствует	Комментарии	Аналог более высокого порядка
РКА 0	Аксиома рекурсивного понимания	ω ω	Конструктивная математика ( Бишоп )	Базовая теория	РКАω 0; доказывает те же предложения второго порядка, что и RCA 0
ВКЛ 0	Слабая лемма Кёнига	ω ω	Финитистский редукционизм ( Гильберт )	Консервативный по PRA (соотв. RCA 0 ) для Π0 2(соотв. Π)1 1) предложения	Функционал веера; вычисляет модуль равномерной непрерывности для непрерывных функций${\displaystyle 2^{\mathbb {N} }}$
АКА 0	Аксиома арифметического понимания	ε 0	Предикативизм ( Вейль , Феферман )	Консервативная арифметика по Пеано для арифметических предложений	Функционал «скачка Тьюринга» выражает существование разрывной функции на ℝ${\displaystyle \существует ^{2}}$
АТР 0	Арифметическая трансфинитная рекурсия	Г 0	Предикативный редукционизм (Фридман, Симпсон)	Консервативный по системе Фефермана IR для Π1 1предложения	Функционал «трансфинитной рекурсии» выводит множество, существование которого утверждает ATR 0 .
П1 1-CA 0	П1 1аксиома понимания	Ψ 0 (Ω ω )	Импредикативизм		Функционал Суслина решает Π${\displaystyle S^{2}}$1 1-формулы (ограничены параметрами второго порядка).

Нижний индекс ₀ в этих названиях означает, что схема индукции была ограничена полной схемой индукции второго порядка. ^[10] Например, ACA ₀ включает аксиому индукции (0 ∈ X ∀ n ( n ∈ X → n + 1 ∈ X )) → ∀ n n ∈ X${\displaystyle \клин}$ . Это вместе с аксиомой полного понимания арифметики второго порядка подразумевает полную схему индукции второго порядка, заданную универсальным замыканием ( φ (0) ∀ n ( φ ( n ) → φ ( n +1))) → ∀ n φ ( n )${\displaystyle \клин}$ для любой формулы второго порядка φ . Однако ACA ₀ не имеет полной аксиомы полного понимания, и нижний индекс ₀ является напоминанием о том, что она также не имеет полной схемы индукции второго порядка. Это ограничение важно: системы с ограниченной индукцией имеют значительно более низкие теоретические порядковые числа доказательств , чем системы с полной схемой индукции второго порядка.

RCA ₀ — фрагмент арифметики второго порядка, аксиомы которого являются аксиомами арифметики Робинсона , индукция для Σ⁰
₁формулы и понимание для Δ⁰
₁формулы.

Подсистема RCA ₀ является наиболее часто используемой в качестве базовой системы для обратной математики. Инициалы «RCA» означают «recursive comprehension axiom», где «recursive» означает «computable», как в recursive function . Это название используется потому, что RCA ₀ неформально соответствует «computable mathematics». В частности, любой набор натуральных чисел, существование которого может быть доказано в RCA _{0 ,} является вычислимым, и, таким образом, любая теорема, подразумевающая существование невычислимых множеств, не доказуема в RCA ₀ . В этом смысле RCA ₀ является конструктивной системой, хотя она и не соответствует требованиям программы конструктивизма , поскольку является теорией в классической логике, включающей закон исключенного третьего .

Несмотря на кажущуюся слабость (не доказано существование невычислимых множеств), RCA ₀ достаточен для доказательства ряда классических теорем, которые, следовательно, требуют лишь минимальной логической силы. Эти теоремы, в некотором смысле, находятся ниже досягаемости предприятия обратной математики, поскольку они уже доказуемы в базовой системе. Классические теоремы, доказуемые в RCA _0, включают:

• Основные свойства натуральных чисел, целых и рациональных чисел (например, то, что последние образуют упорядоченное поле ).
• Основные свойства действительных чисел (действительные числа представляют собой архимедово упорядоченное поле; любая вложенная последовательность замкнутых интервалов , длины которых стремятся к нулю, имеет единственную точку на своем пересечении; действительные числа несчетны). ^{[1] Раздел II.4}
• Теорема Бэра о категории для полного отделимого метрического пространства (условие отделимости необходимо даже для формулировки теоремы на языке арифметики второго порядка). ^{[1] Теорема II.5.8}
• Теорема о промежуточном значении для непрерывных действительных функций. ^{[1] Теорема II.6.6}
• Теорема Банаха –Штейнгауза для последовательности непрерывных линейных операторов на сепарабельных банаховых пространствах. ^{[1] Теорема II.10.8}
• Слабая версия теоремы Гёделя о полноте (для множества предложений в счетном языке, которое уже замкнуто относительно следствия).
• Существование алгебраического замыкания для счетного поля (но не его единственность). ^{[1] II.9.4--II.9.8}
• Существование и единственность действительного замыкания счетного упорядоченного поля. ^{[1] II.9.5, II.9.7}

Часть первого порядка RCA ₀ (теоремы системы, не включающие никаких заданных переменных) представляет собой набор теорем арифметики Пеано первого порядка с индукцией, ограниченной Σ⁰
₁формулы. Он доказуемо непротиворечив, как и RCA ₀ , в полной арифметике Пеано первого порядка.

Подсистема WKL ₀ состоит из RCA ₀ плюс слабая форма леммы Кёнига , а именно утверждение, что каждое бесконечное поддерево полного бинарного дерева (дерево всех конечных последовательностей нулей и единиц) имеет бесконечный путь. Это утверждение, известное как слабая лемма Кёнига , легко сформулировать на языке арифметики второго порядка. WKL ₀ также можно определить как принцип Σ⁰
₁разделение (при двух Σ⁰
₁формулы свободной переменной n, которые являются исключающими, существует множество, содержащее все n, удовлетворяющие одной, и ни одного n , удовлетворяющего другой). Когда эта аксиома добавляется к RCA ₀ , результирующая подсистема называется WKL ₀ . Аналогичное различие между отдельными аксиомами, с одной стороны, и подсистемами, включающими основные аксиомы и индукцию, с другой стороны, проводится для более сильных подсистем, описанных ниже.

В некотором смысле слабая лемма Кёнига является формой аксиомы выбора (хотя, как было сказано, она может быть доказана в классической теории множеств Цермело–Френкеля без аксиомы выбора). Она не является конструктивно валидной в некоторых смыслах слова «конструктивный».

Чтобы показать, что WKL ₀ на самом деле сильнее (не доказуемо в) RCA ₀ , достаточно предъявить теорему WKL _0, которая подразумевает существование невычислимых множеств. Это несложно; WKL ₀ подразумевает существование разделяющих множеств для эффективно неразделимых рекурсивно перечислимых множеств.

Оказывается, что RCA ₀ и WKL ₀ имеют одну и ту же часть первого порядка, что означает, что они доказывают одни и те же предложения первого порядка. Однако WKL ₀ может доказать большое количество классических математических результатов, которые не следуют из RCA ₀ . Эти результаты не могут быть выражены как утверждения первого порядка, но могут быть выражены как утверждения второго порядка.

Следующие результаты эквивалентны слабой лемме Кёнига и, следовательно, WKL ₀ над RCA ₀ :

• Теорема Гейне –Бореля для замкнутого единичного действительного интервала в следующем смысле: каждое покрытие последовательностью открытых интервалов имеет конечное подпокрытие.
• Теорема Гейне–Бореля для полных вполне ограниченных сепарабельных метрических пространств (где покрытие осуществляется последовательностью открытых шаров).
• Непрерывная действительная функция на замкнутом единичном интервале (или на любом компактном сепарабельном метрическом пространстве, как указано выше) ограничена (или: ограничена и достигает своих границ).
• Непрерывную действительную функцию на замкнутом единичном интервале можно равномерно аппроксимировать полиномами (с рациональными коэффициентами).
• Непрерывная действительная функция на замкнутом единичном интервале равномерно непрерывна.
• Непрерывная действительная функция на замкнутом единичном интервале интегрируема по Риману .
• Теорема Брауэра о неподвижной точке (для непрерывных функций на -симплексе). ^{[1] Теорема IV.7.7}${\displaystyle n}$
• Сепарабельная теорема Хана–Банаха в форме: ограниченная линейная форма на подпространстве сепарабельного банахова пространства продолжается до ограниченной линейной формы на всем пространстве.
• Теорема о кривой Жордана
• Теорема Гёделя о полноте (для счётного языка).
• Определенность для открытых (или даже открыто-закрытых) игр на {0,1} длины ω.
• Каждое счетное коммутативное кольцо имеет простой идеал .
• Каждое счетное формально действительное поле упорядочиваемо.
• Единственность алгебраического замыкания (для счетного поля).

ACA ₀ — это RCA ₀ плюс схема понимания для арифметических формул (иногда называемая «аксиомой арифметического понимания»). То есть, ACA ₀ позволяет нам сформировать множество натуральных чисел, удовлетворяющих произвольной арифметической формуле (без связанных переменных множества, хотя, возможно, содержащей параметры множества). ^{[1] стр. 6--7} На самом деле, достаточно добавить к RCA ₀ схему понимания для формул Σ ₁ (включая также свободные переменные второго порядка), чтобы получить полное арифметическое понимание. ^{[1] Лемма III.1.3}

Часть первого порядка ACA ₀ — это в точности арифметика Пеано первого порядка; ACA ₀ — это консервативное расширение арифметики Пеано первого порядка. ^{[1] Следствие IX.1.6} Две системы доказуемо (в слабой системе) равносогласованы. ACA ₀ можно рассматривать как структуру предикативной математики, хотя существуют предикативно доказуемые теоремы, которые не доказуемы в ACA _0. Большинство фундаментальных результатов о натуральных числах и многие другие математические теоремы могут быть доказаны в этой системе.

Один из способов увидеть, что ACA ₀ сильнее, чем WKL _0, — это продемонстрировать модель WKL _0, которая не содержит все арифметические множества. Фактически, можно построить модель WKL _0, состоящую полностью из низких множеств , используя теорему о низком базисе , поскольку низкие множества относительно низких множеств являются низкими.

Следующие утверждения эквивалентны ACA ₀ над RCA ₀ :

• Последовательная полнота действительных чисел (всякая ограниченная возрастающая последовательность действительных чисел имеет предел). ^{[1] Теорема III.2.2}
• Теорема Больцано –Вейерштрасса . ^{[1] Теорема III.2.2}
• Теорема Асколи : каждая ограниченная равностепенно непрерывная последовательность действительных функций на единичном интервале имеет равномерно сходящуюся подпоследовательность.
• Каждое счетное поле изоморфно вкладывается в свое алгебраическое замыкание. ^{[1] Теорема III.3.2}
• Каждое счетное коммутативное кольцо имеет максимальный идеал . ^{[1] Теорема III.5.5}
• Каждое счетное векторное пространство над рациональными числами (или над любым счетным полем) имеет базис. ^{[1] Теорема III.4.3}
• Для любых счетных полей существует базис трансцендентности для более . ^{[1] Теорема III.4.6}${\displaystyle K\subseteq L}$${\displaystyle L}$${\displaystyle К}$
• Лемма Кёнига (для произвольных конечно ветвящихся деревьев, в отличие от слабой версии, описанной выше). ^{[1] Теорема III.7.2}
• Для любой счетной группы и любых подгрупп из существует подгруппа, порожденная . ^{[11] с.40}${\displaystyle G}$${\displaystyle H,I}$${\displaystyle G}$${\displaystyle H\чашка I}$
• Любую частичную функцию можно расширить до полной функции. ^[12]
• Различные теоремы комбинаторики, такие как некоторые формы теоремы Рамсея . ^{[13] [1] Теорема III.7.2}

Система ATR ₀ добавляет к ACA ₀ аксиому, которая неформально утверждает, что любой арифметический функционал (имеется в виду любая арифметическая формула со свободной числовой переменной n и свободной переменной множества X , рассматриваемая как оператор, переносящий X в множество n, удовлетворяющее формуле) может быть итерирован трансфинитно вдоль любого счетного полного порядка, начиная с любого множества. ATR ₀ эквивалентен над ACA ₀ принципу Σ¹
₁разделение. ATR ₀ является непредикативным и имеет доказательно-теоретический ординал , супремум предикативных систем.${\displaystyle \Гамма _{0}}$

ATR ₀ доказывает непротиворечивость ACA ₀ , и, таким образом, по теореме Гёделя он является строго сильнее.

Следующие утверждения эквивалентны ATR ₀ над RCA ₀ :

• Любые два счетных полных порядка сравнимы. То есть они изоморфны или один изоморфен собственному начальному сегменту другого. ^{[1] Теорема V.6.8}
• Теорема Ульма для счетных приведенных абелевых групп.
• Теорема о совершенном множестве , которая утверждает, что каждое несчетное замкнутое подмножество полного сепарабельного метрического пространства содержит совершенное замкнутое множество.
• Теорема Лузина о разделении (по сути Σ¹
  ₁^[1] Теорема ^V.5.1
• Определенность для открытых множеств в пространстве Бэра .

П¹
₁-CA ₀ сильнее арифметической трансфинитной рекурсии и полностью непредикативен. Он состоит из RCA ₀ плюс схема понимания для Π¹
₁формулы.

В каком-то смысле, П¹
₁-CA ₀ понимание относится к арифметической трансфинитной рекурсии (Σ¹
₁разделение), поскольку ACA ₀ является слабой леммой Кёнига (Σ⁰
₁(разделение). Это эквивалентно нескольким утверждениям описательной теории множеств, доказательства которых используют строго непредикативные аргументы; эта эквивалентность показывает, что эти непредикативные аргументы не могут быть удалены.

Следующие теоремы эквивалентны Π¹
₁-CA ₀ по RCA ₀ :

• Теорема Кантора –Бендиксона (каждое замкнутое множество действительных чисел является объединением совершенного множества и счетного множества). ^{[1] Упражнение VI.1.7}
• Дихотомия Сильвера (каждое коаналитическое отношение эквивалентности имеет либо счетное число классов эквивалентности, либо совершенное множество несравнимых) ^{[1] Теорема VI.3.6}
• Каждая счетная абелева группа является прямой суммой делимой группы и редуцированной группы. ^{[1] Теорема VI.4.1}
• Определенность для игр. ^{[1] Теорема VI.5.4}${\displaystyle \Сигма _{1}^{0}\land \Пи _{1}^{0}}$

• Можно определить более слабые системы, чем рекурсивное понимание. Слабая система RCA^*
  ₀состоит из элементарной арифметики функций EFA (основные аксиомы плюс Δ⁰
  ₀индукция в обогащенном языке с экспоненциальной операцией) плюс Δ⁰
  ₁понимание. По RCA^*
  ₀, рекурсивное понимание, как определено ранее (то есть с Σ⁰
  ₁индукция) эквивалентна утверждению, что многочлен (над счетным полем) имеет только конечное число корней, и теореме классификации для конечно порожденных абелевых групп. Система RCA^*
  ₀имеет тот же теоретический ординал доказательства ω ³ , что и EFA, и является консервативным по сравнению с EFA для Π⁰
  ₂предложения.
• Слабая слабая лемма Кёнига — это утверждение, что поддерево бесконечного бинарного дерева, не имеющее бесконечных путей, имеет асимптотически исчезающую долю листьев длины n (с равномерной оценкой того, сколько листьев длины n существует). Эквивалентная формулировка состоит в том, что любое подмножество пространства Кантора, имеющее положительную меру, непусто (это не доказуемо в RCA ₀ ). WWKL ₀ получается присоединением этой аксиомы к RCA ₀ . Это эквивалентно утверждению, что если единичный действительный интервал покрыт последовательностью интервалов, то сумма их длин равна по крайней мере единице. Теория моделей WWKL ₀ тесно связана с теорией алгоритмически случайных последовательностей . В частности, ω-модель RCA ₀ удовлетворяет слабой слабой лемме Кёнига тогда и только тогда, когда для каждого множества X существует множество Y , которое является 1-случайным относительно X .
• DNR (сокращение от "diagonally non-recursive") добавляет к RCA ₀ аксиому, утверждающую существование диагонально нерекурсивной функции относительно каждого множества. То есть, DNR утверждает, что для любого множества A существует полная функция f такая, что для всех e e- я частично рекурсивная функция с оракулом A не равна f . DNR строго слабее, чем WWKL (Lempp et al. , 2004).
• Δ¹
  ₁-понимание в некотором смысле аналогично арифметической трансфинитной рекурсии, как рекурсивное понимание аналогично слабой лемме Кёнига. Оно имеет гиперарифметические множества в качестве минимальной ω-модели. Арифметическая трансфинитная рекурсия доказывает Δ¹
  ₁-понимание, но не наоборот.
• Σ¹
  ₁-выбор - это утверждение, что если η ( n , X ) является Σ¹
  ₁формула такая, что для каждого n существует X, удовлетворяющий η, то существует последовательность множеств X _n такая, что η ( n , X _n ) выполняется для каждого n . Σ¹
  ₁-выбор также имеет гиперарифметические множества как минимальную ω-модель. Арифметическая трансфинитная рекурсия доказывает Σ¹
  ₁-выбор, но не наоборот.
• HBU (сокращение от «несчетный Гейне-Борель») выражает (открытую) компактность единичного интервала, включая несчетные покрытия . Последний аспект HBU делает его выразимым только на языке арифметики третьего порядка . Теорема Кузена (1895) подразумевает HBU, и эти теоремы используют то же понятие покрытия, что и Кузен и Линделёф . HBU трудно доказать: в терминах обычной иерархии аксиом понимания доказательство HBU требует полной арифметики второго порядка. ^[6]
• Теорема Рамсея для бесконечных графов не попадает ни в одну из пяти больших подсистем, и существует множество других более слабых вариантов с различной силой доказательства. ^[13]

По RCA ₀ , Π¹
₁трансфинитная рекурсия, ∆⁰
₂определенность и ∆¹
₁Все теоремы Рамсея эквивалентны друг другу.

По RCA ₀ , Σ¹
₁монотонная индукция, Σ⁰
₂определенность и Σ¹
₁Все теоремы Рамсея эквивалентны друг другу.

Следующие значения эквивалентны: ^{[14] [15]}

• (схема) Π¹
  ₃последствия Π¹
  ₂-CA ₀
• RCA ₀ + (схема над конечным n ) определенность на n -м уровне иерархии разностей Σ⁰
  ₂наборы
• RCA ₀ + {τ: τ — истинное предложение S2S }

Множество Π¹
₃следствия арифметики второго порядка Z ₂ имеют ту же теорию, что и RCA ₀ + (схема над конечным n ) определенность на n- м уровне иерархии разностей Σ⁰
₃наборы. ^[16]

Для частично упорядоченного множества пусть обозначает топологическое пространство, состоящее из фильтров, на которых открытые множества являются множествами вида для некоторого . Следующее утверждение эквивалентно над : для любого счетного частично упорядоченного множества топологическое пространство полностью метризуемо тогда и только тогда, когда оно регулярно . ^[17]${\displaystyle P}$${\displaystyle {\textrm {MF}}(P)}$${\displaystyle P}$${\displaystyle \{F\in {\textrm {MF}}(P)\mid p\in F\}}$${\displaystyle p\in P}$${\displaystyle \Pi _{2}^{1}{\mathsf {-CA}}_{0}}$${\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}}$${\displaystyle P}$${\displaystyle {\textrm {MF}}(P)}$

ω в ω-модели обозначает множество неотрицательных целых чисел (или конечных ординалов). ω-модель — это модель для фрагмента арифметики второго порядка, чья часть первого порядка является стандартной моделью арифметики Пеано ^[1] , но чья часть второго порядка может быть нестандартной. Точнее, ω-модель задается выбором подмножеств . Переменные первого порядка интерпретируются обычным образом как элементы , и , имеют свои обычные значения, в то время как переменные второго порядка интерпретируются как элементы . Существует стандартная ω-модель, в которой просто принимается , что состоит из всех подмножеств целых чисел. Однако существуют и другие ω-модели; например, RCA ₀ имеет минимальную ω-модель, в которой состоит из рекурсивных подмножеств .${\displaystyle S\subseteq {\mathcal {P}}(\omega)}$${\displaystyle \омега}$${\displaystyle \омега}$${\displaystyle +}$${\displaystyle \times}$${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$${\displaystyle \омега}$

β-модель — это ω-модель, которая согласуется со стандартной ω-моделью по истинности предложений (с параметрами).${\displaystyle \Пи _{1}^{1}}$${\displaystyle \Sigma _{1}^{1}}$

Не-ω-модели также полезны, особенно при доказательстве теорем сохранения.

• Выражение в замкнутой форме § Преобразование из числовых форм
• Принципы индукции, ограничения и наименьшего числа
• Порядковый анализ

• Амбос-Спис, К.; Кьос-Ханссен, Б.; Лемпп, С.; Сламан, Т.А. (2004), «Сравнение DNR и WWKL», Журнал символической логики , 69 (4): 1089, arXiv : 1408.2281 , doi : 10.2178/jsl/1102022212, S2CID  17582399.
• Фридман, Харви (1975), «Некоторые системы арифметики второго порядка и их использование», Труды Международного конгресса математиков (Ванкувер, Британская Колумбия, 1974), т. 1 , Канадский математический конгресс, Монреаль, Квебек, стр.  235–242 , MR  0429508
• Фридман, Харви (1976), Болдуин, Джон; Мартин, ДА ; Соаре, РИ ; Тейт, WW (ред.), «Системы арифметики второго порядка с ограниченной индукцией, I, II», Собрание Ассоциации символической логики, Журнал символической логики , 41 (2): 557– 559, doi :10.2307/2272259, JSTOR  2272259
• Хиршфельдт, Денис Р. (2014), Slicing the Truth , Серия лекционных заметок Института математических наук Национального университета Сингапура, т. 28, World Scientific
• Хантер, Джеймс (2008), Обратная топология (PDF) (диссертация), Университет Висконсин-Мэдисон
• Kohlenbach, Ulrich (2005), «Обратная математика высшего порядка», в Simpson, Stephen G (ред.), Обратная математика высшего порядка, Обратная математика 2001 (PDF) , Lecture Notes in Logic, Cambridge University Press , стр.  281–295 , CiteSeerX  10.1.1.643.551 , doi :10.1017/9781316755846.018, ISBN 9781316755846
• Норманн, Даг; Сандерс, Сэм (2018), «О математическом и основополагающем значении несчетного», Журнал математической логики , 19 : 1950001, arXiv : 1711.08939 , doi : 10.1142/S0219061319500016, S2CID  119120366
• Симпсон, Стивен Г. (2009), Подсистемы арифметики второго порядка, Perspectives in Logic (2-е изд.), Cambridge University Press , doi : 10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, г-н  2517689
• Стиллвелл, Джон (2018), Обратная математика, доказательства изнутри наружу , Princeton University Press , ISBN 978-0-691-17717-5

• Соломон, Рид (1999), «Упорядоченные группы: пример из обратной математики», The Bulletin of Symbolic Logic , 5 (1): 45–58 , CiteSeerX  10.1.1.364.9553 , doi :10.2307/421140, ISSN  1079-8986, JSTOR  421140, MR  1681895, S2CID  508431

• Домашняя страница Стивена Г. Симпсона
• Зоопарк обратной математики