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

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

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

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

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

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

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

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

Использование арифметики второго порядка

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

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

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

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

Использование арифметики высшего порядка

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

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

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

Большая пятерка подсистем арифметики второго порядка

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

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

Симпсон (2009) описывает пять конкретных подсистем арифметики второго порядка, которые он называет « Большой пятеркой» , которые часто встречаются в обратной математике. В порядке возрастания силы эти системы называются инициализмами RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ и Π. ¹
₁ -СА ₀ .

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

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

Индекс ₀ в этих именах означает, что схема индукции ограничена полной схемой индукции второго порядка. ^[7] Например, ACA ₀ включает в себя аксиому индукции $(0 \in X \land \forall n (n \in X \to n + 1 \in X)) \to \forall n n \in X$ . Вместе с аксиомой полного понимания арифметики второго порядка это подразумевает полную схему индукции второго порядка, заданную универсальным замыканием $(φ (0) \land \forall n (φ (n) \to φ (n +1))) \to \forall n φ (n)$ второго порядка для любой формулы φ . Однако ACA ₀ не имеет полной аксиомы понимания, а индекс ₀ является напоминанием о том, что у него также нет полной схемы индукции второго порядка. Это ограничение важно: системы с ограниченной индукцией имеют существенно меньшие теоретико-доказательные ординалы , чем системы с полной схемой индукции второго порядка.

Базовая система RCA ₀

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

Подсистема RCA ₀ чаще всего используется в качестве базовой системы для обратной математики. Инициалы «RCA» означают «аксиому рекурсивного понимания», где «рекурсивный» означает «вычислимый», как в рекурсивной функции . Это имя используется потому, что RCA ₀ неформально соответствует «вычислимой математике». В частности, любой набор натуральных чисел, существование которого можно доказать в 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 ₀

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

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

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

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

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

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

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

ACA ₀ — это RCA ₀ плюс схема понимания арифметических формул (которую иногда называют «аксиомой арифметического понимания»). То есть ACA ₀ позволяет нам сформировать набор натуральных чисел, удовлетворяющий произвольной арифметической формуле (без связанных наборов переменных, хотя, возможно, содержащий набор параметров). На самом деле, достаточно добавить к RCA ₀ схему понимания для формул Σ ₁ , чтобы получить полное арифметическое понимание.

Часть первого порядка ACA ₀ представляет собой в точности арифметику Пеано первого порядка; ACA ₀ — это консервативное расширение арифметики Пеано первого порядка. Обе системы доказуемо (в слабой системе) эквисовместимы. ACA ₀ можно рассматривать как основу предикативной математики, хотя существуют предикативно доказуемые теоремы, которые недоказуемы в ACA ₀ . Большинство фундаментальных результатов о натуральных числах и многие другие математические теоремы могут быть доказаны в этой системе.

Один из способов убедиться в том, что 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}
Для любых счетных полей $K\subseteq L$ , существует основа трансцендентности для $L$ над $K$ . ^[1]^{Теорема III.4.6}
Лемма Кенига (для произвольных конечно ветвящихся деревьев, в отличие от описанной выше слабой версии). ^[1]^{Теорема III.7.2}
Для любой счетной группы $G$ и любые подгруппы $H,I$ из $G$ , подгруппа, порожденная $H\cup I$ существует. ^[8]^стр.40
Любую частичную функцию можно расширить до полной функции. ^[9]
Различные теоремы комбинаторики, такие как некоторые формы теоремы Рамсея . ^[10]^[1]^{Теорема III.7.2}

Арифметическая трансфинитная рекурсия ATR ₀

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

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

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

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

П ¹
₁ понимание Π ¹
₁ -СА ₀

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

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

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

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

Дополнительные системы

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

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

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

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

Следующие действия эквивалентны: ^[11]^[12]

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

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

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

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

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

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

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

См. также

Примечания

^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^тот ^п ^д ^р ^с ^т ^в ^v ^В Симпсон, Стивен Г. (2009), Подсистемы арифметики второго порядка, Перспективы логики (2-е изд.), Cambridge University Press, doi: 10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, MR 2517689
^ Х. Фридман, Некоторые системы арифметики второго порядка и их использование (1974), Труды Международного конгресса математиков
^ Коленбах (2005) .
^ Jump up to: Перейти обратно: ^а ^б ^с См. Коленбах (2005) и Хантер (2008) .
^ Jump up to: Перейти обратно: ^а ^б Норманн и Сандерс (2018) .
^ Симпсон (2009) , стр.42.
^ Симпсон (2009) , с. 6.
^ С. Такаши, « Обратная математика и счетные алгебраические системы ». доктор философии диссертация, Университет Тохоку, 2016 г.
^ М. Фудзивара, Т. Сато, « Заметки о полных и частичных функциях в арифметике второго порядка ». В 1950 г. Теория доказательств, теория вычислений и смежные темы , июнь 2015 г.
^ Jump up to: Перейти обратно: ^а ^б Хиршфельдт (2014) .
^ Колодзейчик, Лешек; Михалевский, Хенрик (2016). Насколько недоказуема теорема Рабина о разрешимости? . LICS '16: 31-й ежегодный симпозиум ACM/IEEE по логике в информатике. arXiv : 1508.06780 .
^ Колодзейчик, Лешек (19 октября 2015 г.). «Вопрос о разрешимости S2S» . ФОМ.
^ Монтальбан, Антонио; Шор, Ричард (2014). «Пределы определенности в арифметике второго порядка: непротиворечивость и степень сложности». Израильский математический журнал . 204 : 477–508. дои : 10.1007/s11856-014-1117-9 . S2CID 287519 .
^ К. Маммерт, С.Г. Симпсон. «Обратная математика и $\Pi _{2}^{1}$ понимание». В Бюллетене символической логики , том 11 (2005), стр. 526–533.

Ссылки

Амбос-Спис, К.; Кьос-Ханссен, Б.; Лемпп, С.; Сламан, Т.А. (2004), «Сравнение DNR и WWKL», Журнал символической логики , 69 (4): 1089, arXiv : 1408.2281 , doi : 10.2178/jsl/1102022212 , S2CID 17582399 .
Фридман, Харви (1975), «Некоторые системы арифметики второго порядка и их использование», Труды Международного конгресса математиков (Ванкувер, Британская Колумбия, 1974), Vol. 1 , Канада. Математика. Конгресс, Монреаль, Квебек, стр. 235–242, MR 0429508.
Фридман, Харви (1976), Болдуин, Джон; Мартин, Д.А. ; Соаре, Род-Айленд ; Тейт, В.В. (ред.), «Системы арифметики второго порядка с ограниченной индукцией, I, II», Собрание Ассоциации символической логики, Журнал символической логики , 41 (2): 557–559, doi : 10.2307 /2272259 , JSTOR 2272259
Хиршфельдт, Денис Р. (2014), Нарезая правду , Серия конспектов лекций Института математических наук Национального университета Сингапура, том. 28, Всемирный научный
Хантер, Джеймс (2008), Обратная топология (PDF) (докторская диссертация), Университет Висконсина-Мэдисона
Коленбах, Ульрих (2005), «Обратная математика высшего порядка» , Симпсон, Стивен Дж. (редактор), Обратная математика высшего порядка, Обратная математика 2001 (PDF) , Конспекты лекций по логике, Cambridge University Press , стр. 281–295 , CiteSeerX 10.1.1.643.551 , doi : 10.1017/9781316755846.018 , ISBN 9781316755846
Норманн, Даг; Сандерс, Сэм (2018), «О математическом и фундаментальном значении неисчисляемого», Journal of Mathematical Logic , 19 : 1950001, arXiv : 1711.08939 , doi : 10.1142/S0219061319500016 , S2CID 119120366
Симпсон, Стивен Г. (2009), Подсистемы арифметики второго порядка , Перспективы логики (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), «Упорядоченные группы: пример обратной математики», Бюллетень символической логики , 5 (1): 45–58, CiteSeerX 10.1.1.364.9553 , doi : 10.2307/421140 , ISSN 1079- 8986 , ДЖСТОР 421140 , МР 1681895 , С2КИД 508431

Внешние ссылки

[Simpson2009-1] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^тот ^п ^д ^р ^с ^т ^в ^v ^В Симпсон, Стивен Г. (2009), Подсистемы арифметики второго порядка, Перспективы логики (2-е изд.), Cambridge University Press, doi: 10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, MR 2517689

[2] Х. Фридман, Некоторые системы арифметики второго порядка и их использование (1974), Труды Международного конгресса математиков

[FOOTNOTEKohlenbach2005-3] Коленбах (2005) .

[k05h08-4] Jump up to: Перейти обратно: ^а ^б ^с См. Коленбах (2005) и Хантер (2008) .

[FOOTNOTENormannSanders2018-5] Jump up to: Перейти обратно: ^а ^б Норманн и Сандерс (2018) .

[FOOTNOTESimpson2009p.42-6] Симпсон (2009) , стр.42.

[FOOTNOTESimpson20096-7] Симпсон (2009) , с. 6.

[8] С. Такаши, « Обратная математика и счетные алгебраические системы ». доктор философии диссертация, Университет Тохоку, 2016 г.

[9] М. Фудзивара, Т. Сато, « Заметки о полных и частичных функциях в арифметике второго порядка ». В 1950 г. Теория доказательств, теория вычислений и смежные темы , июнь 2015 г.

[FOOTNOTEHirschfeldt2014-10] Jump up to: Перейти обратно: ^а ^б Хиршфельдт (2014) .

[11] Колодзейчик, Лешек; Михалевский, Хенрик (2016). Насколько недоказуема теорема Рабина о разрешимости? . LICS '16: 31-й ежегодный симпозиум ACM/IEEE по логике в информатике. arXiv : 1508.06780 .

[12] Колодзейчик, Лешек (19 октября 2015 г.). «Вопрос о разрешимости S2S» . ФОМ.

[13] Монтальбан, Антонио; Шор, Ричард (2014). «Пределы определенности в арифметике второго порядка: непротиворечивость и степень сложности». Израильский математический журнал . 204 : 477–508. дои : 10.1007/s11856-014-1117-9 . S2CID 287519 .

[14] К. Маммерт, С.Г. Симпсон. «Обратная математика и $\Pi _{2}^{1}$ понимание». В Бюллетене символической логики , том 11 (2005), стр. 526–533.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]