WikiDer > Порядковый анализ

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

История

Область порядкового анализа сформировалась, когда Герхард Гентцен в 1934 г. использовался вырезать устранение доказать, говоря современным языком, что теоретико-доказательный ординал из Арифметика Пеано является ε₀. Видеть Доказательство непротиворечивости Гентцена.

Определение

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

В теоретико-доказательный ординал такой теории ${displaystyle T}$ наименьший порядковый номер (обязательно рекурсивный, см. следующий раздел), что теория не может доказать, хорошо обоснованный- верхняя грань всех ординалов ${displaystyle alpha}$ для которого существует обозначение ${displaystyle o}$ в смысле Клини такой, что ${displaystyle T}$ доказывает, что ${displaystyle o}$ является порядковая запись. Эквивалентно, это верхняя грань всех ординалов ${displaystyle alpha}$ такой, что существует рекурсивное отношение ${displaystyle R}$ на ${displaystyle omega}$ (набор натуральных чисел), что хорошие порядки это с порядковым номером ${displaystyle alpha}$ и такой, что ${displaystyle T}$ доказывает трансфинитная индукция арифметических утверждений для ${displaystyle R}$.

Верхняя граница

Существование рекурсивного ординала, который теория не может доказать, является хорошо упорядоченным, следует из ${displaystyle Sigma _ {1} ^ {1}}$ ограничивающая теорема, поскольку набор натуральных чисел, которые эффективная теория доказывает, являются порядковыми обозначениями, является ${displaystyle Sigma _ {1} ^ {0}}$ установить (см. Гиперарифметическая теория). Таким образом, теоретико-доказательный ординал теории всегда будет (счетным) рекурсивный порядковый, то есть меньше, чем Чёрч – Клини ординал ${displaystyle omega _ {1} ^ {mathrm {CK}}}$.

Примеры

Теории с ординалом теории доказательств ω

• Q, Арифметика Робинсона (хотя определение теоретико-доказательного ординала для таких слабых теорий должно быть изменено).
• PA^–, теория первого порядка неотрицательной части дискретно упорядоченного кольца.

Теории с ординалом теории доказательств ω²

• RFA, рудиментарная функция арифметика.^[1]
• IΔ₀, арифметика с индукцией по Δ₀-предикаты без какой-либо аксиомы, утверждающей, что возведение в степень является полным.

Теории с ординалом теории доказательств ω³

• EFA, арифметика элементарных функций.
• IΔ₀ + exp, арифметика с индукцией по Δ₀-предикаты, дополненные аксиомой, утверждающей, что возведение в степень является полным.
• RCA^*
  ₀, форма второго порядка EFA, иногда используемая в обратная математика.
• WKL^*
  ₀, форма второго порядка EFA, иногда используемая в обратная математика.

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

Теории с ординалом теории доказательств ω^п (за п = 2, 3, ... ω)

• IΔ₀ или ОДВ, дополненное аксиомой, гарантирующей, что каждый элемент п-й уровень ${displaystyle {mathcal {E}} ^ {n}}$ из Иерархия Гжегорчика итого.

Теории с ординалом теории доказательств ω^ω

• RCA₀, рекурсивное понимание.
• WKL₀, слабая лемма Кёнига.
• PRA, примитивная рекурсивная арифметика.
• IΣ₁, арифметика с индукцией по Σ₁-предикаты.

Теории с ординалом теории доказательств ε₀

• PA, Арифметика Пеано (показано к Gentzen с помощью вырезать устранение).
• ACA₀, арифметическое понимание.

Теории с ординалом теории доказательств ординалом Фефермана – Шютте Γ₀

• ATR₀, арифметическая трансфинитная рекурсия.
• Теория типа Мартина-Лёфа со сколь угодно большим числом вселенных конечного уровня.

Этот порядковый номер иногда считается верхним пределом для «предикативных» теорий.

Теории с ординалом теории доказательств ординалом Бахмана – Ховарда

• Я БЫ₁, теория индуктивных определений.
• КП, Теория множеств Крипке – Платека. с аксиома бесконечности.
• CZF, Aczel's конструктивная теория множеств Цермело – Френкеля.
• EON, слабый вариант Феферманявная математическая система T₀.

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

Теории с большими порядковыми числами теории доказательств

• ${displaystyle Pi _ {1} ^ {1} {mbox {-}} {mathsf {CA}} _ {0}}$, Π₁¹ понимание имеет довольно большой теоретико-доказательный ординал, который Такеути описал в терминах "порядковых диаграмм" и который ограничен ψ₀(Ω_ω) в Обозначения Бухгольца. Это также порядковый номер ${displaystyle ID _ {$, теория конечно итерационных индуктивных определений. А также порядковый номер MLW, теории типов Мартина-Лёфа с индексированными W-типами Сетцер (2004).
• Т₀, Конструктивная система явной математики Фефермана имеет более крупный теоретико-доказательный ординал, который также является теоретико-доказательственным ординалом теории множеств КПи, Крипке – Платека с повторяющимися допустимыми и ${displaystyle Sigma _ {2} ^ {1} {mbox {-}} {mathsf {AC}} + {mathsf {BI}}}$.
• КПМ, расширение Теория множеств Крипке – Платека. на основе Мало кардинал, имеет очень большой теоретико-доказательный ординал, который был описан Ратиен (1990).
• MLM, расширение теории типа Мартина-Лёфа с помощью одной мало-вселенной, имеет еще больший теоретико-доказательный ординал ψ_Ω1(Ω_{M + ω}).

Большинство теорий, способных описать набор степеней натуральных чисел, имеют теоретико-доказательные порядковые числа, которые настолько велики, что явного комбинаторного описания еще не дано. Это включает в себя арифметика второго порядка и установить теории с помощью наборов возможностей, включая ZF и ZFC (по состоянию на 2019 г.^{[Обновить]}). Сила интуиционистский ZF (IZF) совпадает с ZF.

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

• Равносогласованность
• Большое кардинальное свойство
• Порядковый номер Фефермана – Шютте
• Порядковый номер Бахмана – Ховарда
• Класс сложности

Рекомендации

• Buchholz, W .; Феферман, С .; Pohlers, W .; Зиг, В. (1981), Повторяющиеся индуктивные определения и подсистемы анализа, Конспект лекций по математике, 897, Берлин: Springer-Verlag, Дои:10.1007 / BFb0091894, ISBN 978-3-540-11170-2
• Pohlers, Вольфрам (1989), Теория доказательств, Конспект лекций по математике, 1407, Берлин: Springer-Verlag, Дои:10.1007/978-3-540-46825-7, ISBN 3-540-51842-8, МИСТЕР 1026933
• Pohlers, Вольфрам (1998), "Теория множеств и теория чисел второго порядка", Справочник по теории доказательств, Исследования по логике и основам математики, 137, Амстердам: Elsevier Science B. V., стр. 210–335, Дои:10.1016 / S0049-237X (98) 80019-0, ISBN 0-444-89840-9, МИСТЕР 1640328
• Ратиен, Майкл (1990), «Порядковые обозначения, основанные на кардинале со слабой степенью Мало»., Arch. Математика. Логика, 29 (4): 249–263, Дои:10.1007 / BF01651328, МИСТЕР 1062729
• Ратиен, Майкл (2006), «Искусство порядкового анализа» (PDF), Международный конгресс математиков, II, Цюрих: Eur. Математика. Soc., Стр. 45–69, МИСТЕР 2275588, архивировано 22 декабря 2009 г.CS1 maint: BOT: статус исходного URL-адреса неизвестен (связь)
• Роуз, Е. (1984), Подрекурсия. Функции и иерархии, Оксфордские логические руководства, 9, Оксфорд, Нью-Йорк: 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 (Второе изд.), Амстердам: Издательство Северной Голландии, ISBN 0-444-87943-9, МИСТЕР 0882549