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

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

Помимо получения теоретико-доказательного ординала теории, на практике порядковый анализ обычно также дает различную другую информацию об анализируемой теории, например, характеристики классов доказуемо рекурсивных, гиперарифметических или $\Delta _{2}^{1}$ функции теории. ^[1]

История

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

Определение

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

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

Порядковые обозначения

Некоторые теории, такие как подсистемы арифметики второго порядка, не имеют концептуализации или способа аргументации трансфинитных ординалов. Например, чтобы формализовать, что это означает для подсистемы Z ₂ $T$ чтобы «доказать $\alpha$ хорошо упорядочены», вместо этого мы строим порядковую запись $(A,{\tilde {<}})$ с типом заказа $\alpha$ . $T$ теперь может работать с различными принципами трансфинитной индукции $(A,{\tilde {<}})$ , которые заменяют рассуждения о теоретико-множественных ординалах.

Однако существуют некоторые патологические системы обозначений, с которыми неожиданно сложно работать. Например, Ратьен предлагает примитивную рекурсивную систему обозначений. $(\mathbb {N} ,<_{T})$ это вполне обосновано тогда и только тогда, когда PA непротиворечив, ^[2]^{п. 3} несмотря на наличие типа заказа $\omega$ - включение такого обозначения в порядковый анализ PA привело бы к ложному равенству ${\mathsf {PTO(PA)}}=\omega$ .

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

Поскольку порядковая запись должна быть рекурсивной, теоретико-доказательный ординал любой теории меньше или равен ординалу Чёрча – Клини. $\omega _{1}^{\mathrm {CK} }$ . В частности, теоретико-доказательный ординал противоречивой теории равен $\omega _{1}^{\mathrm {CK} }$ , потому что противоречивая теория тривиально доказывает, что все порядковые обозначения обоснованы.

Для любой теории это и то, и другое. $\Sigma _{1}^{1}$ -аксиоматизируемый и $\Pi _{1}^{1}$ -разумно, существование рекурсивного порядка, который теория не может доказать, является хорошо упорядоченным, следует из $\Sigma _{1}^{1}$ ограничивающая теорема, и упомянутые доказуемо обоснованные порядковые обозначения на самом деле хорошо обоснованы $\Pi _{1}^{1}$ -здравость. Таким образом, теоретико-доказательный ординал $\Pi _{1}^{1}$ - обоснованная теория, имеющая $\Sigma _{1}^{1}$ аксиоматизация всегда будет (счетным) рекурсивным порядковым номером , то есть строго меньшим, чем $\omega _{1}^{\mathrm {CK} }$ . ^[2]^{Теорема 2.21}

Примеры

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

Вопрос, арифметика Робинсона (хотя определение теоретико-доказательного ординала для таких слабых теорий необходимо изменить) ^{[ нужна ссылка ]}.
Хорошо ^–, теория первого порядка неотрицательной части дискретно упорядоченного кольца.

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

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

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

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

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

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

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

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

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

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

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

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

Нерешенная задача по математике :

Что такое теоретико-доказательный ординал полной арифметики второго порядка? ^[4]

(еще нерешенные задачи по математике)

$\Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}$ , П ₁¹ понимание имеет довольно большой теоретико-доказательный ординал, который Такеути описал в терминах «порядковых диаграмм», ^[5]^{п. 13} которая ограничена ψ0 _Ωω ( _и ) в обозначениях Бухгольца . Это также порядковый номер $ID_{<\omega }$ , теория конечно итерированных индуктивных определений. А также ординал MLW, теории типов Мартина-Лёфа с индексированными W-типами Setzer (2004) .
ID _ω , теория ω-итерированных индуктивных определений . Его теоретико-доказательный ординал равен ординалу Такеути-Фефермана-Бухгольца .
T ₀ конструктивная система явной математики Фефермана имеет больший теоретико-доказательный ординал, который также является теоретико-доказательным ординалом теории множеств KPi, Крипке-Платека с повторяющимися допустимыми и $\Sigma _{2}^{1}{\mbox{-}}{\mathsf {AC}}+{\mathsf {BI}}$ .
KPi, расширение теории множеств Крипке-Платека, основанное на рекурсивно недоступном ординале , имеет очень большой теоретико-доказательный ординал. $\psi (\varepsilon _{I+1})$ описано в статье Ягера и Полерса 1983 года, где I — наименьший из недоступных. ^[6] Этот ординал также является теоретико-доказательным ординалом $\Delta _{2}^{1}{\mbox{-}}{\mathsf {CA}}+{\mathsf {BI}}$ .
КПМ, расширение теории множеств Крипке-Платека , основанное на рекурсивном ординале Мало , имеет очень большой теоретико-доказательный ординал θ, который был описан Ратьеном (1990) .
TTM, расширение теории типов Мартина-Лёфа с помощью одной Мало-вселенной, имеет еще больший теоретико-доказательный ординал ψ _{Ω ₁} (Ω _{M + ω} ).
${\mathsf {KP}}+\Pi _{3}-Ref$ имеет теоретико-доказательный ординал, равный $\Psi (\varepsilon _{K+1})$ , где $K$ относится к первому слабокомпактному виду, поскольку (Rathjen 1993)
${\mathsf {KP}}+\Pi _{\omega }-Ref$ имеет теоретико-доказательный ординал, равный $\Psi _{X}^{\varepsilon _{\Xi +1}}$ , где $\Xi$ относится к первому $\Pi _{0}^{2}$ - неописуемый и $\mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)$ , благодаря (Stegert 2010).
${\mathsf {Stability}}$ имеет теоретико-доказательный ординал, равный $\Psi _{\mathbb {X} }^{\varepsilon _{\Upsilon +1}}$ где $\Upsilon$ является кардинальным аналогом наименьшего порядкового номера $\alpha$ который $\alpha +\beta$ -стабильный для всех $\beta <\alpha$ и $\mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)$ , благодаря (Stegert 2010).

Большинство теорий, способных описать набор степеней натуральных чисел, имеют теоретико-доказательные ординалы, которые настолько велики, что до сих пор не дано явного комбинаторного описания. Это включает в себя $\Pi _{2}^{1}-CA_{0}$ , полная арифметика второго порядка ( $\Pi _{\infty }^{1}-CA_{0}$ ) и теории множеств с наборами полномочий, включая ZF и ZFC. Сила интуиционистского ZF (IZF) равна силе ZF.

Таблица порядковых анализов

Таблица теоретико-доказательных ординалов
Порядковый номер	Арифметика первого порядка	Арифметика второго порядка	Теория множеств Крипке-Платека	Теория типов	Конструктивная теория множеств	Явная математика
$\omega$	${\mathsf {Q}}$ , ${\mathsf {PA}}^{-}$
$\omega ^{2}$	${\mathsf {RFA}}$ , ${\mathsf {I\Delta }}_{0}$
$\omega ^{3}$	${\mathsf {EFA}}$ , ${\mathsf {I\Delta }}_{0}^{\mathsf {+}}$	${\mathsf {RCA}}_{0}^{}$ , ${\mathsf {WKL}}_{0}^{}$
$\omega ^{n}$ ^[1]	${\mathsf {EFA}}^{\mathsf {n}}$ , ${\mathsf {I\Delta }}_{0}^{\mathsf {n+}}$
$\omega ^{\omega }$	${\mathsf {PRA}}$ , ${\mathsf {I\Sigma }}_{1}$ ^[7]^{п. 13}	${\mathsf {RCA}}_{0}$ ^[7]^{п. 13}, ${\mathsf {WKL}}_{0}$ ^[7]^{п. 13}		${\mathsf {CPRC}}$
$\omega ^{\omega ^{\omega ^{\omega }}}$	${\mathsf {I}}\Sigma _{3}$ ^[8]^[7]^{п. 13}	${\mathsf {RCA}}_{0}+(\Pi _{2}^{0})^{-}{\mathsf {-IND}}$ ^[9]^: 40
$\varepsilon _{0}$	${\mathsf {PA}}$ ^[7]^{п. 13}	${\mathsf {ACA}}_{0}$ ^[7]^{п. 13}, ${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA}}_{0}$ , ${\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}_{0}$ ^[7]^{п. 13}, ${\text{R-}}{\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}$ ^[10]^{п. 8}	$\mathrm {KPu} ^{r}$ ^[11]^{п. 869}			${\mathsf {EM}}_{0}$
$\varepsilon _{\omega }$		${\mathsf {ACA}}_{0}+{\mathsf {iRT}}$ , ^[12] ${\mathsf {RCA}}_{0}+\forall Y\forall n\exists X({\textrm {TJ}}(n,X,Y))$ ^[13]^: 8
$\varepsilon _{\varepsilon _{0}}$		${\mathsf {ACA}}$ ^[14]^{п. 959}
$\zeta _{0}$		${\mathsf {ACA}}_{0}+\forall X\exists Y({\textrm {TJ}}(\omega ,X,Y))$ , ^[15]^[13] ${\mathsf {p}}_{1}({\mathsf {ACA}}_{0})$ , ^[16]^: 7 ${\mathsf {RFN}}_{0}$ ^[15]^{п. 17}, ${\mathsf {ACA}}_{0}+({\mathsf {BR}})$ ^[15]^{п. 5}
$\varphi (2,\varepsilon _{0})$		${\mathsf {RFN}}$ , ${\mathsf {ACA}}+\forall X\exists Y({\textrm {TJ}}(\omega ,X,Y))$ ^[15]^{п. 52}
$\varphi (\omega ,0)$	${\mathsf {ID}}_{1}\#$	${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CR}}$ , $\Sigma _{1}^{1}{\mathsf {-DC}}_{0}$ ^[17]				${\mathsf {EM}}_{0}{\mathsf {+JR}}$
$\varphi (\varepsilon _{0},0)$	${\widehat {\mathsf {ID}}}_{1}$ , ${\mathsf {KFL}}$ ^[18]^{п. 17}, ${\mathsf {KF}}$ ^[18]^{п. 17}	${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA}}$ ^[19]^{п. 140}, ${\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}$ ^[19]^{п. 140}, ${\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}}$ ^[19]^{п. 140}, ${\text{W-}}{\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}$ ^[10]^{п. 8}	$\mathrm {KPu} ^{r}+(\mathrm {IND} _{N})$ ^[11]^{п. 870}	${\mathsf {ML}}_{1}$		${\mathsf {EM}}_{0}{\mathsf {+J}}$
$\varphi (\varepsilon _{\varepsilon _{0}},0)$		${\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}$ ^[10]^{п. 27}, ${\widehat {\mathbf {EID} }}_{\boldsymbol {1}}$ ^[10]^{п. 27}
$\varphi (\varphi (\omega ,0),0)$	$\mathrm {PRS} \omega$ ^[20]^стр.9
$\varphi ({\mathsf {<}}\Omega ,0)$ ^[2]	${\mathsf {Aut(ID\#)}}$
$\Gamma _{0}$	${\widehat {\mathsf {ID}}}_{<\omega }$ , ^[21] ${\mathsf {U(PA)}}$ , $\mathbf {KFL} ^{}$ ^[18]^{п. 22}, $\mathbf {KF} ^{}$ ^[18]^{п. 22}, ${\mathcal {U}}(\mathrm {NFA} )$ ^[22]	${\mathsf {ATR}}_{0}$ , ${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA+BR}}$ , $\Delta _{1}^{1}\mathrm {-CA} _{0}+\mathrm {(SUB)}$ , ^[23] $\mathrm {FP} _{0}$ ^[24]^{п. 26}	${\mathsf {KPi}}^{0}$ ^[11]^{п. 878}, ${\mathsf {KPu}}^{0}+(\mathrm {BR} )$ ^[11]^{п. 878}	${\mathsf {ML}}_{<\omega }$ , ${\mathsf {MLU}}$
$\Gamma _{\omega ^{\omega }}$			${\mathsf {KPI}}^{0}+({\mathsf {\Sigma _{1}-I}}_{\omega })$ ^[25]^стр.13
$\Gamma _{\varepsilon _{0}}$	${\widehat {\mathsf {ID}}}_{\omega }$	${\mathsf {ATR}}$ ^[26]	${\mathsf {KPI}}^{0}{\mathsf {+F-I}}_{\omega }$
$\varphi (1,\omega ,0)$	${\widehat {\mathsf {ID}}}_{<\omega ^{\omega }}$	${\mathsf {ATR}}_{0}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}})$ ^[16]^: 7	${\mathsf {KPi}}^{0}{\mathsf {+\Sigma _{1}-I}}_{\omega }$
$\varphi (1,\varepsilon _{0},0)$	${\widehat {\mathsf {ID}}}_{<\varepsilon _{0}}$	${\mathsf {ATR}}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}})$ ^[16]^: 7	${\mathsf {KPi}}^{0}{\mathsf {+F-I}}_{\omega }$
$\varphi (1,\Gamma _{0},0)$	${\widehat {\mathsf {ID}}}_{<\Gamma _{0}}$			${\mathsf {MLS}}$
$\varphi (2,0,0)$	${\mathsf {Aut({\widehat {ID}})}}$ , ${\mathsf {FTR}}_{0}$ ^[27]	$Ax_{\Sigma _{1}^{1}{\mathsf {-AC}}}{\mathsf {TR}}_{0}$ ^[28]^стр.1167, $Ax_{{\mathsf {ATR}}+\Sigma _{1}^{1}{\mathsf {-DC}}}{\mathsf {RFN}}_{0}$ ^[28]^стр.1167	${\mathsf {KPh}}^{0}$	${\mathsf {Aut(ML)}}$
$\varphi (2,0,\varepsilon _{0})$	${\mathsf {FTR}}$ ^[27]	$Ax_{\Sigma _{1}^{1}{\mathsf {-AC}}}{\mathsf {TR}}$ ^[28]^стр.1167, $Ax_{{\mathsf {ATR}}+\Sigma _{1}^{1}{\mathsf {-DC}}}{\mathsf {RFN}}$ ^[28]^стр.1167
$\varphi (2,\varepsilon _{0},0)$			${\mathsf {KPh}}_{0}+({\mathsf {F-I}}_{\omega })$ ^[27]^: 11
$\varphi (\omega ,0,0)$		$(\Pi _{2}^{1}{\mathsf {-RFN}})_{0}^{\Sigma _{1}^{1}{\mathsf {-DC}}}$ ^[29]^стр.233, $\Sigma _{1}^{1}{\mathsf {-TDC}}_{0}$ ^[29]^стр.233	${\mathsf {KPm}}^{0}$ ^[30]^стр.276	${\mathsf {EMA}}$ ^[30]^стр.276
$\varphi (\varepsilon _{0},0,0)$		$(\Pi _{2}^{1}{\mathsf {-RFN}})^{\Sigma _{1}^{1}{\mathsf {-DC}}}$ ^[29]^стр.233, $\Sigma _{1}^{1}{\mathsf {-TDC}}$ ^[16]	${\mathsf {KPm}}^{0}+({\mathcal {L}}^{*}{\mathsf {-I}}_{\mathsf {N}})$ ^[30]^стр.277	${\mathsf {EMA}}+(\mathbb {L} {\mathsf {-I}}_{\mathsf {N}})$ ^[30]^стр.277
$\varphi (1,0,0,0)$		${\mathsf {p}}_{1}(\Sigma _{1}^{1}{\mathsf {-TDC}}_{0})$ ^[16]^: 7
$\psi _{\Omega _{1}}(\Omega ^{\Omega ^{\omega }})$		${\mathsf {RCA}}_{0}^{*}+\Pi _{1}^{1}{\mathsf {-CA}}^{-}$ , ^[31] ${\mathsf {p}}_{3}({\mathsf {ACA}}_{0})$ ^[16]^: 7
$\vartheta (\Omega ^{\Omega })$		${\mathsf {p}}_{1}({\mathsf {p}}_{3}({\mathsf {ACA}}_{0}))$ ^[16]^: 7
$\psi _{0}(\varepsilon _{\Omega +1})$ ^[3]	${\mathsf {ID}}_{1}$	${\text{W-}}{\widetilde {\mathbf {E} {\boldsymbol {\Omega }}}}$ ^[10]^{п. 8}	${\mathsf {KP}}$ , ^[2] ${\mathsf {KP\omega }}$ , $\mathrm {KPu}$ ^[11]^{п. 869}	${\mathsf {ML}}_{1}{\mathsf {V}}$	${\mathsf {CZF}}$	${\mathsf {EON}}$
$\psi (\varepsilon _{\Omega +\varepsilon _{0}})$		${\widetilde {\mathbf {E} {\boldsymbol {\Omega }}}}$ ^[10]^{п. 31}, ${\widetilde {\mathbf {EID} }}_{\boldsymbol {1}}$ ^[10]^{п. 31}, $\mathbf {ACA} +(\Pi _{1}^{1}{\text{-CA}})^{-}$ ^[10]^{п. 31}
$\psi (\varepsilon _{\Omega +\Omega })$		$({\mathsf {ID}}_{1}^{2})_{0}+{\mathsf {BR}}$ ^[32]
$\psi (\varepsilon _{\varepsilon _{\Omega +1}})$		$\mathbf {E} {\boldsymbol {\Omega }}$ ^[10]^{п. 33}, $\mathbf {EID} _{\boldsymbol {1}}$ ^[10]^{п. 33}, $\mathbf {ACA} +(\Pi _{1}^{1}{\text{-CA}})^{-}+(\mathrm {BI} _{\mathrm {PR} })^{-}$ ^[10]^{п. 33}
$\psi _{0}(\Gamma _{\Omega +1})$ ^[4]	${\mathsf {U(ID}}_{1}{\mathsf {)}}$ , ${\widehat {\mathsf {ID}}}_{<\omega }^{\bullet }$ ^[24]^{п. 26}, $\Sigma _{1}^{1}{\mathsf {-DC}}_{0}^{\bullet }+({\mathsf {SUB}}^{\bullet })$ ^[24]^{п. 26}, ${\mathsf {ATR}}_{0}^{\bullet }$ ^[24]^{п. 26}, $\Sigma _{1}^{1}{\mathsf {-AC}}_{0}^{\bullet }+({\mathsf {SUB}}^{\bullet })$ ^[24]^{п. 26}, ${\mathcal {U}}({\mathsf {ID}}_{1})$ ^[24]^{п. 26}	${\mathsf {FP}}_{0}^{\bullet }$ ^[24]^{п. 26}, ${\mathsf {ATR}}_{0}^{\bullet }$ ^[24]^{п. 26}
$\psi _{0}(\varphi ({\mathsf {<}}\Omega ,0,\Omega +1))$	${\mathsf {Aut(U(ID))}}$
$\psi _{0}(\Omega _{\omega })$	${\mathsf {ID}}_{<\omega }$ ^[4]^{п. 28}	${\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}_{0}$ ^[4]^{п. 28}, ${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}_{0}$		${\mathsf {MLW}}$
$\psi _{0}(\Omega _{\omega }\omega ^{\omega })$	$\Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-IND}}$ ^[33]
$\psi _{0}(\Omega _{\omega }\varepsilon _{0})$	${\mathsf {W-ID}}_{\omega }$	${\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}$ ^[34]^{п. 14}	${\mathsf {W-KPI}}$
$\psi _{0}(\Omega _{\omega }\Omega )$		$\Pi _{1}^{1}{\mathsf {-CA+BR}}$ ^[35]
$\psi _{0}(\Omega _{\omega }^{\omega })$		$\Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-BI}}$ ^[33]
$\psi _{0}(\Omega _{\omega }^{\omega ^{\omega }})$		$\Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-BI}}+\Pi _{3}^{1}{\mathsf {-IND}}$ ^[33]
$\psi _{0}(\varepsilon _{\Omega _{\omega }+1})$ ^[5]	${\mathsf {ID}}_{\omega }$	${\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA+BI}}$	${\mathsf {KPI}}$
$\psi _{0}(\Omega _{\omega ^{\omega }})$	${\mathsf {ID}}_{<\omega ^{\omega }}$	${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CR}}$ ^[4]^{п. 28}
$\psi _{0}(\Omega _{\varepsilon _{0}})$	${\mathsf {ID}}_{<\varepsilon _{0}}$	${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}$ ^[4]^{п. 28}, ${\mathsf {\Sigma }}_{2}^{1}{\mathsf {-AC}}$	${\mathsf {W-KPi}}$
$\psi _{0}(\Omega _{\Omega })$	${\mathsf {Aut(ID)}}$ ^[6]
$\psi _{\Omega _{1}}(\varepsilon _{\Omega _{\Omega }+1})$	${\mathsf {ID}}_{\prec ^{}}$ , ${\mathsf {BID}}^{2}$ , ${\mathsf {ID}}^{2*}+{\mathsf {BI}}$ ^[36]		${\mathsf {KPl}}^{*}$ , ${\mathsf {KPl}}_{\Omega }^{r}$
$\psi _{0}(\Phi _{1}(0))$		$\Pi _{1}^{1}{\mathsf {-TR}}_{0}$ , $\Pi _{1}^{1}{\mathsf {-TR}}_{0}+\Delta _{2}^{1}{\mathsf {-CA}}_{0}$ , $\Delta _{2}^{1}{\mathsf {-CA+BI(impl-}}\Sigma _{2}^{1})$ , $\Delta _{2}^{1}{\mathsf {-CA+BR(impl-}}\Sigma _{2}^{1})$ , $\mathbf {AUT-ID} _{0}^{pos}$ , $\mathbf {AUT-ID} _{0}^{mon}$ ^[36]^: 72	${\mathsf {KPi}}^{w}+{\mathsf {FOUNDR}}({\mathsf {impl-}})\Sigma )$ , ^[36]^: 72 ${\mathsf {KPi}}^{w}+{\mathsf {FOUND}}({\mathsf {impl-}})\Sigma )$ ^[36]^: 72	$\mathbf {AUT-KPl} ^{r}$ , $\mathbf {AUT-KPl} ^{r}+\mathbf {KPi} ^{r}$ ^[36]^: 72
$\psi _{0}(\Phi _{1}(0)\varepsilon _{0})$		$\Pi _{1}^{1}{\mathsf {-TR}}$ , $\mathbf {AUT-ID} ^{pos}$ , $\mathbf {AUT-ID} ^{mon}$ ^[36]^: 72	$\mathbf {AUT-KPl} ^{w}$ ^[36]^: 72
$\psi _{0}(\varepsilon _{\Phi _{1}(0)+1})$		$\Pi _{1}^{1}{\mathsf {-TR}}+({\mathsf {BI}})$ , $\mathbf {AUT-ID} _{2}^{pos}$ , $\mathbf {AUT-ID} _{2}^{mon}$ ^[36]^: 72	$\mathbf {AUT-KPl}$ ^[36]^: 72
$\psi _{0}(\Phi _{1}(\varepsilon _{0}))$		$\Pi _{1}^{1}{\mathsf {-TR}}+\Delta _{2}^{1}{\mathsf {-CA}}$ , $\Pi _{1}^{1}{\mathsf {-TR}}+\Sigma _{2}^{1}{\mathsf {-AC}}$ , $\mathbf {AUT-KPl} ^{w}+\mathbf {KPi} ^{w}$ ^[36]^: 72
$\psi _{0}(\Phi _{\omega }(0))$		$\Delta _{2}^{1}{\mathsf {-TR}}_{0}$ , $\Sigma _{2}^{1}{\mathsf {-TRDC}}_{0}$ , $\Delta _{2}^{1}{\mathsf {-CA}}_{0}+(\Sigma _{2}^{1}{\mathsf {-BI}})$ ^[36]^: 72	$\mathbf {KPi} ^{r}+(\Sigma {\mathsf {-FOUND}})$ , $\mathbf {KPi} ^{r}+(\Sigma {\mathsf {-REC}})$ ^[36]^: 72
$\psi _{0}(\Phi _{\varepsilon _{0}}(0))$		$\Delta _{2}^{1}{\mathsf {-TR}}$ , $\Sigma _{2}^{1}{\mathsf {-TRDC}}$ , $\Delta _{2}^{1}{\mathsf {-CA}}+(\Sigma _{2}^{1}{\mathsf {-BI}})$ ^[36]^: 72	$\mathbf {KPi} ^{w}+(\Sigma {\mathsf {-FOUND}})$ , $\mathbf {KPi} ^{w}+(\Sigma {\mathsf {-REC}})$ ^[36]^: 72
$\psi (\varepsilon _{I+1})$ ^[7]		${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}$ ^[4]^{п. 28}, ${\mathsf {\Sigma }}_{2}^{1}{\mathsf {-AC+BI}}$	${\mathsf {KPi}}$		${\mathsf {CZF+REA}}$	${\mathsf {T}}_{0}$
$\psi (\Omega _{I+\omega })$				${\mathsf {ML}}_{1}{\mathsf {W}}$ ^[37]^: 38
$\psi (\Omega _{L})$ ^[8]			${\mathsf {KPh}}$	${\mathsf {ML}}_{<\omega }{\mathsf {W}}$
$\psi (\Omega _{L^{*}})$ ^[9]				${\mathsf {Aut(MLW)}}$
$\psi _{\Omega }(\chi _{\varepsilon _{M+1}}(0))$ ^[10]		${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}$	${\mathsf {KPM}}$		${\mathsf {CZFM}}$
$\psi (\Omega _{M+\omega })$ ^[11]			${\mathsf {KPM}}^{+}$ ^[38]	${\mathsf {TTM}}$ ^[38]
$\Psi _{\Omega }^{0}(\varepsilon _{K+1})$ ^[12]			${\mathsf {KP+\Pi }}_{3}-{\mathsf {Ref}}$ ^[39]
$\Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _{\Xi +1}}$ ^[13]			${\mathsf {KP+\Pi }}_{\omega }-{\mathsf {Ref}}$ ^[40]
$\Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _{\Upsilon +1}}$ ^[14]			${\mathsf {Stability}}$ ^[40]
$\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {S} ^{+}+1})$ ^[41]			${\mathsf {KP}}\omega +\Pi _{1}^{1}-{\mathsf {Ref}}$ , ^[41] ${\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)$ ^[42]
$\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})$ ^[41]		$\Sigma _{3}^{1}{\mathsf {-DC+BI}}$ , $\Sigma _{3}^{1}{\mathsf {-AC+BI}}$	${\mathsf {KP}}\omega +\Pi _{1}-{\mathsf {Collection}}+(V=L)$
$\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{N}+1})$ ^[43]		$\Sigma _{N+2}^{1}{\mathsf {-DC+BI}}$ , $\Sigma _{N+2}^{1}{\mathsf {-AC+BI}}$	${\mathsf {KP}}\omega +\Pi _{N}-{\mathsf {Collection}}+(V=L)$
?	${\mathsf {PA}}+\bigcup \limits _{N<\omega }{\mathsf {TI}}[\Pi _{0}^{1-},\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{N}+1})]$ ^[43]	$\mathbf {Z} _{2}$ , $\Pi _{\infty }^{1}-{\mathsf {CA}}$	${\mathsf {KP}}+\Pi _{\omega }^{\text{set}}-{\mathsf {Separation}}$	$\lambda 2$ ^[44]

Ключ

Это список символов, используемых в этой таблице:

ψ представляет собой различные порядковые функции свертывания , определенные в соответствующих цитатах.
Ψ представляет собой Пси Ратьена или Стегерта.
φ представляет функцию Веблена.
ω представляет собой первый трансфинитный порядковый номер.
ε _α представляет числа эпсилон .
Γ _α представляет собой гамма-числа (Γ ₀ — ординал Фефермана – Шютте )
Ω _α представляют собой несчетные ординалы (Ω ₁ , сокращенно Ω, представляет собой ω ₁ ). Счетность считается необходимой для того, чтобы порядковый номер считался теоретико-доказательным.
$\mathbb {S}$ является порядковым термином, обозначающим стабильный порядковый номер, и $\mathbb {S} ^{+}$ наименьший допустимый порядковый номер выше $\mathbb {S}$ .
$\mathbb {I} _{N}$ порядковый термин, обозначающий порядковый номер такой, что $L_{\mathbb {I} _{N}}\models {\mathsf {KP}}\omega +\Pi _{N}-{\mathsf {Collection}}+(V=L)$ . N — переменная, определяющая серию порядковых анализов результатов $\Pi _{N}-{\mathsf {Collection}}$ навсегда $1\leq N<\omega$ . когда N=1, $\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{1}+1})=\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})$

Вот список сокращений, используемых в этой таблице:

Арифметика первого порядка
- ${\mathsf {Q}}$ это арифметика Робинсона
- ${\mathsf {PA}}^{-}$ — теория первого порядка неотрицательной части дискретно упорядоченного кольца.
- ${\mathsf {RFA}}$ это элементарная арифметика функций.
- ${\mathsf {I\Delta }}_{0}$ - это арифметика с индукцией, ограниченной ₀ -предикатами, без какой-либо аксиомы, утверждающей, что возведение в степень является полным.
- ${\mathsf {EFA}}$ это элементарная арифметика функций .
- ${\mathsf {I\Delta }}_{0}^{\mathsf {+}}$ — это арифметика с индукцией, ограниченной 0-предикатами Δ _, дополненной аксиомой, утверждающей, что возведение в степень является полным.
- ${\mathsf {EFA}}^{\mathsf {n}}$ — это арифметика элементарной функции, дополненная аксиомой, гарантирующей, что каждый элемент n -го уровня ${\mathcal {E}}^{n}$ иерархии Гжегорчика является тотальной.
- ${\mathsf {I\Delta }}_{0}^{\mathsf {n+}}$ является ${\mathsf {I\Delta }}_{0}^{\mathsf {+}}$ дополнен аксиомой, гарантирующей, что каждый элемент n -го уровня ${\mathcal {E}}^{n}$ иерархии Гжегорчика является тотальной.
- ${\mathsf {PRA}}$ это примитивно-рекурсивная арифметика .
- ${\mathsf {I\Sigma }}_{1}$ является арифметикой с индукцией, ограниченной Σ ₁ -предикатами.
- ${\mathsf {PA}}$ это арифметика Пеано .
- ${\mathsf {ID}}_{\nu }\#$ является ${\widehat {\mathsf {ID}}}_{\nu }$ но с индукцией только для положительных формул.
- ${\widehat {\mathsf {ID}}}_{\nu }$ расширяет PA на ν итерированных неподвижных точек монотонных операторов.
- ${\mathsf {U(PA)}}$ это не совсем арифметическая система первого порядка, но она отражает то, что можно получить с помощью предикативных рассуждений, основанных на натуральных числах.
- ${\mathsf {Aut({\widehat {ID}})}}$ является автоморфизмом на ${\widehat {\mathsf {ID}}}_{\nu }$ .
- ${\mathsf {ID}}_{\nu }$ расширяет PA на ν итерированных наименьших неподвижных точек монотонных операторов.
- ${\mathsf {U(ID}}_{\nu }{\mathsf {)}}$ не является арифметической системой первого порядка, но отражает то, что можно получить с помощью предикативных рассуждений, основанных на ν-кратно повторенных обобщенных индуктивных определениях.
- ${\mathsf {Aut(U(ID))}}$ является автоморфизмом на ${\mathsf {U(ID}}_{\nu }{\mathsf {)}}$ .
- ${\mathsf {W-ID}}_{\nu }$ представляет собой ослабленную версию ${\mathsf {ID}}_{\nu }$ на основе W-типов.
- ${\mathsf {TI}}[\Pi _{0}^{1-},\alpha ]$ — трансфинитная индукция длины α не более $\Pi _{0}^{1}$ -формулы. Это представление порядкового обозначения при использовании в арифметике первого порядка.

Арифметика второго порядка
- ${\mathsf {RCA}}_{0}^{*}$ является формой второго порядка ${\mathsf {EFA}}$ иногда используется в обратной математике .
- ${\mathsf {WKL}}_{0}^{*}$ является формой второго порядка ${\mathsf {EFA}}$ иногда используется в обратной математике.
- ${\mathsf {RCA}}_{0}$ это рекурсивное понимание .
- ${\mathsf {WKL}}_{0}$ является слабой леммой Кенига .
- ${\mathsf {ACA}}_{0}$ это арифметическое понимание .
- ${\mathsf {ACA}}$ является ${\mathsf {ACA}}_{0}$ плюс полная схема индукции второго порядка.
- ${\mathsf {ATR}}_{0}$ это арифметическая трансфинитная рекурсия .
- ${\mathsf {ATR}}$ является ${\mathsf {ATR}}_{0}$ плюс полная схема индукции второго порядка.
- ${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}$ является ${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}$ плюс утверждение «всякое истинное ${\mathsf {\Pi }}_{3}^{1}$ -предложение с параметрами содержится в (исчисляемом коде) $\beta$ -модель ${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}$ ".

Теория множеств Крипке-Платека
- ${\mathsf {KP}}$ — теория множеств Крипке-Платека с аксиомой бесконечности.
- ${\mathsf {KP\omega }}$ — это теория множеств Крипке-Платека, вселенная которой представляет собой допустимое множество, содержащее $\omega$ .
- ${\mathsf {W-KPI}}$ представляет собой ослабленную версию ${\mathsf {KPI}}$ на основе W-типов.
- ${\mathsf {KPI}}$ утверждает, что Вселенная представляет собой предел допустимых множеств.
- ${\mathsf {W-KPi}}$ представляет собой ослабленную версию ${\mathsf {KPi}}$ на основе W-типов.
- ${\mathsf {KPi}}$ утверждает, что Вселенная состоит из недоступных множеств.
- ${\mathsf {KPh}}$ утверждает, что Вселенная гипердоступна: недоступное множество и предел недоступных множеств.
- ${\mathsf {KPM}}$ утверждает, что Вселенная представляет собой множество Мало.
- ${\mathsf {KP+\Pi }}_{\mathsf {n}}-{\mathsf {Ref}}$ является ${\mathsf {KP}}$ дополненный некоторой схемой отражения первого порядка.
- ${\mathsf {Stability}}$ KPi дополнен аксиомой $\forall \alpha \exists \kappa \geq \alpha (L_{\kappa }\preceq _{1}L_{\kappa +\alpha })$ .
- ${\mathsf {KPM}}^{+}$ KPI дополнен утверждением «существует хотя бы один рекурсивно порядковый номер Мало».
- ${\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)$ является ${\mathsf {KP}}\omega$ с аксиомой, утверждающей, что «существует непустое и транзитивное множество M такое, что $M\prec _{\Sigma _{1}}V$ '.

Верхний индекс ноль указывает на то, что $\in$ -индукция удаляется (что делает теорию существенно слабее).

Теория типов
- ${\mathsf {CPRC}}$ — это исчисление примитивных рекурсивных конструкций Гербелена-Пэти.
- ${\mathsf {ML}}_{\mathsf {n}}$ это теория типов без W-типов и с $n$ вселенные.
- ${\mathsf {ML}}_{<\omega }$ — это теория типов без W-типов и с конечным числом вселенных.
- ${\mathsf {MLU}}$ это теория типов с оператором следующей вселенной.
- ${\mathsf {MLS}}$ — это теория типов без W-типов и со сверхвселенной.
- ${\mathsf {Aut(ML)}}$ является автоморфизмом теории типов без W-типов.
- ${\mathsf {ML}}_{1}{\mathsf {V}}$ - это теория типов с одной вселенной и итеративными множествами типа Акселя.
- ${\mathsf {MLW}}$ — это теория типов с индексированными W-типами.
- ${\mathsf {ML}}_{1}{\mathsf {W}}$ — это теория типов с W-типами и одной вселенной.
- ${\mathsf {ML}}_{<\omega }{\mathsf {W}}$ — это теория типов с W-типами и конечным числом вселенных.
- ${\mathsf {Aut(MLW)}}$ является автоморфизмом теории типов с W-типами.
- ${\mathsf {TTM}}$ — это теория типов со вселенной Мало.
- $\lambda 2$ Система F , также полиморфное лямбда-исчисление или лямбда-исчисление второго порядка.

Конструктивная теория множеств
- ${\mathsf {CZF}}$ — это конструктивная теория множеств Акселя.
- ${\mathsf {CZF+REA}}$ является ${\mathsf {CZF}}$ плюс аксиома регулярного расширения.
- ${\mathsf {CZF+REA+FZ}}_{2}$ является ${\mathsf {CZF+REA}}$ плюс схема индукции полного второго порядка.
- ${\mathsf {CZFM}}$ является ${\mathsf {CZF}}$ со вселенной Глаз.

Явная математика
- ${\mathsf {EM}}_{0}$ это базовая явная математика плюс элементарное понимание
- ${\mathsf {EM}}_{0}{\mathsf {+JR}}$ является ${\mathsf {EM}}_{0}$ плюс правило объединения
- ${\mathsf {EM}}_{0}{\mathsf {+J}}$ является ${\mathsf {EM}}_{0}$ плюс присоединяйтесь к аксиомам
- ${\mathsf {EON}}$ является слабым вариантом Фефермана . ${\mathsf {T}}_{0}$ .
- ${\mathsf {T}}_{0}$ является ${\mathsf {EM}}_{0}{\mathsf {+J+IG}}$ , где ${\mathsf {IG}}$ является индуктивной генерацией.
- ${\mathsf {T}}$ является ${\mathsf {EM}}_{0}{\mathsf {+J+IG+FZ}}_{2}$ , где ${\mathsf {FZ}}_{2}$ — полная схема индукции второго порядка.

См. также

Примечания

1. ^ Для

1<n\leq \omega

2. ^ Функция Веблена

\varphi

со счетно-бесконечно повторяемыми наименьшими неподвижными точками. ^{[ нужны разъяснения ]}

3. ^ Также обычно можно записать как

\psi (\varepsilon _{\Omega +1})

в ψ Мадора.

4. ^ Использует ψ Мадора, а не ψ Бухгольца.

5. ^ Также обычно можно записать как

\psi (\varepsilon _{\Omega _{\omega }+1})

в ψ Мадора.

6. ^

K

представляет первый рекурсивно слабо компактный ординал. Использует ψ Араи, а не ψ Бухгольца.

7. ^ Также теоретико-доказательный ординал

{\mathsf {Aut(W-ID)}}

, поскольку степень ослабления, даваемая W-типами, недостаточна.

8. ^

I

представляет собой первого недоступного кардинала. Использует ψ Егера, а не ψ Бухгольца.

9. ^

L

представляет собой предел

\omega

- недоступные кардиналы. Использует (предположительно) ψ Ягера.

10. ^

L^{*}

представляет собой предел

\Omega

- недоступные кардиналы. Использует (предположительно) ψ Ягера.

11. ^

M

представляет первого кардинала Мало. Использует ψ Ратьена, а не ψ Бухгольца.

12. ^

K

представляет собой первый слабо компактный кардинал. Использует Ψ Ратьена, а не ψ Бухгольца.

13. ^

\Xi

представляет собой первый

\Pi _{0}^{2}

- неописуемый кардинал. Использует Ψ Стегерта, а не ψ Бухгольца.

14. ^

Y

самый маленький

\alpha

такой, что

\forall \theta <Y\exists \kappa <Y(

'

\kappa

является

\theta

- неописуемый») и

\forall \theta <Y\forall \kappa <Y(

'

\kappa

является

\theta

- неописуемый

\rightarrow \theta <\kappa

'). Использует Ψ Стегерта, а не ψ Бухгольца.

15. ^

M

представляет первого кардинала Мало. Использует (предположительно) ψ Ратьена.

Цитаты

^ М. Ратьен, « Теория допустимых доказательств и не только ». В исследованиях по логике и основам математики, том. 134 (1995), стр. 123-147.
^ Jump up to: Перейти обратно: ^а ^б ^с Ратьен, Область порядкового анализа . По состоянию на 29 сентября 2021 г.
^ Крайчек, Ян (1995). Ограниченная арифметика, логика высказываний и теория сложности . Издательство Кембриджского университета. стр. 18–20 . ISBN 9780521452052 . определяет рудиментарные множества и рудиментарные функции и доказывает их эквивалентность ₀ -предикатам натуральных чисел. Порядковый анализ системы можно найти в Роуз, HE (1984). Субрекурсия: функции и иерархии . Мичиганский университет: Clarendon Press. ISBN 9780198531890 .
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж М. Ратьен, Теория доказательств: от арифметики к теории множеств (стр. 28). По состоянию на 14 августа 2022 г.
^ Ратьен, Майкл (2006), «Искусство порядкового анализа» (PDF) , Международный конгресс математиков , том. II, Цюрих: Евр. Математика. Soc., стр. 45–69, MR 2275588 , заархивировано из оригинала 22 декабря 2009 г. {{citation}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
^ Д. Мадор, Зоопарк ординалов (2017, стр.2). По состоянию на 12 августа 2022 г.
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г Дж. Авигад, Р. Соммер, « Теоретико-модельный подход к порядковому анализу » (1997).
^ М. Ратьен, В. Карниелли, « Гидры и подсистемы арифметики » (1991)
^ Йерун Ван дер Меерен; Ратьен, Майкл; Вейерманн, Андреас (2014). «Теоретико-порядковая характеристика иерархии Говарда-Бахмана». arXiv : 1411.4481 [ math.LO ].
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к Г. Йегер, Т. Страм, « Теории второго порядка с ординалами и элементарным пониманием ».
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и Г. Йегер, « Сила приемлемости без основания ». Журнал символической логики, том. 49, нет. 3 (1984).
^ Б. Афшари, М. Ратьен, «Порядковый анализ и бесконечная теорема Рамсея» (2012)
^ Jump up to: Перейти обратно: ^а ^б Марконе, Альберто; Монтальбан, Антонио (2011). «Функции Веблена для теоретиков вычислимости». Журнал символической логики . 76 (2): 575–602. arXiv : 0910.5442 . дои : 10.2178/jsl/1305810765 . S2CID 675632 .
^ С. Феферман, «Теории конечного типа, связанные с математической практикой». В Справочнике по математической логике , Исследованиях по логике и основам математики, том. 90 (1977), изд. Дж. Барвайз, паб. Северная Голландия.
^ Jump up to: Перейти обратно: ^а ^б ^с ^д М. Хайсенбюттель, «Теории порядковой силы». $\varphi 20$ и $\varphi 2\varepsilon _{0}$ » (2001)
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г Д. Пробст, «Модульный порядковый анализ метапредикативных подсистем арифметики второго порядка» (2017)
^ А. Кантини, «О связи между принципами выбора и понимания в арифметике второго порядка», Journal of Символическая логика, том. 51 (1986), стр. 360-373.
^ Jump up to: Перейти обратно: ^а ^б ^с ^д Фишер, Мартин; Николай, Карло; Пабло Допико Фернандес (2020). «Неклассическая истина с классической силой. Теоретико-доказательный анализ композиционной истины над HYPE». arXiv : 2007.07188 [ math.LO ].
^ Jump up to: Перейти обратно: ^а ^б ^с С.Г. Симпсон, «Исследование Фридмана подсистем арифметики второго порядка». В «Исследованиях Харви Фридмана по основам математики» , «Исследования по логике и основам математики», том. 117 (1985), изд. Л. Харрингтон, М. Морли, А. Щедров, С.Г. Симпсон, паб. Северная Голландия.
^ Дж. Авигад, « Порядковый анализ допустимой теории множеств с использованием рекурсии по порядковым обозначениям ». Журнал математической логики, том. 2, нет. 1, стр. 91-112 (2002).
^ С. Феферман, « Итеративные индуктивные теории фиксированной точки: применение гипотезы Хэнкока ». В Патрасском симпозиуме по логике , Исследования по логике и основам математики, том. 109 (1982).
^ С. Феферман, Т. Страм, « Развертывание нефинитистской арифметики », Анналы чистой и прикладной логики, том. 104, №1--3 (2000), стр.75--96.
^ С. Феферман, Г. Ягер, «Принципы выбора, правило бара и автономно повторяющиеся схемы понимания в анализе», Journal of Символическая логика, том. 48, нет. (1983), стр. 63-70.
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час У. Бухгольц, Г. Йегер, Т. Страм, « Теории теоретико-доказательной силы ». $\psi (\Gamma _{\Omega +1})$ В книге « Концепции доказательства в математике, философии и информатике» (2016), под ред. Д. Пробста, П. Шустера. DOI 10.1515/9781501502620-007.
^ Т. Страм, « Автономные прогрессии с фиксированной запятой и трансфинитная рекурсия с фиксированной запятой » (2000). В коллоквиуме по логике '98 , под ред. С.Р. Бусс, П. Гаек и П. Пудлак. DOI 10.1017/9781316756140.031
^ Г. Ягер, Т. Страм, «Теории фиксированной точки и зависимый выбор». Архив математической логики, том. 39 (2000), стр. 493–508.
^ Jump up to: Перейти обратно: ^а ^б ^с Т. Страм, «Автономные прогрессии с фиксированной запятой и трансфинитная рекурсия с фиксированной запятой» (2000)
^ Jump up to: Перейти обратно: ^а ^б ^с ^д К. Рюде, « Трансфинитно-зависимый выбор и отражение ω-модели ». Журнал символической логики, том. 67, нет. 3 (2002).
^ Jump up to: Перейти обратно: ^а ^б ^с К. Рюде, " Теоретико-доказательный анализ Σ ¹₁ трансфинитно-зависимый выбор ». Анналы чистой и прикладной логики, том 122 (2003).
^ Jump up to: Перейти обратно: ^а ^б ^с ^д Т. Страм, « Упорядоченные доказательства для метапредикативного Мало ». Журнал символической логики, том. 67, нет. 1 (2002)
^ Ф. Ранци, Т. Страм, «Гибкая система типов для малого порядкового номера Веблена» (2019). Архив математической логики 58: 711–751.
^ К. Фудзимото, "Заметки о некоторых системах повторных индуктивных определений второго порядка и $\Pi _{1}^{1}$ -понимания и соответствующие подсистемы теории множеств». Анналы чистой и прикладной логики, т. 166 (2015), стр. 409--463.
^ Jump up to: Перейти обратно: ^а ^б ^с Кромбхольц, Мартин; Ратьен, Майкл (2019). «Верхние оценки малой теоремы о графе». arXiv : 1907.00412 [ math.LO ].
^ В. Бухгольц, С. Феферман, В. Полерс, В. Зиг, Повторные индуктивные определения и подсистемы анализа: недавние исследования теории доказательств
^ В. Бухгольц, Теория доказательств импредикативных подсистем анализа (Исследования по теории доказательств, Монографии, Том 2 (1988)
^ Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н М. Ратьен, « Исследования подсистем арифметики второго порядка и теории множеств в силе между $\Pi _{1}^{1}{\mathsf {-CA}}$ и $\Delta _{2}^{1}{\mathsf {-CA+BI}}$ : Часть I ». По состоянию на 21 сентября 2023 г.
^ М. Ратьен, « Сила некоторых теорий типа Мартина-Лёфа »
^ Jump up to: Перейти обратно: ^а ^б А. Сетцер, « Модель теории типов со вселенной Мало » (1996).
^ М. Ратьен, « Теория доказательства отражения ». Анналы чистой и прикладной логики, том. 68, вып. 2 (1994), стр. 181–224.
^ Jump up to: Перейти обратно: ^а ^б Стегерт, Ян-Карл, « Порядковая теория доказательства теории множеств Крипке-Платека, дополненная принципами сильного отражения » (2010).
^ Jump up to: Перейти обратно: ^а ^б ^с Арай, Тошиясу (01 апреля 2023 г.). «Лекции по порядковому анализу». arXiv : 2304.00246 [ math.LO ].
^ Арай, Тосиясу (07 апреля 2023 г.). «Обоснованное доказательство $\Pi _{1}^{1}$ -отражение». arXiv : 2304.03851 [ math.LO ].
^ Jump up to: Перейти обратно: ^а ^б Арай, Тошиясу (12 февраля 2024 г.). «Обычный анализ $\Pi _{N}$ -Коллекция». arXiv : 2311.12459 [ math.LO ].
^ Валентин Блот. « Прямая вычислительная интерпретация арифметики второго порядка посредством рекурсии обновления » (2022 г.).

Ссылки

Бухгольц, В.; Феферман, С.; Полерс, В.; Зиг, В. (1981), Итерированные индуктивные определения и подсистемы анализа , Конспекты лекций по математике, том. 897, Берлин: Springer-Verlag, номер номера : 10.1007/BFb0091894 , ISBN. 978-3-540-11170-2
Полерс, Вольфрам (1989), Теория доказательств , Конспекты лекций по математике, том. 1407, Берлин: Springer-Verlag, номер домена : 10.1007/978-3-540-46825-7 , ISBN. 3-540-51842-8 , МР 1026933
Полерс, Вольфрам (1998), «Теория множеств и теория чисел второго порядка», Справочник по теории доказательств , Исследования по логике и основам математики, том. 137, Амстердам: Elsevier Science BV, стр. 210–335, doi : 10.1016/S0049-237X(98)80019-0 , ISBN. 0-444-89840-9 , МР 1640328
Ратьен, Майкл (1990), «Порядковые обозначения, основанные на слабом кардинале Мало», Arch. Математика. Логика , 29 (4): 249–263, doi : 10.1007/BF01651328 , MR 1062729 , S2CID 14125063
Ратьен, Майкл (2006), «Искусство порядкового анализа» (PDF) , Международный конгресс математиков , том. II, Цюрих: Евр. Математика. Soc., стр. 45–69, MR 2275588 , заархивировано из оригинала 22 декабря 2009 г. {{citation}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
Роуз, HE (1984), Субрекурсия. Функции и иерархии , Оксфордские руководства по логике, том. 9, Оксфорд, Нью-Йорк: Clarendon Press, Oxford University Press.
Шютте, Курт (1977), Теория доказательств , Основы математических наук, том. 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 , МР 0882549
Ратьен, Майкл (1994), «Теория доказательства отражения» , Annals of Pure and Applied Logic , 68 (2): 181–224, doi : 10.1016/0168-0072(94)90074-4
Стегерт, Ян-Карл (2010), Порядковая теория доказательства теории множеств Крипке-Платека, дополненная принципами сильного отражения

[1] М. Ратьен, « Теория допустимых доказательств и не только ». В исследованиях по логике и основам математики, том. 134 (1995), стр. 123-147.

[Realm-2] Jump up to: Перейти обратно: ^а ^б ^с Ратьен, Область порядкового анализа . По состоянию на 29 сентября 2021 г.

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

[RathjenFromArithmetic-4] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж М. Ратьен, Теория доказательств: от арифметики к теории множеств (стр. 28). По состоянию на 14 августа 2022 г.

[5] Ратьен, Майкл (2006), «Искусство порядкового анализа» (PDF) , Международный конгресс математиков , том. II, Цюрих: Евр. Математика. Soc., стр. 45–69, MR 2275588 , заархивировано из оригинала 22 декабря 2009 г. {{citation}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )

[6] Д. Мадор, Зоопарк ординалов (2017, стр.2). По состоянию на 12 августа 2022 г.

[AvigadSommer97-7] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г Дж. Авигад, Р. Соммер, « Теоретико-модельный подход к порядковому анализу » (1997).

[8] М. Ратьен, В. Карниелли, « Гидры и подсистемы арифметики » (1991)

[9] Йерун Ван дер Меерен; Ратьен, Майкл; Вейерманн, Андреас (2014). «Теоретико-порядковая характеристика иерархии Говарда-Бахмана». arXiv : 1411.4481 [ math.LO ].

[JagerStrahm-10] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к Г. Йегер, Т. Страм, « Теории второго порядка с ординалами и элементарным пониманием ».

[Jäger84-11] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и Г. Йегер, « Сила приемлемости без основания ». Журнал символической логики, том. 49, нет. 3 (1984).

[12] Б. Афшари, М. Ратьен, «Порядковый анализ и бесконечная теорема Рамсея» (2012)

[MarconeMontalbán2010-13] Jump up to: Перейти обратно: ^а ^б Марконе, Альберто; Монтальбан, Антонио (2011). «Функции Веблена для теоретиков вычислимости». Журнал символической логики . 76 (2): 575–602. arXiv : 0910.5442 . дои : 10.2178/jsl/1305810765 . S2CID 675632 .

[14] С. Феферман, «Теории конечного типа, связанные с математической практикой». В Справочнике по математической логике , Исследованиях по логике и основам математики, том. 90 (1977), изд. Дж. Барвайз, паб. Северная Голландия.

[Heissenbüttel2001-15] Jump up to: Перейти обратно: ^а ^б ^с ^д М. Хайсенбюттель, «Теории порядковой силы». $\varphi 20$ и $\varphi 2\varepsilon _{0}$ » (2001)

[Probst2017-16] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г Д. Пробст, «Модульный порядковый анализ метапредикативных подсистем арифметики второго порядка» (2017)

[17] А. Кантини, «О связи между принципами выбора и понимания в арифметике второго порядка», Journal of Символическая логика, том. 51 (1986), стр. 360-373.

[FNF20-18] Jump up to: Перейти обратно: ^а ^б ^с ^д Фишер, Мартин; Николай, Карло; Пабло Допико Фернандес (2020). «Неклассическая истина с классической силой. Теоретико-доказательный анализ композиционной истины над HYPE». arXiv : 2007.07188 [ math.LO ].

[Simpson85-19] Jump up to: Перейти обратно: ^а ^б ^с С.Г. Симпсон, «Исследование Фридмана подсистем арифметики второго порядка». В «Исследованиях Харви Фридмана по основам математики» , «Исследования по логике и основам математики», том. 117 (1985), изд. Л. Харрингтон, М. Морли, А. Щедров, С.Г. Симпсон, паб. Северная Голландия.

[20] Дж. Авигад, « Порядковый анализ допустимой теории множеств с использованием рекурсии по порядковым обозначениям ». Журнал математической логики, том. 2, нет. 1, стр. 91-112 (2002).

[21] С. Феферман, « Итеративные индуктивные теории фиксированной точки: применение гипотезы Хэнкока ». В Патрасском симпозиуме по логике , Исследования по логике и основам математики, том. 109 (1982).

[22] С. Феферман, Т. Страм, « Развертывание нефинитистской арифметики », Анналы чистой и прикладной логики, том. 104, №1--3 (2000), стр.75--96.

[FJ83-23] С. Феферман, Г. Ягер, «Принципы выбора, правило бара и автономно повторяющиеся схемы понимания в анализе», Journal of Символическая логика, том. 48, нет. (1983), стр. 63-70.

[BJS16-24] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час У. Бухгольц, Г. Йегер, Т. Страм, « Теории теоретико-доказательной силы ». $\psi (\Gamma _{\Omega +1})$ В книге « Концепции доказательства в математике, философии и информатике» (2016), под ред. Д. Пробста, П. Шустера. DOI 10.1515/9781501502620-007.

[25] Т. Страм, « Автономные прогрессии с фиксированной запятой и трансфинитная рекурсия с фиксированной запятой » (2000). В коллоквиуме по логике '98 , под ред. С.Р. Бусс, П. Гаек и П. Пудлак. DOI 10.1017/9781316756140.031

[26] Г. Ягер, Т. Страм, «Теории фиксированной точки и зависимый выбор». Архив математической логики, том. 39 (2000), стр. 493–508.

[Strahm2000-27] Jump up to: Перейти обратно: ^а ^б ^с Т. Страм, «Автономные прогрессии с фиксированной запятой и трансфинитная рекурсия с фиксированной запятой» (2000)

[Ruede2002-28] Jump up to: Перейти обратно: ^а ^б ^с ^д К. Рюде, « Трансфинитно-зависимый выбор и отражение ω-модели ». Журнал символической логики, том. 67, нет. 3 (2002).

[Ruede2003-29] Jump up to: Перейти обратно: ^а ^б ^с К. Рюде, " Теоретико-доказательный анализ Σ ¹₁ трансфинитно-зависимый выбор ». Анналы чистой и прикладной логики, том 122 (2003).

[StrahmMahlo2002-30] Jump up to: Перейти обратно: ^а ^б ^с ^д Т. Страм, « Упорядоченные доказательства для метапредикативного Мало ». Журнал символической логики, том. 67, нет. 1 (2002)

[31] Ф. Ранци, Т. Страм, «Гибкая система типов для малого порядкового номера Веблена» (2019). Архив математической логики 58: 711–751.

[32] К. Фудзимото, "Заметки о некоторых системах повторных индуктивных определений второго порядка и $\Pi _{1}^{1}$ -понимания и соответствующие подсистемы теории множеств». Анналы чистой и прикладной логики, т. 166 (2015), стр. 409--463.

[RathjenKrombholz2019-33] Jump up to: Перейти обратно: ^а ^б ^с Кромбхольц, Мартин; Ратьен, Майкл (2019). «Верхние оценки малой теоремы о графе». arXiv : 1907.00412 [ math.LO ].

[34] В. Бухгольц, С. Феферман, В. Полерс, В. Зиг, Повторные индуктивные определения и подсистемы анализа: недавние исследования теории доказательств

[35] В. Бухгольц, Теория доказательств импредикативных подсистем анализа (Исследования по теории доказательств, Монографии, Том 2 (1988)

[RathjenInvestigations-36] Jump up to: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н М. Ратьен, « Исследования подсистем арифметики второго порядка и теории множеств в силе между $\Pi _{1}^{1}{\mathsf {-CA}}$ и $\Delta _{2}^{1}{\mathsf {-CA+BI}}$ : Часть I ». По состоянию на 21 сентября 2023 г.

[37] М. Ратьен, « Сила некоторых теорий типа Мартина-Лёфа »

[Setzer96-38] Jump up to: Перейти обратно: ^а ^б А. Сетцер, « Модель теории типов со вселенной Мало » (1996).

[39] М. Ратьен, « Теория доказательства отражения ». Анналы чистой и прикладной логики, том. 68, вып. 2 (1994), стр. 181–224.

[Stegert10-40] Jump up to: Перейти обратно: ^а ^б Стегерт, Ян-Карл, « Порядковая теория доказательства теории множеств Крипке-Платека, дополненная принципами сильного отражения » (2010).

[Arai23A-41] Jump up to: Перейти обратно: ^а ^б ^с Арай, Тошиясу (01 апреля 2023 г.). «Лекции по порядковому анализу». arXiv : 2304.00246 [ math.LO ].

[Arai23B-42] Арай, Тосиясу (07 апреля 2023 г.). «Обоснованное доказательство $\Pi _{1}^{1}$ -отражение». arXiv : 2304.03851 [ math.LO ].

[Arai24-43] Jump up to: Перейти обратно: ^а ^б Арай, Тошиясу (12 февраля 2024 г.). «Обычный анализ $\Pi _{N}$ -Коллекция». arXiv : 2311.12459 [ math.LO ].

[44] Валентин Блот. « Прямая вычислительная интерпретация арифметики второго порядка посредством рекурсии обновления » (2022 г.).

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

[40]

[41]

[42]

[43]

[44]

История

Определение

Порядковые обозначения

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

Примеры

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

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

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

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

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

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

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