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

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

История [ править ]

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

Определение [ править ]

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

Доказательства теоретико-порядковое такой теории в наименьшее порядковое (обязательно рекурсивным , смотрите следующий раздел) , что теория не может доказать это вполне обоснованны -The супремуму всех порядковых , для которых существует такая запись в смысле Клини такое , что доказывает , что является порядковое обозначение . Эквивалентно, это верхняя грань всех ординалов, такая, что существует рекурсивное отношение на (наборе натуральных чисел), которое хорошо упорядочивает его с ординалом и такое, что доказывает трансфинитную индукцию ${\ 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Δ ₀ , арифметика с индукцией по Δ ₀ -предикатам без какой-либо аксиомы, утверждающей, что возведение в степень является полным.

Теории с порядковым номером ω ^{3 в} теории доказательств [ править ]

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

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

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

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

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

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

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

ПА, арифметика Пеано ( показано на Генцене , используя устранение разреза ).
ACA ₀ , понимание арифметики .

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

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

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

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

ИД ₁ , теория индуктивных определений.
К.П. Теория множеств Крипке – Платека с аксиомой бесконечности .
CZF, конструктивная теория множеств Цермело – Френкеля Акцеля .
EON, слабый вариант явной математической системы Фефермана T ₀ .

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

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

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

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

См. Также [ править ]

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

Ссылки [ править ]

Buchholz, W .; Feferman, S .; 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: discouraged parameter (link) CS1 maint: bot: original URL status unknown (link)
Роуз, 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.определяет рудиментарные множества и рудиментарные функции и доказывает их эквивалентность Δ ₀ -предикатам на натуральных числах. Порядковый анализ системы можно найти в Rose, HE (1984). Субрекурсия: функции и иерархии . Мичиганский университет: Clarendon Press. ISBN 9780198531890.

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