順序分析

2階算術のサブシステム（Z ₂ ）のような一部の理論には、超限順序数に関する概念化や議論の方法がありません。たとえば、サブシステムにとってそれが何を意味するのかを形式化するには${\displaystyle T}$Z ₂の「証明する」${\displaystyle \alpha }$整然とした」という表現の代わりに、順序表記法を構築します。${\displaystyle (A,{\tilde {<}})}$注文タイプ付き${\displaystyle \alpha }$。${\displaystyle T}$さまざまな超限帰納法の原理と連携して作業できるようになりました${\displaystyle (A,{\tilde {<}})}$これは、集合論的な順序数についての推論に代わるものです。

しかし、中には予想外に扱いにくい病的な記法体系も存在する。例えば、ラトジェンは原始的な再帰記法体系を提示している。${\displaystyle (\mathbb {N} ,<_{T})}$PAが一貫している場合に限り、それは妥当である。^{[ 2 ] p.3順序} タイプを持っているにもかかわらず${\displaystyle \omega }$. PA の順序分析にそのような表記を含めると、誤った等式が生じる。${\displaystyle {\mathsf {PTO(PA)}}=\omega }$。

• Q、ロビンソン算術（ただし、このような弱い理論の証明論的順序数の定義は微調整する必要がある）。
• PA ^– 、離散的に順序付けられた環の非負部分の一次理論。

• RFA、初等関数演算。^{[ 3 ]}
• IΔ ₀ 、指数演算が全演算であることを主張する公理を一切含まない、Δ _{0述語に関する帰納法を用いた算術。}

• EFAとは、初等関数演算のことです。
• IΔ ₀ + exp、指数演算が全演算であることを主張する公理によって拡張された、 Δ _{0述語に関する帰納法を用いた算術。}
• RCA ^* _{0 は}、逆算で使われることもある EFA の 2 次形式です。
• WKL ^* _{0 は}、逆算で使われることもある EFA の 2 次形式です。

フリードマンの大予想は、多くの「通常の」数学が、これを証明論的順序数とする弱い体系で証明できることを示唆している。

• IΔ _{0または、} n番目のレベルの各要素が$\displaystyle {\mathcal {E}}^{n}}$グジェゴルチクの階層は完全です。

• RCA ₀、再帰内包表記。
• WKL ₀、弱いケーニッヒの補題。
• PRA、原始再帰的算術。
• IΣ ₁、Σ ₁述語に対する帰納法を用いた算術。

• PA、ペアノ算術（ゲンツェンがカット消去法を用いて示したもの）。
• ACA ₀、算術理解。

• ATR ₀、算術的超限再帰。
• 任意に多数の有限レベル宇宙を持つマルティン＝レーフ型理論。

この順序数は、「述語的」理論の上限とみなされることがある。

• ID _{1 、}帰納的定義の最初の理論。
• KP、無限公理を持つクリプキ・プラテック集合論。
• CZF、アツェルの構成的ツェルメロ・フレンケル集合論。
• EONは、 Fefermanの明示的な数学システムT ₀の弱い変種です。

クリプキ＝プラテック集合論（CZF集合論）は、すべての部分集合の集合として与えられる完全な冪集合に関する公理を持たない弱い集合論である。その代わりに、これらの理論は、制限された分離と新しい集合の形成に関する公理を持つか、あるいは、より大きな関係から切り出すのではなく、特定の関数空間（べき乗）の存在を認める傾向がある。

• $\displaystyle \Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}}$Π ₁ ¹内包表記は、かなり大きな証明論的順序数を持っており、これは竹内によって「順序図」^{[ 5 ] p.  13で説明され、}ブッフホルツの記法ではψ ₀ ( Ω _ω )で制限されています。これはまた、有限回反復帰納的定義の理論である ID _ωの順序数でもあります。また、インデックス付き W 型を持つ Martin-Löf 型理論である MLW の順序数でもあります(Setzer (2004) )。
• ID _{ω は}、ω 反復帰納的定義の理論である。その証明論的順序数は、竹内-フェファーマン-ブッフホルツ順序数に等しい。
• T ₀、フェファーマンの明示的数学の構成的システムは、より大きな証明論的順序数を持ち、それは KPi、反復許容値を持つクリプキ-プラテック集合論の証明論的順序数でもあります。$\displaystyle \Sigma _{2}^{1}{\mbox{-}}{\mathsf {AC}}+{\mathsf {BI}}}$。
• KPiは、再帰的にアクセス不可能な順序数に基づくクリプキ・プラテック集合論の拡張であり、非常に大きな証明論的順序数を持つ。${\displaystyle \psi (\varepsilon _{I+1})}$1983年のJägerとPohlersの論文で説明されているように、Iは最小の到達不可能な数である。^{[ 6 ]}この順序数は、証明論的順序数でもある。${\displaystyle \Delta _{2}^{1}{\mbox{-}}{\mathsf {CA}}+{\mathsf {BI}}}$。
• KPMは、再帰的マロー順序数に基づくクリプキ・プラテック集合論の拡張であり、ラトジェン（1990）によって記述された非常に大きな証明論的順序数θを持つ。
• マルティン・レーフ型理論をマロー宇宙一つ分拡張したTTMは、さらに大きな証明論的順序数を持つ。${\displaystyle \psi _{\Omega _{1}}(\Omega _{M+\omega })}$。
• ${\displaystyle {\mathsf {KP}}+\Pi _{3}-Ref}$証明論的順序数を持つ${\displaystyle \Psi (\varepsilon _{K+1})}$、 どこ${\displaystyle K}$（Rathjen 1993）によれば、最初の弱コンパクトを指す。
• ${\displaystyle {\mathsf {KP}}+\Pi _{\omega }-Ref}$証明論的順序数を持つ${\displaystyle \Psi _{X}^{\varepsilon _{\Xi +1}}}$、 どこ${\displaystyle \Xi }$最初のものを指します$\displaystyle \Pi _{0}^{2}}$言葉では言い表せないほど${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)}$（Stegert 2010による）。
• $\displaystyle {\mathsf {安定性}}}$証明論的順序数を持つ${\displaystyle \Psi _{\mathbb {X} }^{\varepsilon _{\Upsilon +1}}}$どこ${\displaystyle \Upsilon }$は最小順序数の基数類似物である${\displaystyle \alpha }$それは${\displaystyle (\alpha +\beta )}$-すべての人にとって安定${\displaystyle \beta <\alpha }$ そして${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)}$（Stegert 2010による）。

自然数の冪集合を記述できるほとんどの理論は、証明論的順序数が非常に大きいため、明示的な組み合わせ論的記述がまだ与えられていない。これには以下が含まれる。${\displaystyle \Pi _{2}^{1}-CA_{0}}$、完全な2次演算（${\displaystyle \Pi _{\infty }^{1}-CA_{0}}$）およびZFやZFCを含む冪集合を持つ集合論。^{[ 7 ]}直観主義ZF（IZF）の強さはZFの強さに等しい。

この表で使用されている記号の一覧は以下のとおりです。

• ψは、それぞれの引用文献で定義されている様々な順序縮約関数を表す。
• Ψは、ラートジェンのプサイまたはステガートのプサイのいずれかを表します。
• φはヴェブレン関数を表す。
• ωは第一超限順序数を表す。
• ε _αはイプシロン数を表します。
• Γ _αはガンマ数を表します (Γ _0はフェフェルマン・シュッテ序数です)
• Ω _αは非可算順序数を表します (Ω ₁、略称 Ω はω ₁です)。順序数が証明論的であるとみなされるためには、可算性が必要であると考えられています。
• ${\displaystyle \mathbb {S} }$は安定した順序を表す順序項であり、${\displaystyle \mathbb {S} ^{+}}$最も許容されない序数${\displaystyle \mathbb {S} }$。
• ${\displaystyle \mathbb {I} _{N}}$は、次のような順序数を表す順序項である。${\displaystyle L_{\mathbb {I} _{N}}\models {\mathsf {KP}}\omega +\Pi _{N}-{\mathsf {Collection}}+(V=L)}$; N は、結果の順序分析の系列を定義する変数です。${\displaystyle \Pi _{N}-{\mathsf {Collection}}}$すべての人のために${\displaystyle 1\leq N<\omega }$N=1の場合、${\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{1}+1})=\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})}$
• その他の記号については、注釈を参照してください。

この表で使用されている略語の一覧は以下のとおりです。

• 1階算術
  • ${\displaystyle {\mathsf {Q}}}$ロビンソン算術は
  • ${\displaystyle {\mathsf {PA}}^{-}}$これは、離散的に順序付けられた環の非負部分に関する一次理論である。
  • ${\displaystyle {\mathsf {RFA}}}$これは基本的な関数演算です。
  • ${\displaystyle {\mathsf {I\Delta }}_{0}}$これは、指数演算が全演算であることを主張する公理を持たず、 Δ ₀述語に限定された帰納法を伴う算術です。
  • ${\displaystyle {\mathsf {EFA}}}$は初等関数算術です。
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$これは、指数演算が全演算であることを主張する公理によって拡張された、Δ _{0述語に限定された帰納法を伴う算術である。}
  • ${\displaystyle {\mathsf {EFA}}^{\mathsf {n}}}$は、 n番目のレベルの各要素が${\displaystyle {\mathcal {E}}^{n}}$グジェゴルチクの階層は完全です。
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {n+}}}$は${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$n番目のレベルの各要素が${\displaystyle {\mathcal {E}}^{n}}$グジェゴルチクの階層は完全です。
  • ${\displaystyle {\mathsf {PRA}}}$は原始的な再帰的算術です。
  • ${\displaystyle {\mathsf {I\Sigma }}_{1}}$_{これは、Σ 1}述語に限定された帰納法を用いた算術です。
  • ${\displaystyle {\mathsf {PA}}}$ペアノ算術です。
  • ${\displaystyle {\mathsf {ID}}_{\nu }\#}$は${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$ただし、帰納法は正の公式にのみ適用されます。
  • ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$PAは、単調作用素のν個の反復不動点によって拡張されます。
  • ${\displaystyle {\mathsf {U(PA)}}}$これは厳密には一階算術体系ではないが、自然数に基づいた述語推論によって得られるものを捉えている。
  • ${\displaystyle {\mathsf {Aut({\widehat {ID}})}}}$自律的に反復される${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$（言い換えれば、一度序数が定義されると、それを使って一連の新しい定義をインデックス付けすることができる。）
  • ${\displaystyle {\mathsf {ID}}_{\nu }}$PAは、単調作用素のν個の反復最小不動点によって拡張されます。
  • ${\displaystyle {\mathsf {U(ID}}_{\nu }{\mathsf {)}}}$これは厳密には一階算術体系ではないが、ν回反復された一般化された帰納的定義に基づく述語推論によって得られるものを捉えている。
  • ${\displaystyle {\mathsf {Aut(U(ID))}}}$自律的に反復される${\displaystyle {\mathsf {U(ID}}_{\nu }{\mathsf {)}}}$。
  • ${\displaystyle {\mathsf {W-ID}}_{\nu }}$弱体化したバージョンです${\displaystyle {\mathsf {ID}}_{\nu }}$W型に基づいています。
  • ${\displaystyle {\mathsf {TI}}[\Pi _{0}^{1-},\alpha ]}$長さ α が以下である超限誘導${\displaystyle \Pi _{0}^{1}}$これは、1階算術で使用される順序表記の表現です。
• 2次演算

一般に、添え字0は、帰納法のスキームが単一の集合帰納公理に限定されていることを意味する。

• • ${\displaystyle {\mathsf {RCA}}_{0}^{*}}$は、${\displaystyle {\mathsf {EFA}}}$逆算で使われることもある。
  • ${\displaystyle {\mathsf {WKL}}_{0}^{*}}$は、${\displaystyle {\mathsf {EFA}}}$逆算で用いられることもある。
  • ${\displaystyle {\mathsf {RCA}}_{0}}$再帰内包表記です。
  • ${\displaystyle {\mathsf {WKL}}_{0}}$これは弱いケーニッヒの補題である。
  • ${\displaystyle {\mathsf {ACA}}_{0}}$算術的理解です。
  • ${\displaystyle {\mathsf {ACA}}}$は${\displaystyle {\mathsf {ACA}}_{0}}$さらに、完全な二次誘導スキームも含まれる。
  • ${\displaystyle {\mathsf {TJ}}(n,X,Y)}$これは「 Xのn番目のチューリングジャンプはYである」という述語です。
  • ${\displaystyle {\mathsf {ATR}}_{0}}$算術的超限再帰です。
  • ${\displaystyle {\mathsf {ATR}}}$は${\displaystyle {\mathsf {ATR}}_{0}}$さらに、完全な二次誘導スキームも含まれる。
  • ${\displaystyle {\mathsf {BI}}}$これは棒状帰納法の公理である。
  • ${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}}$は${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}}$さらに「すべての真実${\displaystyle {\mathsf {\Pi }}_{3}^{1}}$-パラメータを持つ文は、（可算コード化された）${\displaystyle \beta }$-モデル${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}}$「。
• クリプキ・プラテック集合論
  • ${\displaystyle {\mathsf {KP}}}$これは、無限公理を持つクリプキ＝プラテック集合論である。
  • ${\displaystyle {\mathsf {KP\omega }}}$はクリプキ・プラテック集合論であり、その宇宙は許容集合であり、${\displaystyle \omega }$。
  • ${\displaystyle {\mathsf {W-KPI}}}$弱体化したバージョンです${\displaystyle {\mathsf {KPI}}}$W型に基づいています。
  • ${\displaystyle {\mathsf {KPI}}}$宇宙は許容集合の極限であると主張する。
  • ${\displaystyle {\mathsf {W-KPi}}}$弱体化したバージョンです${\displaystyle {\mathsf {KPi}}}$W型に基づいています。
  • ${\displaystyle {\mathsf {KPi}}}$宇宙は到達不可能な集合であると主張する。
  • ${\displaystyle {\mathsf {KPh}}}$宇宙は超到達不可能であると主張する。到達不可能な集合と、到達不可能な集合の極限である。
  • ${\displaystyle {\mathsf {KPM}}}$宇宙はマロー集合であると主張する。
  • ${\displaystyle {\mathsf {KP+\Pi }}_{\mathsf {n}}-{\mathsf {Ref}}}$は${\displaystyle {\mathsf {KP}}}$ある特定の一次反射スキームによって拡張される。
  • ${\displaystyle {\mathsf {Stability}}}$KPiは公理によって拡張されるか${\displaystyle \forall \alpha \exists \kappa \geq \alpha (L_{\kappa }\preceq _{1}L_{\kappa +\alpha })}$。
  • ${\displaystyle {\mathsf {KPM}}^{+}}$KPIは「少なくとも1つの再帰的マロ順序数が存在する」という主張によって拡張されます。
  • ${\displaystyle {\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)}$は${\displaystyle {\mathsf {KP}}\omega }$「空でない推移的な集合Mが存在し、${\displaystyle M\prec _{\Sigma _{1}}V}$'。

上付き文字のゼロは、${\displaystyle \in }$帰納法が取り除かれる（理論が著しく弱くなる）。

• 型理論
  • ${\displaystyle {\mathsf {CPRC}}}$これは、原始再帰的構成のヘルベリン＝ペイティ計算です。
  • ${\displaystyle {\mathsf {ML}}_{\mathsf {n}}}$W型を除いた型理論と${\displaystyle n}$宇宙。
  • ${\displaystyle {\mathsf {ML}}_{<\omega }}$これは、W型を含まず、有限個の宇宙を持つ型理論である。
  • ${\displaystyle {\mathsf {MLU}}}$これは、次の宇宙演算子を持つ型理論です。
  • ${\displaystyle {\mathsf {MLS}}}$これは、W型を含まず、超宇宙を持つ型理論である。
  • ${\displaystyle {\mathsf {Aut(ML)}}}$これは、W型を用いず、自律的に反復される宇宙を持つ型理論である。
  • ${\displaystyle {\mathsf {ML}}_{1}{\mathsf {V}}}$これは、1つの宇宙とアツェルの反復集合の型を持つ型理論です。
  • ${\displaystyle {\mathsf {MLW}}}$これは、インデックス付きW型を用いた型理論です。
  • ${\displaystyle {\mathsf {ML}}_{1}{\mathsf {W}}}$これは、W型と1つの宇宙を持つ型理論です。
  • ${\displaystyle {\mathsf {ML}}_{<\omega }{\mathsf {W}}}$これは、W型と有限個の宇宙を持つ型理論です。
  • ${\displaystyle {\mathsf {Aut(MLW)}}}$これは、W型と自律的に反復される宇宙を持つ型理論です。
  • ${\displaystyle {\mathsf {TTM}}}$これは、マロ宇宙論に基づく型理論である。
  • ${\displaystyle \lambda 2}$システムFは、多相ラムダ計算または二階ラムダ計算とも呼ばれます。
• 構成的集合論
  • ${\displaystyle {\mathsf {CZF}}}$これはアツェルの構成的集合論である。
  • ${\displaystyle {\mathsf {CZF+REA}}}$は${\displaystyle {\mathsf {CZF}}}$さらに、通常の拡張公理も加える。
  • ${\displaystyle {\mathsf {CZF+REA+FZ}}_{2}}$は${\displaystyle {\mathsf {CZF+REA}}}$さらに、完全な二次誘導スキームも含まれる。
  • ${\displaystyle {\mathsf {CZFM}}}$は${\displaystyle {\mathsf {CZF}}}$マロの世界観で。
• 明示的な数学
  • ${\displaystyle {\mathsf {EM}}_{0}}$基本的な明示的数学と初歩的な理解
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+JR}}}$は${\displaystyle {\mathsf {EM}}_{0}}$プラス結合ルール
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J}}}$は${\displaystyle {\mathsf {EM}}_{0}}$さらに公理を結合する
  • ${\displaystyle {\mathsf {EON}}}$フェファーマンの弱い変種です${\displaystyle {\mathsf {T}}_{0}}$。
  • ${\displaystyle {\mathsf {T}}_{0}}$は${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG}}}$、 どこ${\displaystyle {\mathsf {IG}}}$誘導発生です。
  • ${\displaystyle {\mathsf {T}}}$は${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG+FZ}}_{2}}$、 どこ${\displaystyle {\mathsf {FZ}}_{2}}$これは完全な2次誘導スキームである。