順序分析

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

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

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

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

このような理論の証明論的順序数は、理論が適切であることを証明できるすべての順序表記法（必然的に再帰的、次のセクションを参照）の順序タイプの上限、つまりが順序表記法であることを証明するKleene の意味での表記法が存在するすべての順序数の上限です。同様に、それは、および でそれを適切に順序付ける再帰的関係が(自然数の集合)上に存在し、が に対する算術ステートメントの超限帰納法を証明するようなすべての順序数の上限です。 ${\displaystyle T}$${\displaystyle \alpha}$${\displaystyle o}$${\displaystyle T}$${\displaystyle o}$${\displaystyle \alpha}$ ${\displaystyle R}$${\displaystyle \omega}$${\displaystyle \alpha}$${\displaystyle T}$${\displaystyle R}$

2 階算術のサブシステムなどの一部の理論には、超限順序数についての概念化や議論の方法がありません。たとえば、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 次形式。
• ウィキペディア^*
  ₀逆数学で時々使用される EFA の 2 次形式。

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

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

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

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

• ATR ₀、算術超限再帰。
• 任意の数の有限レベルの宇宙を持つMartin-Löf 型理論。

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

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

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

• ${\displaystyle \Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}}$, Π ₁ ^{1 の}内包には、かなり大きな証明論的順序数があり、これは Takeuti によって「順序数図」^{[5] p. 13で説明され、} Buchholz の表記法ではψ ₀ (Ω _ω )で制限されます。これは、有限反復帰納的定義の理論である の順序数でもあります。また、MLW、インデックス付き W 型を持つ Martin-Löf 型理論 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は、再帰的マーロ順序数に基づくクリプキ-プラテック集合論の拡張であり、非常に大きな証明論的順序数θを持ち、これはRathjen (1990)によって記述されました。
• TTM は、Martin-Löf 型理論を 1 つの Mahlo 宇宙で拡張したもので、証明論的順序数がさらに大きくなります。${\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 {安定性}}}$の証明論的順序数は に等しく、ここでは(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)}$

自然数のべき集合を記述できる理論のほとんどは、証明論的順序数が非常に大きいため、明示的な組み合わせ記述がまだ与えられていません。これには、、完全な2階算術( )、および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}}$指数関数が完全であることを主張する公理がなく、帰納法が Δ ₀述語に制限された算術です。
  • ${\displaystyle {\mathsf {EFA}}}$基本的な関数の算術です。
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$指数関数は、指数関数が完全であることを主張する公理によって拡張されたΔ _{0述語に制限された帰納法による算術です。}
  • ${\displaystyle {\mathsf {EFA}}^{\mathsf {n}}}$は、 Grzegorczyk 階層のn番目のレベルの各要素が完全であることを保証する公理によって拡張された基本的な関数の算術です。${\displaystyle {\mathcal {E}}^{n}}$
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {n+}}}$グジェゴルチク階層の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 {ATR}}_{0}}$算術超限再帰です。
  • ${\displaystyle {\mathsf {ATR}}}$完全な2次誘導スキームが追加されます。${\displaystyle {\mathsf {ATR}}_{0}}$
  • ${\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 が存在し、それが成り立つ」という公理を伴います。${\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 \omega }$

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

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

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

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

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

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

8. ^ は最初の到達不可能な基数を表します。Buchholz の ψ ではなく Jäger の ψ を使用します。 ${\displaystyle I}$

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

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

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

12. ^ は最初の弱コンパクト基数を表します。Buchholz の ψ ではなく Rathjen の Ψ を使用します。 ${\displaystyle K}$

13. ^ は最初の- 記述不可能な基数を表します。Buchholz の ψ ではなく Stegert の Ψ を使用します。 ${\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. ^ は最初のマーロ基数を表します。(おそらく) Rathjen の ψ を使用します。 ${\displaystyle M}$