Теории повторных индуктивных определений

В теории множеств логике иерархия и идентификаторов Бухгольца представляет собой иерархию подсистем арифметики первого порядка . Системы/теории $ID_{\nu }$ называются «формальными теориями ν-кратно повторенных индуктивных определений». ID _ν расширяет PA посредством ν итерированных наименьших неподвижных точек монотонных операторов.

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

Исходное определение [ править ]

Формальная теория ID _ω (и ID _ν в целом) является расширением арифметики Пеано , сформулированной на языке L _ID , посредством следующих аксиом: ^[1]

$\forall y\forall x({\mathfrak {M}}_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})$
$\forall y(\forall x({\mathfrak {M}}_{y}(F,x)\rightarrow F(x))\rightarrow \forall x(x\in P_{y}^{\mathfrak {M}}\rightarrow F(x)))$ для каждой L _ID -формулы F(x)
$\forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}<y\land x_{1}\in P_{x_{0}}^{\mathfrak {M}})$

Теория ID _ν с ν ≠ ω определяется как:

$\forall y\forall x(Z_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})$
$\forall x({\mathfrak {M}}_{u}(F,x)\rightarrow F(x))\rightarrow \forall x(P_{u}^{\mathfrak {M}}x\rightarrow F(x))$ для любой L _ID -формулы F(x) и каждого u < ν
$\forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}<y\land x_{1}\in P_{x_{0}}^{\mathfrak {M}})$

Объяснение/альтернативное определение [ править ]

ID ₁ [ править ]

Набор $I\subseteq \mathbb {N}$ называется индуктивно определенным, если для некоторого монотонного оператора $\Gamma :P(N)\rightarrow P(N)$ , $LFP(\Gamma )=I$ , где $LFP(f)$ обозначает наименее неподвижную точку $f$ . Язык ID ₁ , $L_{ID_{1}}$ , получается из теории чисел первого порядка, $L_{\mathbb {N} }$ , путем добавления константы множества (или предиката) I _A для каждой X-положительной формулы A(X, x) в L _N [X], которая содержит только X (новую переменную множества) и x (числовую переменную) как свободные переменные. Термин X-положительный означает, что X встречается только положительно в A (X никогда не находится слева от импликации). Позволим себе немного теоретико-множественных обозначений:

$F(x)=\{x\in N\mid F(x)\}$
$s\in F$ означает $F(s)$
Для двух формул $F$ и $G$ , $F\subseteq G$ означает $\forall xF(x)\rightarrow G(x)$ .

Тогда ID ₁ содержит аксиомы теории чисел первого порядка (ПА) с схемой индукции, распространенной на новый язык, а также следующие аксиомы:

$(ID_{1})^{1}:A(I_{A})\subseteq I_{A}$
$(ID_{1})^{2}:A(F)\subseteq F\rightarrow I_{A}\subseteq F$

Где $F(x)$ колеблется по всем $L_{ID_{1}}$ формулы.

Обратите внимание, что $(ID_{1})^{1}$ выражает это $I_{A}$ замкнуто относительно арифметически определимого оператора множества $\Gamma _{A}(S)=\{x\in \mathbb {N} \mid \mathbb {N} \models A(S,x)\}$ , пока $(ID_{1})^{2}$ выражает это $I_{A}$ является наименьшим из таких (по крайней мере, среди множеств, определяемых в $L_{ID_{1}}$ ).

Таким образом, $I_{A}$ подразумевается наименьшая предфиксированная точка и, следовательно, наименьшая фиксированная точка оператора $\Gamma _{A}$ .

ID _ν [ править ]

Чтобы определить систему индуктивных определений, повторенных ν раз, где ν — ординал, положим $\prec$ — примитивно-рекурсивное упорядочение типа порядка ν. Мы используем греческие буквы для обозначения элементов области $\prec$ . Язык ID _ν , $L_{ID_{\nu }}$ получается из $L_{\mathbb {N} }$ добавлением бинарной константы предиката J _A для каждого X-положительного $L_{\mathbb {N} }[X,Y]$ формула $A(X,Y,\mu ,x)$ который содержит не более показанных свободных переменных, где X снова является унарной (множественной) переменной, а Y — новой двоичной переменной-предикатом. Мы пишем $x\in J_{A}^{\mu }$ вместо $J_{A}(\mu ,x)$ , считая x выделенной переменной в последней формуле.

Идентификатор системы _ν теперь получается из системы теории чисел первого порядка (ПА) путем расширения схемы индукции на новый язык и добавления схемы $(TI_{\nu }):TI(\prec ,F)$ выражая трансфинитную индукцию вдоль $\prec$ для произвольного $L_{ID_{\nu }}$ формула $F$ а также аксиомы:

$(ID_{\nu })^{1}:\forall \mu \prec \nu ;A^{\mu }(J_{A}^{\mu })\subseteq J_{A}^{\mu }$
$(ID_{\nu })^{2}:\forall \mu \prec \nu ;A^{\mu }(F)\subseteq F\rightarrow J_{A}^{\mu }\subseteq F$

где $F(x)$ является произвольным $L_{ID_{\nu }}$ формула. В $(ID_{\nu })^{1}$ и $(ID_{\nu })^{2}$ мы использовали аббревиатуру $A^{\mu }(F)$ для формулы $A(F,(\lambda \gamma y;\gamma \prec \mu \land y\in J_{A}^{\gamma }),\mu ,x)$ , где $x$ — отличительная переменная. Мы видим, что они выражают то, что каждый $J_{A}^{\mu }$ , для $\mu \prec \nu$ , является наименее неподвижной точкой (среди определимых множеств) для оператора $\Gamma _{A}^{\mu }(S)=\{n\in \mathbb {N} |(\mathbb {N} ,(J_{A}^{\gamma })_{\gamma \prec \mu }\}$ . Обратите внимание, как все предыдущие наборы $J_{A}^{\gamma }$ , для $\gamma \prec \mu$ , используются в качестве параметров.

Затем мы определяем ${\textstyle ID_{\prec \nu }=\bigcup _{\xi \prec \nu }ID_{\xi }}$ .

Варианты [ править ]

${\widehat {\mathsf {ID}}}_{\nu }$ - ${\widehat {\mathsf {ID}}}_{\nu }$ представляет собой ослабленную версию ${\mathsf {ID}}_{\nu }$ . В системе ${\widehat {\mathsf {ID}}}_{\nu }$ , набор $I\subseteq \mathbb {N}$ вместо этого называется индуктивно определенным, если для некоторого монотонного оператора $\Gamma :P(N)\rightarrow P(N)$ , $I$ является фиксированной точкой $\Gamma$ , а не наименее фиксированная точка. Эта тонкая разница делает систему значительно слабее: $PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})$ , пока $PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})$ .

${\mathsf {ID}}_{\nu }\#$ является ${\widehat {\mathsf {ID}}}_{\nu }$ ослаб еще больше. В ${\mathsf {ID}}_{\nu }\#$ , он не только использует фиксированные точки, а не наименьшие фиксированные точки, и имеет индукцию только для положительных формул. Это еще раз тонкое различие делает систему еще слабее: $PTO({\mathsf {ID}}_{1}\#)=\psi (\Omega ^{\omega })$ , пока $PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})$ .

${\mathsf {W-ID}}_{\nu }$ самый слабый из всех вариантов ${\mathsf {ID}}_{\nu }$ , на основе W-типов. Величина ослабления по сравнению с обычными итеративными индуктивными определениями идентична удалению барной индукции при наличии определенной подсистемы арифметики второго порядка . $PTO({\mathsf {W-ID}}_{1})=\psi _{0}(\Omega \times \omega )$ , пока $PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})$ .

${\mathsf {U(ID}}_{\nu }{\mathsf {)}}$ представляет собой «разворачивающееся» усиление ${\mathsf {ID}}_{\nu }$ . Это не совсем арифметическая система первого порядка, но она отражает то, что можно получить с помощью предикативных рассуждений, основанных на ν-кратно повторенных обобщенных индуктивных определениях. Величина прироста силы идентична приросту от $\varepsilon _{0}$ к $\Gamma _{0}$ : $PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})$ , пока $PTO({\mathsf {U(ID}}_{1}{\mathsf {)}})=\psi (\Gamma _{\Omega +1})$ .

Результаты [ править ]

Пусть ν > 0. Если a ∈ T ₀ не содержит символа D _µ с ν < µ, то «a ∈ W ₀ » доказуемо в ID _ν .
ID _ω содержится в $\Pi _{1}^{1}-CA+BI$ .
Если $\Pi _{2}^{0}$ -предложение $\forall x\exists y\varphi (x,y)(\varphi \in \Sigma _{1}^{0})$ доказуемо в ID _ν , то существует $p\in N$ такой, что $\forall n\geq p\exists k<H_{D_{0}D_{\nu }^{n}0}(1)\varphi (n,k)$ .
Если предложение A доказуемо в ID _ν для всех ν < ω, то существует k ∈ N такой, что $\vdash _{k}^{D_{\nu }^{k}0}A^{N}$ .

Теоретико-доказательные ординалы [ править ]

Теоретико-доказательный ординал ID _<ν равен $\psi _{0}(\Omega _{\nu })$ .
Теоретико-доказательный ординал ID _ν равен $\psi _{0}(\varepsilon _{\Omega _{\nu }+1})=\psi _{0}(\Omega _{\nu +1})$ .
Теоретико-доказательный ординал ${\widehat {ID}}_{<\omega }$ равно $\Gamma _{0}$ .
Теоретико-доказательный ординал ${\widehat {ID}}_{\nu }$ для $\nu <\omega$ равно $\varphi (\varphi (\nu ,0),0)$ .
Теоретико-доказательный ординал ${\widehat {ID}}_{\varphi (\alpha ,\beta )}$ равно $\varphi (1,0,\varphi (\alpha +1,\beta -1))$ .
Теоретико-доказательный ординал ${\widehat {ID}}_{<\varphi (0,\alpha )}$ для $\alpha >1$ равно $\varphi (1,\alpha ,0)$ .
Теоретико-доказательный ординал ${\widehat {ID}}_{<\nu }$ для $\nu \geq \varepsilon _{0}$ равно $\varphi (1,\nu ,0)$ .
Теоретико-доказательный ординал $ID_{\nu }\#$ равно $\varphi (\omega ^{\nu },0)$ .
Теоретико-доказательный ординал $ID_{<\nu }\#$ равно $\varphi (0,\omega ^{\nu +1})$ .
Теоретико-доказательный ординал $W{\textrm {-}}ID_{\varphi (\alpha ,\beta )}$ равно $\psi _{0}(\Omega _{\varphi (\alpha ,\beta )}\times \varphi (\alpha +1,\beta -1))$ .
Теоретико-доказательный ординал $W{\textrm {-}}ID_{<\varphi (\alpha ,\beta )}$ равно $\psi _{0}(\varphi (\alpha +1,\beta -1)^{\Omega _{\varphi (\alpha ,\beta -1)}+1})$ .
Теоретико-доказательный ординал $U(ID_{\nu })$ равно $\psi _{0}(\varphi (\nu ,0,\Omega +1))$ .
Теоретико-доказательный ординал $U(ID_{<\nu })$ равно $\psi _{0}(\Omega ^{\Omega +\varphi (\nu ,0,\Omega )})$ .
Теоретико-доказательный ординал ID ₁ ( ординал Бахмана-Говарда ) также является теоретико-доказательным ординалом ${\mathsf {KP}}$ , ${\mathsf {KP\omega }}$ , ${\mathsf {CZF}}$ и ${\mathsf {ML_{1}V}}$ .
Теоретико-доказательный ординал W-ID _ω ( $\psi _{0}(\Omega _{\omega }\varepsilon _{0})$ ) также является теоретико-доказательным ординалом ${\mathsf {W-KPI}}$ .
Теоретико-доказательный ординал ID _ω ( порядковый номер Такеути-Фефермана-Бухгольца ) также является теоретико-доказательным ординалом ${\mathsf {KPI}}$ , $\Pi _{1}^{1}-{\mathsf {CA}}+{\mathsf {BI}}$ и $\Delta _{2}^{1}-{\mathsf {CA}}+{\mathsf {BI}}$ .
Теоретико-доказательный ординал ID _<ω^ω ( $\psi _{0}(\Omega _{\omega ^{\omega }})$ ) также является теоретико-доказательным ординалом $\Delta _{2}^{1}-{\mathsf {CR}}$ .
Теоретико-доказательный ординал ID _<ε0 ( $\psi _{0}(\Omega _{\varepsilon _{0}})$ ) также является теоретико-доказательным ординалом $\Delta _{2}^{1}-{\mathsf {CA}}$ и $\Sigma _{2}^{1}-{\mathsf {AC}}$ .