В теории доказательств , порядковое анализ присваивает порядковые (часто большие счетными порядковыми ) математических теорий , как меру своих сил. Если теории имеют один и тот же теоретико-доказательный ординал, они часто равносогласованы , а если одна теория имеет более крупный теоретико-доказательный ординал, чем другая, это часто может доказать непротиворечивость второй теории.
История
Поле порядкового анализа было сформировано , когда Генцен в 1934 году б ликвидации разреза , чтобы доказать, в современных терминах, что доказательство теоретико-порядковое из арифметики Пеано является ε 0 . См . Доказательство непротиворечивости Гентцена .
Определение
Порядковый анализ касается истинных, эффективных (рекурсивных) теорий, которые могут интерпретировать достаточную часть арифметики, чтобы делать утверждения о порядковых обозначениях.
Доказательства теоретико-порядковые такой теории внаименьший ординал (обязательно рекурсивный , см. следующий раздел), который теория не может доказать, является хорошо обоснованным - верхняя грань всех ординаловдля которого существует обозначениев смысле Клини такой, что доказывает, что - порядковое обозначение . Эквивалентно, это верхняя грань всех ординалов.такое, что существует рекурсивное отношение на (набор натуральных чисел), который хорошо упорядочивает его с порядковым номером и такой, что доказывает трансфинитную индукцию арифметических утверждений для.
Верхняя граница
Существование рекурсивного ординала, который теория не может доказать, является хорошо упорядоченным, следует из ограничивающая теорема, поскольку набор натуральных чисел, которые эффективная теория доказывает, являются порядковыми обозначениями, является множество (см. Гиперарифметическая теория ). Таким образом, теоретико-доказательный ординал теории всегда будет (счетным) рекурсивным ординалом , то есть меньшим, чем ординал Черча – Клини. .
Примеры
Теории с ординалом теории доказательств ω
- Q, арифметика Робинсона (хотя определение теоретико-доказательственного ординала для таких слабых теорий должно быть изменено).
- PA - теория первого порядка неотрицательной части дискретно упорядоченного кольца.
Теории с ординалом теории доказательств ω 2
- RFA, элементарная арифметика функций . [1]
- IΔ 0 , арифметика с индукцией по Δ 0 -предикатам без какой-либо аксиомы, утверждающей, что возведение в степень является полным.
Теории с ординалом теории доказательств ω 3
- EFA, арифметика элементарных функций .
- IΔ 0 + exp, арифметика с индукцией по Δ 0 -предикатам, дополненная аксиомой, утверждающей, что возведение в степень является полным.
- RCA*
0, форма второго порядка EFA, иногда используемая в обратной математике . - WKL*
0, форма второго порядка EFA, иногда используемая в обратной математике .
Грандиозная гипотеза Фридмана предполагает, что большая часть «обычной» математики может быть доказана в слабых системах, имеющих это в качестве своего теоретического порядкового номера.
Теории с теоретико-доказательственным ординалом ω n (для n = 2, 3, ... ω)
- IΔ 0 или EFA, дополненная аксиомой, гарантирующей, что каждый элемент n -го уровняв иерархии Гжегорчика является полным.
Теории с ординалом теории доказательств ω ω
- RCA 0 , рекурсивное понимание .
- WKL 0 , слабая лемма Кенига .
- PRA, примитивно-рекурсивная арифметика .
- IΣ 1 , арифметика с индукцией по Σ 1 -предикатам.
Теории с ординалом теории доказательств ε 0
- ПА, арифметика Пеано ( показано на Генцене , используя устранение разреза ).
- ACA 0 , понимание арифметики .
Теории с теоретико-доказательственным ординалом ординалом Фефермана – Шютте Γ 0
- ATR 0 , арифметическая трансфинитная рекурсия .
- Теория типа Мартина-Лёфа с произвольным числом вселенных конечного уровня.
Этот порядковый номер иногда считается верхним пределом для «предикативных» теорий.
Теории с ординалом теории доказательств ординалом Бахмана – Ховарда
- ИД 1 , теория индуктивных определений.
- К.П. Теория множеств Крипке – Платека с аксиомой бесконечности .
- CZF, конструктивная теория множеств Цермело – Френкеля Акцеля .
- EON, слабый вариант явной математической системы Фефермана T 0 .
Теории множеств Крипке-Платека или CZF представляют собой теории слабых множеств без аксиом для полного набора степеней, заданного как набор всех подмножеств. Вместо этого они, как правило, либо имеют аксиомы ограниченного разделения и формирования новых множеств, либо допускают существование определенных функциональных пространств (возведение в степень) вместо того, чтобы вырезать их из более крупных отношений.
Теории с большими порядковыми номерами теории доказательств
- , Π 1 1 понимание имеет довольно большой теоретико-доказательный ординал, который был описан Такеути в терминах «порядковых диаграмм» и который ограничен ψ 0 (Ω ω ) в обозначениях Бухгольца . Это также порядковый номер, теория конечно итерационных индуктивных определений. А также порядковый номер MLW, теории типов Мартина-Лёфа с индексированным W-типом Setzer (2004) .
- T 0 конструктивная система явной математики Фефермана имеет более крупный теоретико-доказательный ординал, который также является теоретико-доказательственным ординалом теории множеств КПи, теории множеств Крипке – Платека с повторяющимися допустимыми и.
- КПМ, расширение теории множеств Крипке – Платека, основанное на кардинале Мало , имеет очень большой теоретико-доказательный ординал, который был описан Ратьеном (1990) .
- MLM, расширение теории типа Мартина-Лёфа с помощью одной мало-вселенной, имеет еще больший теоретико-доказательный ординал ψ Ω 1 (Ω M + ω ).
Большинство теорий, способных описывать набор степеней натуральных чисел, имеют теоретические порядковые порядковые номера, которые настолько велики, что явного комбинаторного описания еще не дано. Это включает арифметику второго порядка и теории множеств с наборами мощности, включая ZF и ZFC (по состоянию на 2019 г.[Обновить]). Сила интуиционистского ZF (IZF) равна силе ZF.
Смотрите также
- Равносогласованность
- Большое кардинальное свойство
- Порядковый номер Фефермана – Шютте
- Порядковый номер Бахмана – Ховарда
- Класс сложности
Рекомендации
- Buchholz, W .; Феферман, С .; Pohlers, W .; Зиг, В. (1981), Итерированные индуктивные определения и подсистемы анализа ., Lecture Notes в математике, 897 , Берлин: Springer-Verlag, DOI : 10.1007 / BFb0091894 , ISBN 978-3-540-11170-2
- Pohlers, Вольфрам (1989), теория доказательств , конспект лекций по математике, 1407 , Берлин: Springer-Verlag, doi : 10.1007 / 978-3-540-46825-7 , ISBN 3-540-51842-8, MR 1026933
- Pohlers, Вольфрам (1998), "Теория множеств и второй порядок теория чисел", Справочник по теории доказательств , Исследование в области логики и основа математики, 137 , Амстердам:. Elsevier Science BV, С. 210-335, DOI : 10.1016 / S0049 -237X (98) 80019-0 , ISBN 0-444-89840-9, Руководство по ремонту 1640328
- Ратьен, Майкл (1990), «Порядковые обозначения, основанные на слабом кардинале Mahlo». , Arch. Математика. Логика , 29 (4): 249-263, DOI : 10.1007 / BF01651328 , МР 1062729
- Ратиен, Майкл (2006), «Искусство порядкового анализа» (PDF) , Международный конгресс математиков , II , Цюрих: Eur. Математика. Soc., Стр. 45–69, MR 2275588 , архивировано 22 декабря 2009 г.CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
- Роуз, HE (1984), Subrecursion. Функции и иерархии , Oxford logic guides, 9 , Oxford, New York: Clarendon Press, Oxford University Press
- Шютте, Курт (1977), Теория доказательств , Grundlehren der Mathematischen Wissenschaften, 225 , Берлин-Нью-Йорк: Springer-Verlag, стр. Xii + 299, ISBN 3-540-07911-4, Руководство по ремонту 0505313
- Сетцер, Антон (2004), "Теория доказательств теории типа Мартина-Лёфа. Обзор" , Mathématiques et Sciences Humaines. Математика и социальные науки (165): 59–99.
- Такеути, Гайси (1987), Теория доказательств , Исследования в области логики и основ математики, 81 (второе издание), Амстердам: North-Holland Publishing Co., ISBN 0-444-87943-9, MR 0882549
- ^ Крайчек, Ян (1995). Ограниченная арифметика, логика высказываний и теория сложности . Издательство Кембриджского университета. С. 18–20 . ISBN 9780521452052.определяет рудиментарные множества и рудиментарные функции и доказывает их эквивалентность Δ 0 -предикатам на натуральных числах. Порядковый анализ системы можно найти в Роза, HE (1984). Субрекурсия: функции и иерархии . Мичиганский университет: Clarendon Press. ISBN 9780198531890.