反復帰納的定義の理論

集合論と論理学において、ブッフホルツの ID 階層は、一階算術のサブシステムの階層です。このシステム/理論は、「ν 回反復された帰納的定義の形式理論」と呼ばれます。ID _{ν は、}単調演算子の ν 回反復された最小不動点によって PA を拡張します。${\displaystyle ID_{\nu}}$

形式理論ID _ω（および一般にID _ν ）は、言語L _{IDで定式化された}ペアノ算術の拡張であり、次の公理によって表される：^[1]

• ${\displaystyle \forall y\forall x({\mathfrak {M}}_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})}$
• ${\displaystyle \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)
• ${\displaystyle \forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}}^{\mathfrak {M}})}$

ν ≠ ω の 理論 ID _{νは次のように定義されます。}

• ${\displaystyle \forall y\forall x(Z_{y}(P_{y}^{\mathfrak {M}},x)\rightarrow x\in P_{y}^{\mathfrak {M}})}$
• ${\displaystyle \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 < νに対して
• ${\displaystyle \forall y\forall x_{0}\forall x_{1}(P_{<y}^{\mathfrak {M}}x_{0}x_{1}\leftrightarrow x_{0}}^{\mathfrak {M}})}$

集合は、何らかの単調演算子 に対して が成り立つとき、帰納的に定義されているといいます。ここで はの最小不動点を表します。ID ₁の言語 は、一階数論の言語 に、X (新しい集合変数) と x (数値変数) のみを自由変数として含む L _N [X]のすべての X 正の式 A(X, x) に対して、集合 (または述語) 定数 I _{A を}追加することで得られます。X 正という用語は、X が A でのみ正に出現することを意味します (X が含意の左側にあることはありません)。集合論的な表記を少し許可します。 ${\displaystyle I\subseteq \mathbb {N} }$${\displaystyle \Gamma :P(N)\rightarrow P(N)}$${\displaystyle LFP(\Gamma )=I}$${\displaystyle LFP(f)}$${\displaystyle f}$${\displaystyle L_{ID_{1}}}$${\displaystyle L_{\mathbb {N} }}$

• ${\displaystyle F(x)=\{x\in N\mid F(x)\}}$
• ${\displaystyle s\in F}$手段${\displaystyle F(s)}$
• 2 つの式との場合、は を意味します。${\displaystyle F}$${\displaystyle G}$${\displaystyle F\subseteq G}$${\displaystyle \forall xF(x)\rightarrow G(x)}$

ID ₁には、次の公理に加えて、新しい言語に拡張された帰納法による一階数論 (PA) の公理が含まれます。

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

ここで、範囲はすべての数式にわたります。 ${\displaystyle F(x)}$${\displaystyle L_{ID_{1}}}$

 は算術的に定義可能な集合演算子 の下で閉じていることを表し、 は （少なくとも で定義可能な集合の中では） そのようなものが最も少ないことを 表すことに注意してください。${\displaystyle (ID_{1})^{1}}$${\displaystyle I_{A}}$${\displaystyle \Gamma _{A}(S)=\{x\in \mathbb {N} \mid \mathbb {N} \models A(S,x)\}}$${\displaystyle (ID_{1})^{2}}$${\displaystyle I_{A}}$${\displaystyle L_{ID_{1}}}$

したがって、 は 最小の事前固定点であり、したがって演算子 の最小の固定点であることを意味します。 ${\displaystyle I_{A}}$${\displaystyle \Gamma _{A}}$

ν 回反復される帰納的定義のシステムを定義するために、 ν は順序数であり、 を 順序型 ν の原始的な再帰的整列化とします。 の体の要素を表すためにギリシャ文字を使用します。 ID _νの言語は、最大で示されている自由変数を含むすべての X が正の式に対して、2 項述語定数 J _Aを追加することによってから取得されます。ここで、 X は単項 (集合) 変数であり、 Y は新しい 2 項述語変数です。の代わりに と書き、 x を後者の式で区別された変数と見なします。 ${\displaystyle \prec }$${\displaystyle \prec }$${\displaystyle L_{ID_{\nu }}}$${\displaystyle L_{\mathbb {N} }}$${\displaystyle L_{\mathbb {N} }[X,Y]}$${\displaystyle A(X,Y,\mu ,x)}$${\displaystyle x\in J_{A}^{\mu }}$${\displaystyle J_{A}(\mu ,x)}$

システムID _νは、新しい言語に帰納法スキームを拡張し、任意の 式 と公理 に沿った超限帰納法を表現する スキームを追加することで、第1階数論(PA)のシステムから取得されます。${\displaystyle (TI_{\nu }):TI(\prec ,F)}$${\displaystyle \prec }$${\displaystyle L_{ID_{\nu }}}$${\displaystyle F}$

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

ここで、 は 任意の 式です。 および では 、 式 の 省略形を使用しました。ここで、は特別な変数です。 これらは、 に対する各 が、演算子 に対する（定義可能な集合の中で）最小の不動点である ことを表していることがわかります。に対する以前のすべての集合 がパラメータとして使用されていることに注意してください。 ${\displaystyle F(x)}$${\displaystyle L_{ID_{\nu }}}$${\displaystyle (ID_{\nu })^{1}}$${\displaystyle (ID_{\nu })^{2}}$${\displaystyle A^{\mu }(F)}$${\displaystyle A(F,(\lambda \gamma y;\gamma \prec \mu \land y\in J_{A}^{\gamma }),\mu ,x)}$${\displaystyle x}$${\displaystyle J_{A}^{\mu }}$${\displaystyle \mu \prec \nu }$${\displaystyle \Gamma _{A}^{\mu }(S)=\{n\in \mathbb {N} |(\mathbb {N} ,(J_{A}^{\gamma })_{\gamma \prec \mu }\}}$${\displaystyle J_{A}^{\gamma }}$${\displaystyle \gamma \prec \mu }$

次に を定義します。 ${\textstyle ID_{\prec \nu }=\bigcup _{\xi \prec \nu }ID_{\xi }}$

${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$-は の弱められたバージョンです。 のシステムでは、何らかの単調演算子 に対して が の最小の不動点ではなく不動点である場合、集合 は帰納的に定義される と呼ばれます。 この微妙な違いにより、システムはと の間で大幅に弱くなります。 ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$${\displaystyle {\mathsf {ID}}_{\nu }}$${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$${\displaystyle I\subseteq \mathbb {N} }$${\displaystyle \Gamma :P(N)\rightarrow P(N)}$${\displaystyle I}$${\displaystyle \Gamma }$${\displaystyle PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})}$${\displaystyle PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})}$

${\displaystyle {\mathsf {ID}}_{\nu }\#}$はさらに弱くなります。 では、最小不動点ではなく不動点を使用するだけでなく、帰納法は正の式に対してのみ有効です。 この微妙な違いによって、システムはさらに弱くなります。であるのに対し、 です。 ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$${\displaystyle {\mathsf {ID}}_{\nu }\#}$${\displaystyle PTO({\mathsf {ID}}_{1}\#)=\psi (\Omega ^{\omega })}$${\displaystyle PTO({\widehat {\mathsf {ID}}}_{1})=\psi (\Omega ^{\varepsilon _{0}})}$

${\displaystyle {\mathsf {W-ID}}_{\nu }}$は、W 型に基づくのすべての変種の中で最も弱いものです。通常の反復帰納的定義と比較した弱化の量は、2 階算術の特定のサブシステムが与えられた場合にバー帰納法を削除することと同じです。、一方。 ${\displaystyle {\mathsf {ID}}_{\nu }}$${\displaystyle PTO({\mathsf {W-ID}}_{1})=\psi _{0}(\Omega \times \omega )}$${\displaystyle PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})}$

${\displaystyle {\mathsf {U(ID}}_{\nu }{\mathsf {)}}}$は、 の「展開」強化です。これは、厳密には 1 階の算術システムではありませんが、 ν 回反復された一般化された帰納的定義に基づく述語的推論によって得られるものを捉えています。強度の増加量は、 からへの増加と同じです。一方、 です。 ${\displaystyle {\mathsf {ID}}_{\nu }}$${\displaystyle \varepsilon _{0}}$${\displaystyle \Gamma _{0}}$${\displaystyle PTO({\mathsf {ID}}_{1})=\psi (\varepsilon _{\Omega +1})}$${\displaystyle PTO({\mathsf {U(ID}}_{1}{\mathsf {)}})=\psi (\Gamma _{\Omega +1})}$

• ν > 0とします。a ∈ T _{0に ν < μ の記号 D μ が}含まれていない場合、 "a ∈ W ₀ " は ID _νで証明可能です。
• ID _ωは に含まれます。${\displaystyle \Pi _{1}^{1}-CA+BI}$
• -文がID _νで証明可能であれば、となるものが存在する。${\displaystyle \Pi _{2}^{0}}$${\displaystyle \forall x\exists y\varphi (x,y)(\varphi \in \Sigma _{1}^{0})}$${\displaystyle p\in N}$${\displaystyle \forall n\geq p\exists k<H_{D_{0}D_{\nu }^{n}0}(1)\varphi (n,k)}$
• _{文Aがすべてのν<ωに対してIDν}で証明可能であれば、k∈Nが存在し、 となります。${\displaystyle \vdash _{k}^{D_{\nu }^{k}0}A^{N}}$

• _{ID <ν}の証明論的順序数は に等しい。${\displaystyle \psi _{0}(\Omega _{\nu })}$
• _{ID ν}の証明論的順序数は に等しい。${\displaystyle \psi _{0}(\varepsilon _{\Omega _{\nu }+1})=\psi _{0}(\Omega _{\nu +1})}$
• の証明論的順序数は に等しい。${\displaystyle {\widehat {ID}}_{<\omega }}$${\displaystyle \Gamma _{0}}$
• の証明理論的順序数はに等しい。${\displaystyle {\widehat {ID}}_{\nu }}$${\displaystyle \nu <\omega }$${\displaystyle \varphi (\varphi (\nu ,0),0)}$
• の証明論的順序数は に等しい。${\displaystyle {\widehat {ID}}_{\varphi (\alpha ,\beta )}}$${\displaystyle \varphi (1,0,\varphi (\alpha +1,\beta -1))}$
• の証明理論的順序数はに等しい。${\displaystyle {\widehat {ID}}_{<\varphi (0,\alpha )}}$${\displaystyle \alpha >1}$${\displaystyle \varphi (1,\alpha ,0)}$
• の証明理論的順序数はに等しい。${\displaystyle {\widehat {ID}}_{<\nu }}$${\displaystyle \nu \geq \varepsilon _{0}}$${\displaystyle \varphi (1,\nu ,0)}$
• の証明論的順序数は に等しい。${\displaystyle ID_{\nu }\#}$${\displaystyle \varphi (\omega ^{\nu },0)}$
• の証明論的順序数は に等しい。${\displaystyle ID_{<\nu }\#}$${\displaystyle \varphi (0,\omega ^{\nu +1})}$
• の証明論的順序数は に等しい。${\displaystyle W{\textrm {-}}ID_{\varphi (\alpha ,\beta )}}$${\displaystyle \psi _{0}(\Omega _{\varphi (\alpha ,\beta )}\times \varphi (\alpha +1,\beta -1))}$
• の証明論的順序数は に等しい。${\displaystyle W{\textrm {-}}ID_{<\varphi (\alpha ,\beta )}}$${\displaystyle \psi _{0}(\varphi (\alpha +1,\beta -1)^{\Omega _{\varphi (\alpha ,\beta -1)}+1})}$
• の証明論的順序数は に等しい。${\displaystyle U(ID_{\nu })}$${\displaystyle \psi _{0}(\varphi (\nu ,0,\Omega +1))}$
• の証明論的順序数は に等しい。${\displaystyle U(ID_{<\nu })}$${\displaystyle \psi _{0}(\Omega ^{\Omega +\varphi (\nu ,0,\Omega )})}$
• _{ID 1}の証明論的順序数(バッハマン-ハワード順序数) は、、、およびの証明論的順序数でもあります。${\displaystyle {\mathsf {KP}}}$${\displaystyle {\mathsf {KP\omega }}}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {ML_{1}V}}}$
• _{W-ID ω} ( )の証明理論的順序数はの証明理論的順序数でもある。${\displaystyle \psi _{0}(\Omega _{\omega }\varepsilon _{0})}$${\displaystyle {\mathsf {W-KPI}}}$
• _{ID ω}の証明論的順序数（Takeuti-Feferman-Buchholz 順序数）は、 、およびの証明論的順序数でもあります。${\displaystyle {\mathsf {KPI}}}$${\displaystyle \Pi _{1}^{1}-{\mathsf {CA}}+{\mathsf {BI}}}$${\displaystyle \Delta _{2}^{1}-{\mathsf {CA}}+{\mathsf {BI}}}$
• _{ID <ω^ω} ( )の証明論的順序数はの証明論的順序数でもある。${\displaystyle \psi _{0}(\Omega _{\omega ^{\omega }})}$${\displaystyle \Delta _{2}^{1}-{\mathsf {CR}}}$
• _{ID <ε0} ( )の証明論的順序数は、およびの証明論的順序数でもある。${\displaystyle \psi _{0}(\Omega _{\varepsilon _{0}})}$${\displaystyle \Delta _{2}^{1}-{\mathsf {CA}}}$${\displaystyle \Sigma _{2}^{1}-{\mathsf {AC}}}$

• Π 1 1 − C A + B I {\displaystyle \Pi _{1}^{1}-CA+BI}の独立性の結果
• 反復帰納的定義と分析のサブシステム：最近の証明理論的研究
• nLab における反復帰納的定義
• 反復帰納的定義の直観主義理論の補題
• 反復帰納的定義と Σ 2 1 − A C {\displaystyle \Sigma _{2}^{1}-AC}
• Agda における大きな可算順序数と数
• nLab における順序分析