Обратная математика - Reverse mathematics

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

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

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

Программа была основана Харви Фридманом  ( 1975 , 1976 ) и выдвинута Стивом Симпсоном . Стандартным справочным материалом по этому предмету является Simpson (2009) , а для неспециалистов - Stillwell (2018) . Введение в обратную математику высшего порядка, а также основополагающий документ - это Коленбах (2005) .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Индекс ₀ в этих именах означает, что индукционная схема была ограничена полной индукционной схемой второго порядка. Например, АС ₀ включает в себя индукционную аксиому (0 ∈  X  ∧ ∀ п ( п  ∈  X  →  п  +-∈  X )) → ∀ п  п  ∈ X . Это вместе с аксиомой полного понимания арифметики второго порядка влечет полную схему индукции второго порядка, задаваемую универсальным замыканием ( φ (0) ∧ ∀ n ( φ ( n ) → φ ( n +1))) → ∀ n φ ( n ) для любой формулы второго порядка φ . Однако ACA ₀ не имеет аксиомы полного понимания, а индекс ₀ является напоминанием о том, что он также не имеет полной схемы индукции второго порядка. Это ограничение важно: системы с ограниченной индукцией имеют значительно более низкие порядковые номера теории доказательства, чем системы с полной схемой индукции второго порядка.

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

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

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

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

• Основные свойства натуральных, целых и рациональных чисел (например, что последние образуют упорядоченное поле ).
• Основные свойства действительных чисел (действительные числа представляют собой упорядоченное по Архимеду поле; любая вложенная последовательность отрезков , длина которых стремится к нулю, имеет единственную точку на своем пересечении; действительные числа не подсчитываются).
• Теорема Бэра о категории для полного сепарабельного метрического пространства (условие отделимости необходимо даже для формулировки теоремы на языке арифметики второго порядка).
• Теорема о промежуточном значении о непрерывных действительных функциях.
• Теорема Банаха – Штейнхауза для последовательности непрерывных линейных операторов в сепарабельных банаховых пространствах.
• Слабая версия теоремы Гёделя о полноте (для набора предложений на счетном языке, который уже закрыт по следствию).
• Существование алгебраического замыкания счетного поля (но не его единственность).
• Существование и единственность действительного замыкания счетного упорядоченного поля.

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

Слабая лемма Кёнига WKL ₀

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

Следующее замечание по терминологии уместно. Термин «слабая лемма Кёнига» относится к предложению, в котором говорится, что любое бесконечное поддерево двоичного дерева имеет бесконечный путь. Когда эта аксиома добавляется к RCA ₀ , результирующая подсистема называется WKL ₀ . Аналогичное различие между конкретными аксиомами, с одной стороны, и подсистемами, включая основные аксиомы и индукцию, с другой стороны, проводится для более сильных подсистем, описанных ниже.

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

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

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

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

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

Понимание арифметики ACA ₀

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

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

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

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

• Последовательная полнота действительных чисел (каждая ограниченная возрастающая последовательность действительных чисел имеет предел).
• Теорема Больцано – Вейерштрасса .
• Теорема Асколи : любая ограниченная равностепенно непрерывная последовательность вещественных функций на единичном интервале имеет равномерно сходящуюся подпоследовательность.
• Каждое счетное коммутативное кольцо имеет максимальный идеал .
• Каждое счетное векторное пространство над рациональными числами (или над любым счетным полем) имеет базис.
• Каждое счетное поле имеет основу трансцендентности .
• Лемма Кёнига (для произвольных конечно ветвящихся деревьев, в отличие от слабой версии, описанной выше).
• Различные теоремы комбинаторики, такие как некоторые формы теоремы Рамсея .

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

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

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

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

• Любые два порядка счетных скважин сопоставимы. То есть они изоморфны или один изоморфен собственному начальному отрезку другого.
• Теорема Ульма для счетных редуцированных абелевых групп.
• Теорема о совершенном множестве , которая утверждает, что каждое несчетное замкнутое подмножество полного сепарабельного метрического пространства содержит совершенное замкнутое множество.
• Теорема Лусина об отделимости (по существу Σ¹
  ₁ разделение).
• Решимость для открытых множеств в пространстве Бэра .

Π¹
₁ понимание Π¹
₁-CA ₀

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

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

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

• Теорема Кантора – Бендиксона (каждое замкнутое множество действительных чисел является объединением совершенного множества и счетного множества).
• Каждая счетная абелева группа является прямой суммой делимой группы и редуцированной группы.

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

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

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

Ω в ω-модели обозначает набор неотрицательных целых чисел (или конечных ординалов). Ω-модель - это модель фрагмента арифметики второго порядка, часть первого порядка которой является стандартной моделью арифметики Пеано, но часть второго порядка может быть нестандартной. Точнее, ω-модель задается выбором S ⊆2 ^ω подмножеств ω. Переменные первого порядка интерпретируются обычным образом в качестве элементов со, +, × имеют их обычные значения, а переменные второго порядка интерпретируются как элементы S . Существует стандартная ω-модель, в которой S просто состоит из всех подмножеств целых чисел. Однако есть и другие ω-модели; например, RCA ₀ имеет минимальную ω-модель, где S состоит из рекурсивных подмножеств ω.

Β-модель - это ω-модель, которая эквивалентна стандартной ω-модели для Π¹
₁ и Σ¹
₁ предложения (с параметрами).

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

Смотрите также

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

Примечания

использованная литература

• Ambos-Spies, K .; Kjos-Hanssen, B .; Lempp, S .; Сламан, Т.А. (2004), «Сравнение DNR и WWKL», Журнал символической логики , 69 (4): 1089, arXiv : 1408.2281 , doi : 10.2178 / jsl / 1102022212 .
• Фридман, Харви (1975), "Некоторые системы арифметики второго порядка и их использование", Труды Международного конгресса математиков (Ванкувер, Британская Колумбия, 1974), Vol. 1 , Канад. Математика. Congress, Montreal, Que., Стр. 235–242, MR  0429508
• Фридман, Харви (1976), Болдуин, Джон; Мартин, Д.А .; Соаре, Род-Айленд ; Тайт, WW (ред.), «Системы арифметики второго порядка с ограниченной индукцией, I, II», Встреча Ассоциации символической логики, Журнал символической логики , 41 (2): 557–559, DOI : 10.2307 / 2272259 , JSTOR  2272259
• Хиршфельдт, Денис Р. (2014), Нарезка истины , Серия лекций Института математических наук Национального университета Сингапура, 28 , World Scientific
• Хантер, Джеймс (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
• Симпсон, Стивен Г. (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 , JSTOR  421140 , Руководство по ремонту  1681895

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

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