查看“︁证明论序数”︁的源代码

'''证明论序数'''（或称证明论强度序数，Proof-Theoretic Ordinal）是衡量形式理论强度的核心工具，通过将理论映射到序数上，刻画其能证明的良序关系的复杂度。该概念源于希尔伯特的证明论计划，旨在通过有限方法证明数学基础理论的一致性，后由阿克曼（Wilhelm Ackermann）和根岑（Gerhard Gentzen）发展为序数分析技术。

=== 定义和性质 ===
序数是良序集的序型，满足超限归纳原理：<math>\forall\alpha(\forall\beta<\alpha(P(\beta)\Rightarrow P(\alpha))\Rightarrow\forall\alpha P(\alpha))</math>，其中 <math>P</math> 是任意性质。

对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（在 googology 语境中，可写为 <math>\text{PTO}(T)</math>）定义为满足以下条件的最小序数 <math>\alpha</math>：

# 存在一种自然表示序数 <math><\alpha</math> 的递归记号系统
# 通过超限归纳至 <math>\alpha</math>，可证明 <math>T</math> 的一致性（即 <math>T\nvdash\perp</math>）
# <math>T</math> 能证明所有初等递归函数在 <math><\alpha</math> 的序数上总停止

或者说，是理论 <math>T</math> 能用超限归纳证明的原始递归良序的序型最大值。

证明论序数满足：

# '''不可达性'''（Inaccessibility）：若 <math>|T|_\text{ord}=\alpha</math>，则 <math>T</math> 无法证明“存在序数 <math>\beta</math> 使得 <math>\beta=\alpha</math>”的良序性
# '''递归性'''（Recursivity）：证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序

=== 证明论序数表 ===
{| class="wikitable class="article-table" border="0" cellpadding="1" cellspacing="1""
! scope="col" |证明论序数
! scope="col" |算术论体系
! scope="col" |集合论体系
! scope="col" |其他体系
|-
| -
|<math>Q</math>
|<math>\rm KP^-</math>
|
|-
|<math>\omega^2</math>
|<math>\rm RFA</math><br><math>\rm I\Delta_0</math>
|
|
|-
|<math>\omega^3</math>
|<math>\rm RCA_0^*</math><br><math>\rm WKL_0^*</math><br><math>\rm I\Delta_0+exp</math>
|
|
|-
|<math>\omega^n</math>
|<math>{\rm I\Delta_0}+\mathcal{E}_n\text{ is total}</math>
|
|
|-
|<math>\omega^\omega</math>
|<math>\rm RCA_0</math><br><math>\rm WKL_0</math><br><math>\rm PRA</math><br><math>\rm RCA_0^2</math>
|<math>\rm CPRC</math><br><math>\rm KP^-+\Pi_1^{set}\ Fondation+IND</math>
|
|-
|<math>\omega^{\omega^{\omega^\omega}}</math>
|<math>\rm RCA_0+(\Pi_2^0)^--IND</math>
|
|
|-
|<math>\omega\uparrow\uparrow(n+2)</math>
|<math>{\rm I}\Sigma_{n+1}</math>
|
|
|-
|<math>\varepsilon_0</math>
|<math>\rm PA</math><br><math>\rm ACA_0</math><br><math>\rm \Delta_1^1-CA_0</math><br><math>\rm \Sigma_1^1-AC_0</math>
|<math>\rm KP^{-\infty}</math>
|<math>\rm EM_0</math>
|-
|<math>\varepsilon_1</math>
|<math>\rm ACA_0+KPHT</math>
|
|
|-
|<math>\varepsilon_\omega</math>
|<math>\rm ACA_0+iRT</math><br><math>{\rm RCA_0}+\forall Y\forall n\exists X({\rm TJ}(n,X,Y))</math>
|
|
|-
|<math>\varepsilon_{\varepsilon_0}</math>
|<math>\rm ACA</math><br><math>{\rm FP}_n-{\rm ACA'_0}</math><br><math>{\rm FP}_n-{\rm ACA'}</math>
|
|
|-
|<math>\zeta_0</math>
|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm ACA_0+(BR)</math><br><math>\rm p_1(ACA_0)</math>
|
|
|-
|<math>\varphi(2,\varepsilon_0)</math>
|<math>{\rm ACA}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm RFN</math>
|
|
|-
|<math>\varphi(\omega,0)</math>
|<math>\rm \Delta_1^1-CR</math><br><math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm \Sigma_1^1-DC_0</math>
|
|<math>\rm ID_1^\#</math><br><math>\rm EM_0+JR</math><br><math>\rm PID</math><br><math>\rm Acc-ID(Acc)</math><br><math>\rm (\Pi_0^0(P),P\cup N)-ID</math><br><math>\rm (\Pi_0^0(P),P\land N)-ID(Acc)</math>
|-
|<math>\varphi(\nu+1,0)</math>
|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega^\nu,X,Y))</math>
|
|
|-
|<math>\psi(\Omega^{\varepsilon_0})</math>
|<math>\rm \Delta_1^1-CA</math><br><math>\rm \Sigma_1^1-AC</math><br><math>\rm{(\Pi_1^0-CA)}_{<\varepsilon_0}</math>
|
|
|-
|<math>\psi(\Omega^{\psi(\Omega^\omega)})</math>
|
|<math>\rm PRS\ \omega</math>
|
|-
|<math>\Gamma_0</math>
|<math>\rm ATR_0</math><br><math>\rm \Delta_1^1-CA+BR</math><br><math>\rm RCA_0+\Sigma_1^0-RT</math><br><math>\rm RCA_0+\Delta_1^0-RT</math><br><math>\rm RCA_0+\Sigma_1^0-det.</math><br><math>\rm RCA_0+\Delta_1^0-det.</math><br><math>\rm FP_0</math>
|<math>\rm KPi^-</math><br><math>\rm CZF^-+INAC</math>
|<math>\widehat{\rm ID}_{<\omega}</math><br><math>\widehat{\rm ID}^*</math><br><math>{\rm ML}_{<\omega}</math><br><math>\rm MLU</math><br><math>\rm U(PA)</math>
|-
|<math>\varphi(1,0,\omega^\omega)</math>
|
|<math>\rm KPl_0+(\Sigma_1-I_\omega)</math>
|
|-
|<math>\varphi(1,0,\varepsilon_0)</math>
|<math>\rm ATR</math>
|
|<math>\widehat{\rm ID}_\omega</math>
|-
|<math>\psi(\Omega^{\Omega+1})</math>
|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ATR_0})</math>
|
|
|-
|<math>\psi(\Omega^{\Omega+\omega})</math>
|<math>\rm ATR_0+\Sigma_1^1-DC</math>
|
|<math>\widehat{\rm ID}_{<\omega^\omega}</math>
|-
|<math>\psi(\Omega^{\Omega+\varepsilon_0})</math>
|<math>\rm ATR+\Sigma_1^1-DC</math>
|
|<math>\widehat{\rm ID}_{<\varepsilon_0}</math>
|-
|<math>\psi(\Omega^{\Omega+\Gamma_0})</math>
|
|
|<math>\widehat{\rm ID}_{<\Gamma_0}</math><br><math>\rm MLS</math>
|-
|<math>\varphi(2,0,0)</math>
|<math>\rm FTR_0</math>
|<math>\rm KPh^-</math>
|<math>\rm Aut(\widehat{ID})</math>
|-
|<math>\varphi(2,0,\varepsilon_0)</math>
|<math>\rm FTR</math>
|
|
|-
|<math>\varphi(2,\varepsilon_0,0)</math>
|
|<math>\rm KPh^0+(F-I_\omega)</math>
|
|-
|<math>\psi(\Omega^{\Omega\omega})</math>
|
|<math>\rm KPM^-</math>
|
|-
|<math>\varphi(\varepsilon_0,0,0)</math>
|<math>\rm \Sigma_1^1-TDC</math>
|
|
|-
|<math>\varphi(1,0,0,0)</math>
|<math>\rm p_1(\Sigma_1^1-TDC_0)</math>
|
|
|-
|<math>\psi(\Omega^{\Omega^\omega})</math>
|<math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm p_3(ACA_0)</math>
|
|<math>\rm FIT</math><br><math>\rm TID</math>
|-
|<math>\vartheta(\Omega^\Omega)</math>
|<math>\rm p_1(p_3(ACA_0))</math>
|
|
|-
|<math>\theta_{(n+2)(\Omega^\omega)}0</math>
|<math>{\rm ACA_0}+\Pi_{n+2}^1-{\rm BI}</math><br><math>\Pi_{n+1}^1-{\rm RFN}</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0^-</math>
|<math>{\rm KP}\omega^-+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math>
|
|-
|<math>\theta_{(n+2)(\Omega^\omega)}0</math>
|<math>{\rm ACA}+\Pi_{n+2}^1-{\rm BI}</math><br><math>(\Pi_{n+2}^1-{\rm BI})^-</math>
|<math>{\rm KP}\omega^-+{\rm IND}+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math>
|
|-
|<math>\psi(\psi_1(0))</math>
|<math>\rm ACA+BI</math><br><math>\rm ACA_0+\Pi_1^1-CA^-</math><br><math>\rm \Pi_1^0-FXP_0</math>
|<math>\rm KP</math><br><math>\rm KP+\Pi_2^{set}-Reflection</math><br><math>\rm KP+(BI^*)</math><br><math>\rm KP+(ATR_0^*)</math><br><math>\rm CZF</math><br><math>{\rm KP}\omega_2\upharpoonright+\Delta_1-{\rm CA}+s\Pi_1^1-{\rm ref}</math>
|<math>\rm ID_1</math><br><math>\rm ID_1^2</math><br><math>\rm ML_1\ V</math>
|-
|<math>\psi(\Omega_2)</math>
|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ACA+BI})</math>
|
|
|-
|<math>\psi(\Omega_2^{\Omega_2})</math>
|<math>\rm ATR_0^\bullet</math><br><math>\rm FP_0^\bullet</math><br><math>\rm \Sigma_1^1-DC_0^\bullet+(SUB^\bullet)</math><br><math>\rm \Sigma_1^1-AC_0^\bullet+(SUB^\bullet)</math>
|
|<math>\widehat{\rm ID}_{<\omega}^\bullet</math><math>\mathcal{U}({\rm ID_1})</math>
|-
|<math>\psi(\psi_2(0))</math>
|
|<math>\rm KP+\exists\omega_1^{CK}</math>
|<math>\rm ID_2</math><br><math>\rm ID_2^2</math>
|-
|<math>\psi(\Omega_\omega)</math>
|<math>\rm \Pi_1^1-CA_0</math><br><math>\rm \Delta_2^1-CA_0</math><br><math>\rm RCA_0+\Sigma_1^0\land\Pi_1^0-det.</math><br><math>\rm RCA_0+\Delta_2^0-RT</math>
|<math>{\rm KPl}^r</math><br><math>{\rm KPi}^r</math><br><math>{\rm KP}\beta^r</math>
|<math>{\rm ID}_{<\omega}</math><br><math>({\rm ID}_{<\omega}^2)_0</math>
|-
|<math>\psi(\Omega_\omega\cdot\omega^\omega)</math>
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-IND</math>
|
|
|-
|<math>\psi(\Omega_\omega\cdot\varepsilon_0)</math>
|<math>\rm \Pi_1^1-CA</math>
|<math>\rm W-KPl</math>
|<math>\rm W-ID_\omega</math><br><math>\rm ID_{<\omega}^2</math>
|-
|<math>\psi(\Omega_\omega\cdot\Omega)</math>
|<math>\rm \Pi_1^1-CA+BR</math>
|
|
|-
|<math>\psi(\Omega_\omega^\omega)</math>
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI</math>
|
|
|-
|<math>\psi(\Omega_\omega^{\omega^\omega})</math>
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI+\Pi_3^1-IND</math>
|
|
|-
|<math>\psi(\psi_\omega(0))</math>
|<math>\rm \Pi_1^1-CA+BI</math>
|<math>\rm KPl</math>
|<math>\rm ID_\omega</math><br><math>\rm BID_\omega^2</math>
|-
|<math>\psi(\Omega_{\omega^\omega})</math>
|<math>\rm \Delta_2^1-CR</math><br><math>\rm (\Pi_1^1-CA_{<\omega^\omega})</math>
|<math>{\rm KPl}_{\omega^\omega}^r</math>
|<math>\rm ID_{<\omega^\omega}</math>
|-
|<math>\psi(\Omega_{\varepsilon_0})</math>
|<math>\rm \Delta_2^1-CA</math><br><math>\rm \Sigma_2^1-AC</math><br><math>\rm (\Pi_1^1-CA_{<\varepsilon_0})</math>
|<math>{\rm KPl}_{\varepsilon_0}^r</math><br><math>\rm W-KPi</math><br><math>{\rm W-KP}\beta</math>
|<math>\rm ID_{<\varepsilon_0}</math><br><math>\rm ID_{<\varepsilon_0}^2</math><br><math>\rm BID_{<\varepsilon_0}^2</math>
|-
|<math>\psi(\Omega_{\nu\cdot\omega})</math>
|<math>\rm (\Pi_1^1-CA_\nu^+)_0</math>
|<math>{\rm KPl}_{\nu+}^r</math>
|<math>\rm ID_{<\nu\cdot\omega}</math><br><math>\rm (PID_\nu^2)_0</math>
|-
|<math>\psi(\Omega_\gamma\cdot\omega)</math>
|<math>\rm (\Pi_1^1-CA_{\gamma-})_0</math>
|<math>{\rm KPl}_\gamma^r</math>
|<math>\rm (NUID_\gamma^2)_0</math>
|-
|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\varepsilon_0))</math>
|<math>\rm \Pi_1^1-CA_\nu^+</math>
|<math>\rm W-KPl_{\nu+}</math>
|<math>\rm W-ID_{\nu\cdot\omega}</math><br><math>\rm PID_\nu^2</math>
|-
|<math>\psi(\Omega_\gamma\cdot\varepsilon_0)</math>
|<math>\rm (\Pi_1^1-CA_\gamma)</math><br><math>\rm \Pi_1^1-CA_{\gamma-}</math>
|<math>\rm W-KPl_\gamma</math>
|<math>\rm W-ID_\gamma</math><br><math>\rm ID_\gamma^2</math><br><math>\rm NUID_\gamma^2</math>
|-
|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\Omega))</math>
|<math>\rm \Pi_1^1-CA_\nu^++BR</math>
|
|<math>\rm PID_\nu^2+BR</math>
|-
|<math>\psi(\Omega_\gamma\cdot\Omega)</math>
|<math>\rm \Pi_1^1-CA_{\gamma-}+BR</math>
|
|<math>\rm NUID_\gamma^2+BR</math>
|-
|<math>\psi(\Omega_{\omega^\gamma})</math>
|<math>\rm (\Pi_1^1-CA_{\omega\gamma})_0</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})+BI</math>
|
|<math>\rm (ID_{\omega^\gamma}^2)_0</math><br><math>\rm ID_{<\omega^\gamma}</math><br><math>\rm BID_{<\omega^\gamma}^2</math><br><math>\rm (ID_{<\nu}^2)+BI</math>
|-
|<math>\psi(\psi_\nu(0))</math>
|<math>\rm (\Pi_1^1-CA_\nu)_0</math>
|<math>\rm KPl_\nu</math>
|<math>\rm ID_\nu</math><br><math>\rm (ID_\nu^2)_0</math>
|-
|<math>\psi(\psi_\nu(\varepsilon_0))</math>
|<math>\rm \Pi_1^1-CA_\nu</math>
|
|<math>\rm ID_\nu^2</math>
|-
|<math>\psi(\psi_\nu(\Omega))</math>
|<math>\rm \Pi_1^1-CA_\nu+BR</math>
|
|<math>\rm ID_\nu^2+BR</math>
|-
|<math>\psi(\psi_\nu(\psi_\nu(0)))</math>
|
|
|<math>\rm BID_\nu^2</math>
|-
|<math>\psi(\psi_{\nu+1}(0))</math>
|<math>\rm \Pi_1^1-CA_\nu+BI</math>
|<math>\rm KPl_{\nu+1}</math>
|<math>\rm ID_{\nu+1}</math><br><math>\rm ID_\nu^2+BI</math>
|-
|<math>\psi(\psi_{\nu\cdot\omega}(0))</math>
|<math>\rm \Pi_1^1-CA_\nu^++BI</math>
|<math>\rm KPl_{\nu+}</math>
|<math>\rm ID_{\nu\cdot\omega}</math><br><math>\rm PID_\nu^2+BI</math><br><math>\rm PBID_\nu^2</math>
|-
|<math>\psi(\psi_\gamma(0))</math>
|<math>\rm (\Pi_1^1-CA_\gamma)_0</math><br><math>\rm (\Pi_1^1-CA_\gamma)+BI</math><br><math>\rm \Pi_1^1-CA_{\gamma-}+BI</math>
|<math>\rm KPl_\gamma</math>
|<math>\rm ID_\gamma</math><br><math>\rm (ID_\gamma^2)_0</math><br><math>{\rm ID}_\gamma^i(\mathcal{O}){\rm BID}_\nu^2</math><br><math>\rm ID_\gamma^2+BI</math><br><math>\rm NUID_\gamma^2+BI</math>
|-
|<math>\psi(\psi_\Omega(0))</math>
|
|<math>\rm KPl^*</math><br><math>{\rm KPl}_\Omega^r</math>
|<math>\rm ID_{\prec*}</math><br><math>\rm BID^{2*}</math><br><math>\rm ID^{2*}+BI^2</math>
|-
|<math>\psi_{\Omega_1}(\psi_I(0))</math>
|<math>\rm \Pi_1^1-TR_0</math><br><math>\rm \Pi_1^1-TR_0+\Delta_2^1-CA_0</math><br><math>\rm \Delta_2^1-CA+BI(impl\ \Sigma_2^1)</math><br><math>\rm \Delta_2^1-CA+BR(impl\ \Sigma_2^1)</math><br><math>\rm RCA_0+\Delta_2^0-det.</math><br><math>\rm RCA_0+\Delta_1^1-RT</math>
|<math>{\rm Aut-KPl}^r</math><br><math>{\rm Aut-KPl}^r+{\rm KPi}^r</math><br><math>\rm KPi^\omega+FOUNDR(impl-\Sigma)</math><br><math>\rm KPi^\omega+FOUND(impl-\Sigma)</math>
|<math>{\rm Aut-ID}_0^{pos}</math><br><math>{\rm Aut-ID}_0^{mon}</math>
|-
|<math>\psi_{\Omega_1}(\psi_I(0)\cdot\varepsilon_0)</math>
|<math>\rm \Pi_1^1-TR</math>
|<math>\rm W-Aut-KPl</math>
|<math>{\rm Aut-ID}^{pos}</math><br><math>{\rm Aut-ID}^{mon}</math><br><math>\rm Aut-KPl^\omega</math>
|-
|<math>\psi_{\Omega_1}(\psi_{\Omega_{\psi_I(0)+1}}(0))</math>
|<math>\rm \Pi_1^1-TR+BI</math>
|<math>\rm Aut-KPl</math>
|<math>{\rm Aut-ID}_2^{pos}</math><br><math>{\rm Aut-ID}_2^{mon}</math><br><math>\rm Aut-BID</math>
|-
|<math>\psi_{\Omega_1}(\psi_I(I^\omega))</math>
|<math>\rm \Delta_2^1-TR_0</math><br><math>\rm \Sigma_2^1-TRDC_0</math><br><math>\rm \Delta_2^1-CA_0+\Sigma_2^1-BI</math>
|
|<math>{\rm KPi}^r+(\Sigma-{\rm FOUND})</math><br><math>{\rm KPi}^r+(\Sigma-{\rm REC})</math>
|-
|<math>\psi_{\Omega_1}(\psi_I(I^{\varepsilon_0}))</math>
|<math>\rm \Delta_2^1-TR</math><br><math>\rm \Sigma_2^1-TRDC</math><br><math>\rm \Delta_2^1-CA+\Sigma_2^1-BI</math>
|
|<math>\rm KPi^\omega+(\Sigma-FOUND)</math><br><math>\rm KPi^\omega+(\Sigma-REC)</math>
|-
|<math>\psi_{\Omega_1}(\varepsilon_{I+1})</math>
|<math>\rm \Delta_2^1-CA+BI</math><br><math>\rm \Sigma_2^1-AC+BI</math>
|<math>\rm KPi</math><br><math>{\rm KP}\beta</math><br><math>\rm CZF+REA</math>
|<math>\rm T_0</math>
|-
|<math>\psi_{\Omega_1}(\Omega_{I+\omega})</math>
|
|<math>\rm KPi^+</math>
|<math>\rm ML_1\ W</math><br><math>\rm KP_1\ W</math><br><math>\rm IARI</math>
|-
|<math>\psi_{\Omega_1}(\varepsilon_{M+1})</math>
|<math>\rm \Delta_2^1-CA+BI+(M)</math>
|<math>\rm KPM</math><br><math>\rm CZFM</math>
|
|-
|<math>\psi_{\Omega_1}(\Omega_{M+\omega})</math>
|
|<math>\rm KPM^+</math>
|<math>\rm MLM</math><br><math>\rm Agda</math>
|-
|<math>\Psi_{\Omega_1}^0(\varepsilon_{K+1})</math>
|<math>{\rm ACA+BI}+\Pi_4^1-\beta\text{-model-Reflection}</math>
|<math>{\rm KP}+\Pi_3^{\rm set}\text{-Reflection}</math>
|
|-
|<math>\Psi_\mathbb{X}^{\varepsilon_{\xi_n+1}}</math>
|<math>{\rm ACA+BI}+\Pi_{n+5}^1-\beta\text{-model-Reflection}</math>
|<math>{\rm KP}+\Pi_{n+4}^{\rm set}\text{-Reflection}</math>
|
|-
|<math>\Psi_\mathbb{X}^{\varepsilon_{\Xi+1}}</math>
|<math>{\rm ACA+BI}-\beta\text{-model-Reflection}</math>
|<math>{\rm KP}+\Pi_\omega^{\rm set}\text{-Reflection}</math>
|
|-
|<math>\Psi_\mathbb{H}^{\varepsilon_{\Upsilon+1}}</math>
|
|<math>{\rm KPi}+\forall\alpha\exists\kappa(L_\kappa\prec_1L_{\kappa+\alpha})</math>
|
|-
|<math>\psi(\Omega_{\mathbb{S}+\omega})</math>
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-CA^-</math>
|<math>{\rm KPl}^r+\exists M(\text{Trans}(M)\land M\prec_1 V)</math>
|
|-
|<math>\Psi_\mathbb{K}^{\varepsilon_{I+1}}</math>
|<math>\rm \Delta_2^1-CA+BI+\Pi_2^1-CA^-</math>
|<math>{\rm KPi}+\exists M(\text{Trans}(M)\land M\prec_1 V)</math>
|
|-
|<math>\mathcal{I}_\omega\cap\omega_1^{\rm CK}</math>
|<math>\rm \Pi_2^1-CA_0</math><br><math>\rm \Delta_3^1-CA_0</math>
|
|
|-
|<math>\mathcal{I}_{\omega+1}\cap\omega_1^{\rm CK}</math>
|<math>\rm \Pi_2^1-CA+BI</math>
|<math>\rm KP+\Sigma_1^{set}-Separation</math><br><math>{\rm KPi}+\forall\alpha\exists\beta(\beta>\alpha)(\beta\text{ stable})</math>
|
|-
|<math>\mathcal{I}_{\varepsilon_0}\cap\omega_1^{\rm CK}</math>
|<math>\rm \Delta_3^1-CA</math><br><math>\rm \Sigma_3^1-AC</math>
|
|
|-
|<math>\text{maybe }\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math>
|<math>\rm \Delta_3^1-CA+BI</math><br><math>\rm \Sigma_3^1-AC+BI</math><br><math>\rm \Sigma_3^1-DC+BI</math>
|<math>{\rm KP}+\Delta_2^{\rm set}\text{-Separation}</math>
|
|-
|<math>\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math>
|
|<math>{\rm KP}+\Pi_1^{\rm set}\text{-Collection}</math>
|
|-
|
|<math>\Pi_{n+3}^1{\rm-CA+BI}</math>
|<math>{\rm KP}+\Sigma_{n+2}^{\rm set}\text{-Separation}</math>
|
|-
|
|<math>\Pi_{n+3}^1{\rm-CA}+\Sigma_{n+3}^1{\rm-AC+BI}</math>
|<math>{\rm KP^-}+\Sigma_{n+2}^{\rm set}\text{-Separation}+\Sigma_{n+2}^{\rm set}\text{-Collection}</math>
|
|-
|
|<math>\rm Z_2=\Pi_\infty^1-CA</math><br><math>\rm \Delta_1^2-CA_0</math><br><math>\rm Z_2+\Sigma_\infty^1-AC</math>
|<math>{\rm KP}+\Sigma_\omega^{\rm set}\text{-Separation}</math><br><math>{\rm KP^-}+\Sigma_\omega^{\rm set}\text{-Separation}+\Sigma_\omega^{\rm set}\text{-Collection}</math><br><math>\rm ZFC^-=ZFC-Powerset</math>
|
|-
|
|<math>{\rm Z}_{n+3}=\Pi_\infty^{n+2}{\rm-CA}</math><br><math>\Delta_1^{n+3}{\rm-CA_0}</math>
|<math>{\rm ZFC^-+V=L+}\exists\omega_{n+1}</math>
|
|-
|
|<math>\rm Z_\infty=\Pi_0^\infty-CA</math>
|<math>\rm Z</math><br><math>\rm ZC</math><br><math>\rm IZ</math>
|
|-
|
|
|<math>\rm IZF=CZF+Powerset+\Pi_\omega^{set}-Reflection</math><br><math>\rm ZF=CZF+LEM=IZF+LEM</math><br><math>\rm ZFC</math><br><math>\rm ZFC+V=L</math><br><math>\rm AST</math><br><math>\rm IST</math><br><math>\rm NBG=GBC</math><br><math>\rm GB</math>
|
|}