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

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

• 1 История
• 2 Определение
• 3 Верхняя граница
• 4 Примеры
  • 4.1 Теории с порядковым номером теории доказательства ω
  • 4.2 Теории с порядковым номером теории доказательства ω
  • 4.3 Теории с ординалом теории доказательства ω
  • 4.4 Теории с ординалом теории доказательства ω (для n = 2, 3,... ω)
  • 4.5 Теории с ординалом теории доказательства ω
  • 4.6 Теории с ординалом доказательства -теоретический ординал ε 0
  • 4.7 Теории с теоретико-доказательственным ординалом ординал Фефермана – Шютте Γ 0
  • 4.8 Теории с теоретико-доказательским ординалом ординал Бахмана – Ховарда
  • 4.9 Теории с более крупными теоретико-доказательными ординалами
• 5 См. Также
• 6 Ссылки

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

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

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

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

Теории с порядковым номером ω

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

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

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

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

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

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

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

• IΔ0или EFA, дополненным аксиомой, гарантирующей, что каждый элемент n-го уровня $E\; n\; \{\backslash \; displaystyle\; \{\backslash \; mathcal\; \{E\}\}\; ^\; \{n\}\}$из иерархии Гжегорчика всего.

Теории с порядковым номером ω

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

Теории с доказательством- теоретический порядковый ε 0

• PA, арифметика Пеано (показан Gentzen с использованием исключения вырезания ).
• ACA 0, арифметическое понимание.

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

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

Иногда этот ординал считается верхний предел для "предикативных" теорий.

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

• ID1, теория индуктивных определений.
• КП, теория множеств Крипке – Платека с аксиомой бесконечности.
• CZF, конструктив Цермело Акзеля - Теория множеств Френкеля.
• EON, слабый вариант явной математической системы Фефермана T 0.

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

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

• $\Pi \; 1\; 1\; -\; CA\; 0\; \{\backslash \; displaystyle\; \backslash \; Pi\; \_\; \{1\}\; ^\; \{1\}\; \{\backslash \; t\_dv\; \{-\}\}\; \{\backslash \; mathsf\; \{CA\}\}\; \_\; \{0\}\}$, Π1понимание имеет довольно большой теоретико-доказательный порядковый номер, который был описан Такеути в терминах «порядковых диаграмм» и который ограничен ψ0(Ωω) в нотации Бухгольца. Это также ординал , теории конечно-итерационных индуктивных определений. А также ординал MLW, теории типов Мартина-Лёфа с индексированными W-типами Setzer (2004).
• T0, конструктивная система явной математики Фефермана имеет более крупный теоретико-доказательный ординал, который также является теоретико-доказательным ординалом. теории множеств КПи, теории множеств Крипке – Платека с повторными допустимыми и $\Sigma \; 2\; 1\; -\; AC\; +\; BI\; \{\backslash \; displaystyle\; \backslash \; Sigma\; \_\; \{2\}\; ^\; \{1\}\; \{\backslash \; t\_dv\; \{-\}\}\; \{\backslash \; mathsf\; \{AC\}\}\; +\; \{\backslash \; mathsf\; \{BI\}\}\}$.
• KPM, расширение теории множеств Крипке – Платека, основанное на кардинале Мало, имеет очень большой теоретико-доказательный ординал ϑ, который был описан Ратьеном (1990).
• MLM, расширение теории типа Мартина-Лёфа одной Мало-вселенной, имеет еще больший теоретико-доказательный ординал ψ Ω1(ΩM + ω).

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

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

• Buchholz, W.; Феферман, С.; Pohlers, W.; Зиг, W. (1981), Итерированные индуктивные определения и подсистемы анализа, Lecture Notes in Math., 897, Berlin: Springer-Verlag, doi : 10.1007 / BFb0091894, ISBN 978-3-540-11170-2
• Pohlers, Wolfram (1989), Теория доказательств, Конспект лекций по математике, 1407, Берлин: Springer-Verlag, doi : 10.1007 / 978-3-540-46825-7, ISBN 3-540-51842-8, MR 1026933
• Полерс, Вольфрам (1998), «Теория множеств и теория чисел второго порядка», Справочник по теории доказательства, исследования по логике и основам математики, 137, Амстердам: Elsevier Science BV, стр. 210–335, doi : 10.1016 / S0049-237X (98) 80019-0, ISBN 0-444-89840-9, MR 1640328
• Rathjen, Michael (1990), «Порядковые обозначения, основанные на слабом кардинале Mahlo.», Arch. Математика. Логика, 29 (4): 249–263, doi : 10.1007 / BF01651328, MR 1062729
• Рэтджен, Майкл (2006), " искусство порядкового анализа » (PDF), Международный конгресс математиков, II, Цюрих: Eur. Математика. Soc., Pp. 45–69, MR 2275588, заархивировано из оригинала 22 декабря 2009 г. CS1 maint: BOT: статус исходного URL-адреса неизвестен (ссылка )
• Rose, HE (1984), Subrecursion. Functions and Hierarchies, Oxford logic guides, 9, Oxford, New York: Clarendon Press, Oxford University Press
• Schütte, Kurt (1977), Proof theory, Grundlehren der Mathematischen Wissenschaften, 225, Берлин-Нью-Йорк: Springer-Verlag, pp. Xii + 299, ISBN 3-540-07911-4, MR 0505313
• Setzer, Антон (2004), «Теория доказательств теории типа Мартина-Лёфа. Обзор», Mathématiques et Sciences Humaines. Математика и социальные науки (165): 59–99
• Такеути, Гайси (1987)), Теория доказательства, Исследования по логике и основам математики, 81 (второе изд.), Амстердам: North-Holland Publishing Co., ISBN 0-444- 87943-9, MR 0882549

1. ^Крайчек, Ян (1995). Ограниченная арифметика, пропозициональная логика и теория сложности. Cambridge University Press. Стр. 18–20. ISBN 9780521452052.определяет рудиментарные множества и рудиментарные функции и доказывает их эквивалентность Δ 0 -предикатам на натуральных числах. Порядковый анализ системы можно найти в Rose, H.E. (1984). Субрекурсия: функции и иерархии. Мичиганский университет: Clarendon Press. ISBN 9780198531890.