順序分析

証明理論において、順序分析は数学理論の強さを測る尺度として、それらの理論に順序数（多くの場合、大きな可算順序数）を割り当てます。理論が同じ証明理論的順序数を持つ場合、それらはしばしば等矛盾であり、ある理論の証明理論的順序数が他の理論よりも大きい場合、それはしばしば後者の理論の無矛盾性を証明できます。

理論の証明論的順序数を得ることに加えて、実際には順序分析は、分析対象の理論に関するさまざまな他の情報ももたらします。たとえば、理論の証明可能再帰的、超算術的、または関数のクラスの特性評価などです。^[1]${\displaystyle \Delta _{2}^{1}}$

歴史

順序解析の分野は、1934年にゲルハルト・ゲンツェンがカット消去法を用いて、ペアノ算術の証明論的順序数がε ₀であることを現代的な言葉で証明したときに形成されました。ゲンツェンの無矛盾性証明を参照してください。

意味

順序分析は、順序表記についての記述を行うために算術の十分な部分を解釈できる、真で有効な（再帰的な）理論に関係します。

このような理論の証明論的順序数は、理論が十分に基礎づけられていることを証明できるすべての順序記法（必然的に再帰的、次のセクションを参照）の順序型の上限、つまり、 が順序記法であることを証明するクリーネの意味での記法が存在するようなすべての順序数の上限です。同様に、 は、が順序数と十分に順序づけられる（自然数の集合）上の再帰関係が存在し、が に対する算術的ステートメントの超限帰納法を証明するようなすべての順序数の上限です。 ${\displaystyle T}$ ${\displaystyle \alpha }$ ${\displaystyle o}$ ${\displaystyle T}$ ${\displaystyle o}$ ${\displaystyle \alpha }$ ${\displaystyle R}$ ${\displaystyle \omega }$ ${\displaystyle \alpha }$ ${\displaystyle T}$ ${\displaystyle R}$

序数表記

二階算術の部分系（Z ₂ ）のような一部の理論では、超限順序数について概念化や議論を行う手段が存在しない。例えば、Z ₂の部分系が「整列性を証明する」とはどういうことかを形式化するために、代わりに順序型 を持つ順序記法を構築する。これにより、 に沿った様々な超限帰納法原理を利用でき、集合論的順序数に関する推論の代替となる。 ${\displaystyle T}$ ${\displaystyle \alpha }$ ${\displaystyle (A,{\tilde {<}})}$ ${\displaystyle \alpha }$ ${\displaystyle T}$ ${\displaystyle (A,{\tilde {<}})}$

しかしながら、予想外に扱いが難しい病的な記法体系も存在します。例えば、Rathjenは、順序型 を持つにもかかわらず、PA が整合的である場合に限り整基数となる原始的な再帰記法体系を提示しています^{[2] p. 3。}このような記法をPA の順序解析に含めると、誤った等式 が導かれます。 ${\displaystyle (\mathbb {N} ,<_{T})}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {PTO(PA)}}=\omega }$

上限

順序記法は再帰的でなければならないため、あらゆる理論の証明論的順序数はチャーチ・クリーネ順序 数 以下となる。特に、矛盾する理論の証明論的順序数は となる。なぜなら、矛盾する理論は、すべての順序記法が整基礎であることを自明に証明するからである。 ${\displaystyle \omega _{1}^{\mathrm {CK} }}$ ${\displaystyle \omega _{1}^{\mathrm {CK} }}$

-公理化可能かつ-健全な理論において、その理論が整列していることを証明できない再帰的順序付けの存在は境界定理から導かれ、そして、証明可能に整列している順序表記は、実際には-健全性によって整列している。したがって、公理化可能な-健全な理論の証明論的順序数は常に（可算な）再帰的順序数、すなわち より真に小さいとなる。^{[2]定理2.21}${\displaystyle \Sigma _{1}^{1}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle \Sigma _{1}^{1}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle \Sigma _{1}^{1}}$ ${\displaystyle \omega _{1}^{\mathrm {CK} }}$

例

証明論的順序数ωを持つ理論

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

証明論的順序数ωを持つ理論²

• RFA、初等関数演算。^[3]
• IΔ ₀、指数演算が完全であることを主張する公理のない Δ ₀述語に基づく帰納法による算術。

証明論的順序数ωを持つ理論³

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

フリードマンの壮大な予想は、これを証明論的順序数として持つ弱いシステムで多くの「通常の」数学が証明できることを示唆しています。

証明論的順序数ωを持つ理論ⁿ（のためにn= 2, 3, ... ω)

• IΔ _0またはGrzegorczyk 階層のn番目のレベルの各要素が合計であることを保証する公理によって拡張された EFA 。${\displaystyle {\mathcal {E}}^{n}}$

証明論的順序数ωを持つ理論^ω

• RCA ₀、再帰的理解。
• WKL ₀、弱いケーニッヒの補題。
• PRA、原始再帰演算。
• IΣ ₁、 Σ ₁述語に基づく帰納法による算術。

証明論的順序数 ε を持つ理論₀

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

証明論的順序数を持つ理論Feferman–Schütte 序数 Γ ₀

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

この順序数は、「述語的」理論の上限であると考えられる場合もあります。

証明論的順序数を持つ理論バッハマン・ハワード順序数

• ID _{1 、}帰納的定義の最初の理論。
• KP、無限公理を持つクリプキ・プラテック集合論。
• CZF、Aczel の構成的 Zermelo–Fraenkel 集合論。
• EON は、 Fefermanの明示的数学システム T ₀の弱い変種です。

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

より大きな証明理論的順序数を持つ理論

数学における未解決問題

完全な二階算術の証明論的順序数は何ですか？^[4]

数学におけるさらなる未解決問題

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

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

順序分析表

鍵

この表で使用されている記号のリストは次のとおりです。

• ψ は、それぞれの引用文献で定義されているさまざまな順序崩壊関数を表します。
• Ψ は Rathjen の Psi または Stegert の Psi のいずれかを表します。
• φはヴェブレンの関数を表します。
• ω は最初の超限順序数を表します。
• ε _αはイプシロン数を表します。
• Γ _αはガンマ数を表します (Γ _0はフェフェルマン・シュッテ序数です)
• Ω _{α は}非可算順序数（Ω ₁、略して Ω はω ₁）を表す。順序数が証明理論的であるとみなされるためには、可算性が必要であると考えられている。
• ${\displaystyle \mathbb {S} }$ は安定した順序数を表す順序数項であり、を超える最小の順序数です。${\displaystyle \mathbb {S} ^{+}}$ ${\displaystyle \mathbb {S} }$
• ${\displaystyle \mathbb {I} _{N}}$ は、 となる順序数を表す順序項である。Nは、 forallの結果の一連の順序数分析を定義する変数である。N=1のとき、${\displaystyle L_{\mathbb {I} _{N}}\models {\mathsf {KP}}\omega +\Pi _{N}-{\mathsf {Collection}}+(V=L)}$ ${\displaystyle \Pi _{N}-{\mathsf {Collection}}}$ ${\displaystyle 1\leq N<\omega }$ ${\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{1}+1})=\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})}$
• 追加の記号は注記に記載されています。

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

• 一次演算
  • ${\displaystyle {\mathsf {Q}}}$ ロビンソン算術
  • ${\displaystyle {\mathsf {PA}}^{-}}$ 離散順序付けされた環の非負部分に関する第一階理論である。
  • ${\displaystyle {\mathsf {RFA}}}$ 基本的な関数演算です。
  • ${\displaystyle {\mathsf {I\Delta }}_{0}}$ 指数関数が完全であることを主張する公理がなく、Δ _{0述語に制限された帰納法による算術です。}
  • ${\displaystyle {\mathsf {EFA}}}$ は初等関数の算術です。
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$ は、指数関数が完全であることを主張する公理によって拡張されたΔ ₀述語に制限された帰納法による算術です。
  • ${\displaystyle {\mathsf {EFA}}^{\mathsf {n}}}$ は、 Grzegorczyk 階層のn番目のレベルの各要素が完全であることを保証する公理によって拡張された基本関数算術です。${\displaystyle {\mathcal {E}}^{n}}$
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {n+}}}$ は、Grzegorczyk 階層のn番目のレベルの各要素が完全であることを保証する公理によって拡張されます。${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$ ${\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 }}$ W型をベースにした弱体化版です。${\displaystyle {\mathsf {ID}}_{\nu }}$
  • ${\displaystyle {\mathsf {TI}}[\Pi _{0}^{1-},\alpha ]}$ は長さ α が -式以下の超限帰納法である。これは、一階算術において用いられる順序記法の表現となる。${\displaystyle \Pi _{0}^{1}}$
• 2階算術

一般に、下付き文字 0 は、誘導スキームが単一の誘導公理に制限されていることを意味します。

• • ${\displaystyle {\mathsf {RCA}}_{0}^{*}}$ は逆数学で時々使用されるの 2 次形式です。${\displaystyle {\mathsf {EFA}}}$
  • ${\displaystyle {\mathsf {WKL}}_{0}^{*}}$ 逆数学で時々使用されるの 2 次形式です。${\displaystyle {\mathsf {EFA}}}$
  • ${\displaystyle {\mathsf {RCA}}_{0}}$ 再帰的理解です。
  • ${\displaystyle {\mathsf {WKL}}_{0}}$ は弱いケーニヒの補題である。
  • ${\displaystyle {\mathsf {ACA}}_{0}}$ 算数の理解です。
  • ${\displaystyle {\mathsf {ACA}}}$ 完全な 2 次誘導スキームをプラスしたものです。${\displaystyle {\mathsf {ACA}}_{0}}$
  • ${\displaystyle {\mathsf {TJ}}(n,X,Y)}$ は「 Xのn番目のチューリングジャンプはYである」という述語です。
  • ${\displaystyle {\mathsf {ATR}}_{0}}$ 算術超限再帰です。
  • ${\displaystyle {\mathsf {ATR}}}$ 完全な 2 次誘導スキームをプラスしたものです。${\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}}}$ W型をベースにした弱体化版です。${\displaystyle {\mathsf {KPI}}}$
  • ${\displaystyle {\mathsf {KPI}}}$ 宇宙は許容される集合の限界であると主張する。
  • ${\displaystyle {\mathsf {W-KPi}}}$ W型をベースにした弱体化版です。${\displaystyle {\mathsf {KPi}}}$
  • ${\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}}^{+}}$ 「少なくとも 1 つの再帰的な Mahlo 順序数が存在する」というアサーションによって拡張された KPI です。
  • ${\displaystyle {\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)}$ は、「空でない推移的な集合 M が存在し、そのような集合 M が存在する」という公理を伴います。${\displaystyle {\mathsf {KP}}\omega }$ ${\displaystyle M\prec _{\Sigma _{1}}V}$

上付きのゼロは、-induction が削除されたことを示します (理論が大幅に弱くなります)。 ${\displaystyle \in }$

• 型理論
  • ${\displaystyle {\mathsf {CPRC}}}$ 原始再帰構造の Herbelin-Patey 計算です。
  • ${\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 つの宇宙と Aczel 型の反復集合を持つ型理論です。
  • ${\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}}}$ これは、Mahlo 宇宙を持つ型理論です。
  • ${\displaystyle \lambda 2}$ System Fは、多態的ラムダ計算または 2 階ラムダ計算とも呼ばれます。
• 構成的集合論
  • ${\displaystyle {\mathsf {CZF}}}$ アチェルの構成的集合論です。
  • ${\displaystyle {\mathsf {CZF+REA}}}$ は正規拡張公理を加算したものです。${\displaystyle {\mathsf {CZF}}}$
  • ${\displaystyle {\mathsf {CZF+REA+FZ}}_{2}}$ 完全な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}}}$ は、Fefermanの弱い変種です。${\displaystyle {\mathsf {T}}_{0}}$
  • ${\displaystyle {\mathsf {T}}_{0}}$ は、ここでは誘導生成です。${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG}}}$ ${\displaystyle {\mathsf {IG}}}$
  • ${\displaystyle {\mathsf {T}}}$ は であり、は完全な 2 次誘導スキームです。${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG+FZ}}_{2}}$ ${\displaystyle {\mathsf {FZ}}_{2}}$

参照

• 等一貫性
• 大きな基数特性
• フェファーマン・シュッテ順序数
• バッハマン・ハワード順序数
• 複雑度クラス
• ゲンツェンの一貫性証明

注記

1. ^のために${\displaystyle 1<n\leq {\mathsf {\omega }}}$

2. ^可算無限反復最小不動点を持つヴェブレン関数。 ^{[説明が必要]}${\displaystyle \varphi }$

3. ^一般的にはMadore の ψ のように表記されることもあります。${\displaystyle \psi (\varepsilon _{\Omega +1})}$

4. ^ Buchholz の ψ ではなく Madore の ψ を使用します。

5. ^ Madore の ψ のように表記されることもあります。${\displaystyle \psi (\varepsilon _{\Omega _{\omega }+1})}$

6. ^は最初の再帰的に弱コンパクト順序数を表す。Buchholz の ψ ではなく Arai の ψ を用いる。 ${\displaystyle K}$

7. ^の証明理論的順序数も、W型によって与えられる弱化の量が十分ではないためである。${\displaystyle {\mathsf {Aut(W-ID)}}}$

8. ^ は最初の到達不可能な基数を表します。ブッフホルツの ψ ではなく、イェーガーの ψ を使用します。 ${\displaystyle I}$

9. ^ は- 到達不可能基数の極限を表す。（おそらく）Jäger の ψ を用いる。 ${\displaystyle L}$ ${\displaystyle \omega }$

10. ^ は- 到達不可能基数の極限を表す。（おそらく）Jäger の ψ を用いる。 ${\displaystyle L^{*}}$ ${\displaystyle \Omega }$

11. ^ はマーロ基数の最初の数を表す。ブッフホルツの ψ ではなく、ラトジェンの ψ を用いる。 ${\displaystyle M}$

12. ^は最初の弱コンパクト基数を表す。ブッフホルツの ψ ではなく、ラトジェンの Ψ を用いる。 ${\displaystyle K}$

13. ^ は最初の- 記述不可能な基数を表す。ブッフホルツの ψ ではなく、ステゲルトの Ψ を用いる。 ${\displaystyle \Xi }$ ${\displaystyle \Pi _{0}^{2}}$

14. ^は、 'が-記述不可能'である最小のものである。また、 'が-記述不可能' である最小のものである。Buchholz の ψ ではなく Stegert の Ψ を使用する。 ${\displaystyle Y}$ ${\displaystyle \alpha }$ ${\displaystyle \forall \theta <Y\exists \kappa <Y(}$ ${\displaystyle \kappa }$ ${\displaystyle \theta }$ ${\displaystyle \forall \theta <Y\forall \kappa <Y(}$ ${\displaystyle \kappa }$ ${\displaystyle \theta }$ ${\displaystyle \rightarrow \theta <\kappa }$

15. ^はマーロ基数の最初の数を表す。（おそらく）ラトジェンのψを用いる。 ${\displaystyle M}$

引用

1. M. Rathjen, "Admissible Proof Theory and Beyond". Studies in Logic and the Foundations of Mathematics vol. 134 (1995), pp.123--147.
2. Rathjen, The Realm of Ordinal Analysis. 2021年9月29日にアクセス。
3. Krajicek, Jan (1995). 有界算術、命題論理、計算量理論. ケンブリッジ大学出版局. pp. 18–20. ISBN 9780521452052。基本的な集合と基本的な関数を定義し、それらが自然数上のΔ _{0 -述語と同値であることを証明した。このシステムの順序解析は、} Rose, HE (1984). Subrecursion: Functions and hierarchies . University of Michigan: Clarendon Press. ISBN 978-4-855-2555-2555 を参照のこと。 9780198531890。
4. M. Rathjen, 証明理論：算術から集合論へ（p.28）。2022年8月14日にアクセス。
5. Rathjen, Michael (2006), "The art of ordinal analysis" (PDF) , International Congress of Mathematicians , vol. II, Zürich: Eur. Math. Soc., pp.  45– 69, MR 2275588, 2009年12月22日時点 のオリジナル(PDF)からアーカイブ、2024年5月3日取得
6. D. Madore、A Zoo of Ordinals (2017、p.2)。 2022 年 8 月 12 日にアクセス。
7. J. Avigad、R. Sommer、「順序分析へのモデル理論的アプローチ」（1997年）。
8. M. Rathjen、W. Carnielli、「Hydrae と算術サブシステム」（1991）
9. ジェロン・ファン・デル・メーレン;ラジーン、マイケル。ワイアーマン、アンドレアス (2014)。 「ハワード・バックマン階層の秩序理論的特徴付け」。arXiv : 1411.4481 [math.LO]。
10. G. Jäger, T. Strahm, "Second order theory with ordinals and elementary comprehension". Archive for Mathematical Logic vol. 34 (1995).
11. HM Friedman, SG Simpson, RL Smith, "Countable algebra and set existence axioms". Annals of Pure and Applied Logic vol. 25, iss. 2 (1983).
12. 「Subsystems of Second-Order Arithmetic」（2009年）の定理IX.4.4に従う。
13. G. Jäger, "The Strength of Admissibility Without Foundation". Journal of Symbolic Logic vol. 49, no. 3 (1984).
14. B. Afshari, M. Rathjen, 「順序分析と無限ラムゼー定理」. Lecture Notes in Computer Science vol. 7318 (2012)
15. Marcone, Alberto; Montalbán, Antonio (2011). 「計算可能性理論家のためのヴェブレン関数」. The Journal of Symbolic Logic . 76 (2): 575– 602. arXiv : 0910.5442 . doi :10.2178/jsl/1305810765. S2CID  675632.
16. S. Feferman, 「数学的実践に関連する有限型理論」『数理論理学ハンドブック』 、J. Barwise編『論理学と数学の基礎研究』第90巻（1977年）、ノースホランド出版。
17. と」（2001）の理論${\displaystyle \varphi 20}$ ${\displaystyle \varphi 2\varepsilon _{0}}$
18. D. Probst、「2階算術のメタ述語サブシステムのモジュラー順序分析」（2017）
19. F. Ranzi, 「柔軟な型システムからメタ述語的ウェル順序証明へ」 ベルン大学博士論文、2015年。
20. A. Cantini、「第2階算術における選択原理と理解原理の関係について」、Journal of Symbolic Logic vol. 51 (1986)、360-373ページ。
21. Fischer, Martin; Nicolai, Carlo; Pablo Dopico Fernandez (2020). 「非古典的真理と古典的強度。HYPE上の構成的真理の証明理論的分析」arXiv : 2007.07188 [math.LO].
22. SG Simpson, "Friedman's Research on Subsystems of Second Order Arithmetic". Harvey Friedman's Research on the Foundations of Mathematics , Studies in Logic and the Foundations of Mathematics vol. 117 (1985), ed. L. Harrington, M. Morley, A. Šcedrov, SG Simpson, pub. North-Holland.
23. J. Avigad, 「順序記法の再帰を用いた許容集合論の順序解析」『Journal of Mathematical Logic』第2巻第1号、91-112頁（2002年）。
24. S. Feferman, 「反復帰納的不動点理論：ハンコック予想への応用」『Patras Logic Symposion』、論理学と数学の基礎研究第109巻（1982年）。
25. S. Feferman, T. Strahm、「非有限主義的算術の展開」、Annals of Pure and Applied Logic vol. 104, no.1--3 (2000), pp.75--96。
26. S. Feferman, G. Jäger、「分析における選択原理、バールール、自律反復理解スキーム」、Journal of Symbolic Logic vol. 48, no. (1983)、63-70ページ。
27. U. Buchholtz, G. Jäger, T. Strahm, "Theories of proof-theoretic strength ψ ( Γ Ω + 1 ) {\displaystyle \psi (\Gamma _{\Omega +1})} ".数学、哲学、コンピュータサイエンスにおける証明の概念(2016)、D. Probst、P. Schuster編。DOI 10.1515/9781501502620-007。
28. T. Strahm, 「自律的固定点進行と固定点超限再帰」（2000年）. Logic Colloquium '98 , 編. SR Buss, P. Hájek, P. Pudlák. DOI 10.1017/9781316756140.031
29. G. Jäger, T. Strahm, 「不動点理論と従属選択」. 数学論理アーカイブ第39巻 (2000年), pp.493--508.
30. T. Strahm、「自律不動点進行と不動点超限再帰」（2000年）
31. C. Rüede、「超限依存選択とω-モデル反射」。Journal of Symbolic Logic vol. 67, no. 3 (2002).
32. C. Rüede、「Σ11超限従属選択の証明理論的分析」。Annals of Pure and Applied Logic vol. 122 (2003)。
33. T. Strahm, "Metapredicateative Mahlo の Wellordering Proofs". Journal of Symbolic Logic vol. 67, no. 1 (2002)
34. F. Ranzi, T. Strahm, 「小さなヴェブレン順序数のための柔軟な型システム」（2019年）Archive for Mathematical Logic 58: 711–751.
35. K. Fujimoto, 「反復帰納的定義と内包表記のいくつかの二次体系と集合論の関連サブシステムに関するノート」Annals of Pure and Applied Logic, vol. 166 (2015), pp. 409--463.${\displaystyle \Pi _{1}^{1}}$
36. G. Jäger, T. Strahm, 「応用理論におけるスースリン作用素の証明理論的分析」『数学の基礎に関する考察：ソロモン・フェファーマンに捧ぐエッセイ集』（2002年）。
37. Krombholz, Martin; Rathjen, Michael (2019). 「グラフマイナー定理の上限」. arXiv : 1907.00412 [math.LO].
38. W. Buchholz、S. Feferman、W. Pohlers、W. Sieg、「反復帰納的定義と分析のサブシステム：最近の証明理論的研究」
39. W. Buchholz,非述語的解析サブシステムの証明理論 (証明理論研究、モノグラフ、第2巻(1988))
40. M. Rathjen, "Π 1 1 − C A {\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}} と Δ 2 1 − C A + B I {\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BI}}} 間の強度における2次演算と集合論のサブシステムの調査：パートI". 2023年12月7日アーカイブ。
41. M. Rathjen、「いくつかのMartin-Löf型理論の強さ」
42. 保守性の結果については、Rathjen (1996) 「The Recursively Mahlo Property in Second Order Arithmetic」（Math. Log. Quart.、42 : 59–66、doi :10.1002/malq.19960420106）を参照。同じ序数を与える${\displaystyle {\mathsf {KPM}}}$
43. A. Setzer、「Mahlo宇宙を持つ型理論のモデル」（1996年）。
44. M. Rathjen, "Proof Theory of Reflection". Annals of Pure and Applied Logic vol. 68, iss. 2 (1994), pp.181--224.
45. Stegert, Jan-Carl、「強い反射原理によって拡張されたクリプキ-プラテック集合論の順序証明理論」（2010年）。
46. 新井 敏康 (2023-04-01). 「順序解析講義」. arXiv : 2304.00246 [math.LO].
47. 新井 敏康 (2023-04-07). 「-reflection の well-foundedness 証明」. arXiv : 2304.03851 [math.LO].${\displaystyle \Pi _{1}^{1}}$
48. 新井 敏康 (2024-02-12). 「-Collection の順序分析」. arXiv : 2311.12459 [math.LO].${\displaystyle \Pi _{N}}$
49. Blot, Valentin (2022-08-02). 「更新再帰による2階算術の直接計算的解釈」.第37回ACM/IEEEコンピュータサイエンスにおける論理シンポジウム論文集. ACM. pp.  1– 11. doi :10.1145/3531130.3532458. ISBN 978-1-4503-9351-5。
50. Lubarsky, Robert (2015-10-02). 「CZFと2階算術」. arXiv : 1510.00469 [math.LO].

参考文献

• Buchholz, W.; Feferman, S.; Pohlers, W.; Sieg, W. (1981),反復帰納的定義と解析のサブシステム, Lecture Notes in Math., vol. 897, Berlin: Springer-Verlag, doi :10.1007/BFb0091894, ISBN 978-3-540-11170-2
• ポーラーズ、ウォルフラム（1989）、証明論、数学講義ノート、第1407巻、ベルリン：シュプリンガー・フェアラーク、doi：10.1007/978-3-540-46825-7、ISBN 3-540-51842-8、MR  1026933
• ポーラーズ、ウォルフラム（1998）「集合論と第二階数論」『証明論ハンドブック』 、論理学と数学の基礎研究、第137巻、アムステルダム：エルゼビア・サイエンスBV、pp.  210– 335、doi :10.1016/S0049-237X(98)80019-0、ISBN 0-444-89840-9、MR  1640328
• ラスジェン、マイケル (1990)、「弱マロ基数に基づく序数表記法」、Arch. Math. Logic、29 (4): 249– 263、doi :10.1007/BF01651328、MR  1062729、S2CID  14125063
• Rathjen, Michael (2006)、「順序解析の技法」（PDF）、国際数学者会議、第2巻、チューリッヒ：欧州数学協会、pp.  45– 69、MR  2275588、2009年12月22日時点のオリジナルよりアーカイブ
• Rose, HE (1984), 『部分再帰：関数と階層』、オックスフォード・ロジック・ガイド第9巻、オックスフォード、ニューヨーク：クラレンドン・プレス、オックスフォード大学出版局
• シュッテ、クルト (1977)、証明理論、Grundlehren der Mathematischen Wissenschaften、vol. 225、ベルリン-ニューヨーク: Springer-Verlag、pp. xii+299、ISBN 3-540-07911-4、MR  0505313
• Setzer、Anton (2004)、「Martin-Löf 型理論の証明理論。概要」、数学と科学、ヒューメイン。数学と社会科学( 165): 59–99
• 竹内, ガイシ (1987),証明理論, 論理学と数学の基礎研究, 第81巻 (第2版), アムステルダム: North-Holland Publishing Co., ISBN 0-444-87943-9、MR  0882549
• ラトジェン、マイケル（1994）「反射の証明理論」、純粋論理学と応用論理学年報、68（2）：181-224、doi：10.1016/0168-0072（94）90074-4
• ステガート、ヤン＝カール（2010）、強い反射原理によって強化されたクリプキ＝プラテック集合論の順序証明理論