Googology Wiki - 用户贡献 [zh-cn]

证明论序数

2025-09-16T17:41:18Z

QuantumJack1：

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

=== 定义和性质 ===
对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（<math>|T|</math> 或 <math>\text{PTO}(T)</math>）定义为能用超限归纳证明的原始递归良序的序型最大值。

证明论序数满足：

# 对任意递归序数 <math>\beta<|T|</math>，理论 <math>T</math> 能证明“所有序数小于 <math>\beta</math> 的原始递归良序关系都是良序的”；对 <math>\alpha=|T|</math>，理论 <math>T</math> 无法证明“所有序数小于 <math>\alpha</math> 的原始递归良序关系都是良序的”。
# 存在一种递归记号系统，自然表示所有小于 <math>|T|</math> 的序数；理论 <math>T</math> 能通过超限归纳（序数是良序集的序型，满足超限归纳原理：<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\nvdash\perp</math>）；理论 <math>T</math> 能证明所有初等递归函数在小于 <math>|T|</math> 的序数上总停止；对任意递归序数 <math>\beta<|T|</math>，至少不满足上述条件中的一条。
# 证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序。

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

ZFC 相关证明论序数：

* <math>\mathrm{S}_0 = (\mathrm{Ext}) + (\mathrm{Null}) + (\mathrm{Pair}) + (\mathrm{Union}) + (\mathrm{Diff})\ (\text{Rudimentary set theory})</math>
* <math>\mathrm{S}_1 = \mathrm{S}_0 + (\mathrm{Powerset})</math>
* <math>\mathrm{M}_0 = \mathrm{S}_1 + (\Delta_0^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{M}_1 = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Transitive\ Containment})</math>
* <math>\mathrm{KP}^- = \mathrm{S}_0 + (\mathrm{Infinity}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP}^{-\infty} = \mathrm{S}_0 + (\mathrm{Foundation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP} = \mathrm{KP}^{-\infty} + (\mathrm{Infinity}) = \mathrm{KP}^- + (\mathrm{Foundation})</math>
* <math>\mathrm{KPl} = \mathrm{KP} + (\text{universe limit of admissible sets})</math>
* <math>\mathrm{KPi} = \mathrm{KP} + (\text{recursively inaccessible universe})</math>
* <math>\mathrm{KPh} = \mathrm{KP} + (\text{recursively hyperinaccessible universe})</math>
* <math>\mathrm{KPM} = \mathrm{KP} + (\text{recursively Mahlo universe})</math>
* <math>\mathrm{ZBQC} = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\mathrm{Choice})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{MAC} = \mathrm{M}_1 + (\mathrm{Infinity}) + (\mathrm{Choice}) = \mathrm{ZBQC} + (\text{Transitive Containment})</math>
* <math>\mathrm{MOST} = \mathrm{MAC} + (\Delta_0^{\mathrm{set}} - \mathrm{Collection}) = \mathrm{ZBQC} + \mathrm{KP} + (\Sigma_1^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{Z} = \mathrm{S}_1 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\Sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{ZC} = \mathrm{Z} + (\mathrm{Choice}) = \mathrm{ZBQC} + (\sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{MAC} + \forall m (\beth_{\beth_{m}}\text{ exists})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{Z} + (\Pi_2^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{NFU}^* = \mathrm{NFU} + (\mathrm{Counting}) + (\mathrm{Strongly\ Cantorian\ Separation})</math>
* <math>\mathrm{Z} + (\Pi_m^{\mathrm{set}} - \mathrm{Replacement})</math>
* <math>\mathrm{ZF} = \mathrm{Z} + (\Pi_\omega^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{AST}</math> <math>\mathrm{GB}</math>
* <math>\mathrm{ZFC} = \mathrm{ZF} + (\text{Choice})</math> <math>\mathrm{NBG} = \mathrm{GBC} = \mathrm{GB} + (\text{Global Choice})</math>
* <math>\mathrm{ZFC} + (\text{there is a worldly cardinal})</math>
* <math>\mathrm{NBG} + (\text{there is a stationary proper class of worldly cardinals})</math>
* <math>\mathrm{NBG} + (\text{Class Forcing Theorem})</math> <math>\mathrm{NBG} + (\text{Clopen Class Game Determinacy})</math>
* <math>\mathrm{MK} = \mathrm{NBG} + (\Pi_{\infty}^{\mathrm{class}} - \mathrm{CA})</math>
* <math>\mathrm{ZFC} + (\text{there is an inaccessible cardinal})</math> <math>\mathrm{ZFC} + (\Pi_{1}^{1}\ \text{Perfect Set Property})</math> <math>\mathrm{ZFC} + (\Sigma_{3}^{1}\ \text{Lebesgue measurability})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega\ \text{inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\forall\alpha(\omega \leq \alpha \leq \aleph_{\omega} \Rightarrow |\mathrm{V}_{\alpha} \cap L| = |\alpha|))</math>
* <math>\mathrm{ZFC} + (\text{there is a proper class of inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\text{Grothendieck Universe Axiom})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \Sigma_{n}^{\mathrm{set}}\text{-reflecting cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \sigma_{\omega}^{\mathrm{set}}\text{-reflecting cardinal})</math> <math>\mathrm{ZFC} + (\text{Ord is Mahlo})</math>
* <math>\mathrm{ZFC} + (\text{there is an uplifting cardinal})</math> <math>\mathrm{ZFC} + (\text{Resurrection Axioms})</math>
* <math>\mathrm{ZFC} + (\text{there is a Mahlo cardinal})</math>
* <math>\mathrm{SMAH} = \mathrm{ZFC} + (\text{there is a } n\text{-Mahlo cardinal})_{n\in\mathbb{N}}</math> <math>\mathrm{NFUA} = \mathrm{NFU} + (\text{Infinity}) + (\text{Cantorian Sets})</math>
* <math>\mathrm{SMAH}^{+} = \mathrm{ZFC} + \forall n(\text{there is a } n\text{-Mahlo cardinal})</math>
* <math>\mathrm{MK} + (\text{Ord is weakly compact})</math> <math>\mathrm{GPK}_{\infty}^{+} = \mathrm{GPK}^{+} + (\text{Infinity})</math> <math>\mathrm{NFUB} =\mathrm{NFU} +(\text{Infinity}) + (\text{Cantorian Sets}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFC} + (\text{there is a weakly compact cardinal})</math> <math>\mathrm{ZFC} + (\omega_{2}\ \text{has the tree property})</math>
* <math>\mathrm{ZFC} + (\text{there is a totally indescribable cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a subtle cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is an ineffable cardinal})</math>
* <math>\mathrm{ZFC} + \forall\alpha(\alpha < \omega_{1} \Rightarrow \text{there is a } \alpha\text{-Erdős cardinal})</math>
* <math>\mathrm{ZFC} + (0^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (L \models \aleph_{\omega}\ \text{is regular})</math> <math>\mathrm{ZFC} + \forall \alpha (\alpha \geq \omega \Longrightarrow |V_{\alpha} \cap L| = |\alpha|)</math> <math>\mathrm{ZFC} + (\text{parameter-free } \Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x \in \mathbb{R} \Longrightarrow x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{2}^{1}\ \text{universal Baireness})</math>
* <math>\mathrm{ZFC} + (\text{there is an } \omega_{1}\text{-Erdős cardinal})</math> <math>\mathrm{ZFC} + (\text{Chang's Conjecture})</math>
* <math>\mathrm{SRP} = \mathrm{ZFC} + (\text{there is cardinal with the } n\text{-stationary Ramsey property})_{n \in \mathbb{N}}</math>
* <math>\mathrm{SRP}^{+} = \mathrm{ZFC} + \forall n\ (\text{there is a cardinal with the } n\text{-stationary Ramsey property})</math>
* <math>\mathrm{MK} + (\text{Ord is measurable})</math> <math>\mathrm{NFUM} = \mathrm{NFU} + (\text{Infinity}) + (\text{Large Ordinals}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFM} = \mathrm{ZFC} + (\text{there is a measurable cardinal})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is precipitous})</math> <math>\mathrm{ZF} + (\omega_{1}\ \text{is measurable})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = 2)</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{2}}\ \text{is precipitous})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = \kappa^{++})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{ZFC} + (2^{\aleph_{\omega}} = \aleph_{\omega + 2})</math>
* <math>\mathrm{ZFC} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{2} + (\Delta_{2}^{1}\text{-determinacy})\ (\text{conjectural})</math>
* <math>\mathrm{MK} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\text{lightface } \Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{NBG} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + (\text{there is a Woodin cardinal})</math> <math>\mathrm{ZFC} + (\Delta_{2}^{1}\text{-determinacy})</math> <math>\mathrm{ZFC} + (\mathrm{OD} \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is } \omega_{2}\text{-saturated})</math>
* <math>\mathrm{ZFC} + (\text{there are } n\ \text{Woodin cardinals})_{n \in \mathbb{N}}</math> <math>\mathrm{Z}_{2} + (\mathrm{PD})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega \text{ Woodin cardinals})</math> <math>\mathrm{ZF} + (\mathrm{AD})</math> <math>\mathrm{ZFC} + (L(\mathbb{R}) \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{OD}(\mathbb{R}) \models \mathrm{AD})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\omega_1)\text{-strongly compact})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_1} \text{ is } \omega_1\text{-dense})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\mathbb{R})\text{-strongly compact})</math> <math>\mathrm{ZF} + \mathrm{DC} + (\mathrm{AD}_{\mathbb{R}})</math>
* <math>\mathrm{ZFC} + \text{(there is a superstrong cardinal)}</math>
* <math>\mathrm{ZFC} + \text{(there is a subcompact cardinal)}</math> <math>\mathrm{ZFC} + (V = L[\vec{E}]) + \exists\kappa(\neg\square_{\kappa})</math>
* <math>\mathrm{ZFC} + \text{(there is a strongly compact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Proper Forcing Axiom)}</math>
* <math>\mathrm{ZFC} + \text{(there is a supercompact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Martin's Maximum)}</math>
* <math>\mathrm{ZFC} + \forall n \text{(there is a proper class of } C^{(n)}\text{-extendible cardinals)}</math> <math>\mathrm{ZFC} + \text{(Vopěnka's Principle)}</math>
* <math>\mathrm{ZFC} + \text{(there is a high-jump cardinal)}</math>
* <math>\mathrm{HUGE} = \mathrm{ZFC} + \text{( there is a } n\text{-huge cardinal )}_{n\in\mathbb{N}}</math>
* <math>\mathrm{ZFC} + \text{(Wholeness Axiom } \mathrm{WA}_n)</math>
* <math>\mathrm{ZFC} + \mathrm{I}3 = \mathrm{ZFC} + \exists\lambda(E_0(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}2 = \mathrm{ZFC} + \exists\lambda(E_1(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}1 = \mathrm{ZFC} + \exists\lambda(E_{\omega}(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}0</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \exists\lambda\exists j : V_{\lambda + 2} \prec_{\Sigma_{\omega}^{\mathrm{set}}} V_{\lambda + 2}</math>
* <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math>

[[分类:集合论相关]]

序数表

2025-09-16T17:34:58Z

QuantumJack1：

本条目列举出一些有名字的[[序数]]，它们大多在 [[googology]] 中具有重大意义。

需要注意的是，它们的命名很多来自 googology 爱好者而非专业数学研究者。

=== 序数表 ===
{| class="wikitable"
|-
! 缩写 !! 英文全称 !! 常规表示方法（[[序数坍缩函数#BOCF|BOCF]] 等） !! [[BMS]] / [[Y序列|Y]]
|-
| [[FTO]]|| First Transfinite Ordinal || <math>\omega</math>|| <math>\mathrm{BMS}(0)(1)</math>
|-
| [[LAO]]|| Linear Array Ordinal<ref>因为在googology一度经典的线性数阵的极限是它，因此得名</ref>|| <math>\omega^\omega</math>|| <math>\mathrm{BMS}(0)(1)(2)</math>
|-
| [[SCO]]|| Small Cantor Ordinal || <math>\varphi(1,0)=\varepsilon_0=\psi(\Omega)</math>|| <math>\mathrm{BMS}(0)(1,1)</math>
|-
| [[CO]]|| Cantor Ordinal || <math>\varphi(2,0)=\zeta_0=\psi(\Omega^2)</math>|| <math>\mathrm{BMS}(0)(1,1)(2,1)</math>
|-
|[[LCO]]
|Large Cantor Ordinal
|<math>\varphi(3,0)=\eta_0=\psi(\Omega^3)</math>
|<math>\mathrm{BMS}(0)(1,1)(2,1)(2,1)</math>
|-
| [[HCO]]|| Hyper Cantor Ordinal || <math>\varphi(\omega,0)=\psi(\Omega^\omega)</math>|| <math>\mathrm{BMS}(0)(1,1)(2,1)(3)</math>
|-
| [[FSO]]|| Feferman-Schütte Ordinal || <math>\varphi(1,0,0)=\Gamma_0=\psi(\Omega^\Omega)</math>|| <math>\mathrm{BMS}(0)(1,1)(2,1)(3,1)</math>
|-
|[[ACO]]
|Ackermann Ordinal
|<math>\varphi(1,0,0,0)=\psi(\Omega^{\Omega^2})</math>
|<math>\mathrm{BMS}(0)(1,1)(2,1)(3,1)(3,1)</math>
|-
| [[SVO]]|| Small Veblen Ordinal || <math>\psi(\Omega^{\Omega^\omega})</math>|| <math>\mathrm{BMS}(0)(1,1)(2,1)(3,1)(4)</math>
|-
| [[LVO]]|| Large Veblen Ordinal || <math>\psi(\Omega^{\Omega^\Omega})</math>|| <math>\mathrm{BMS}(0)(1,1)(2,1)(3,1)(4,1)</math>
|-
| [[BHO]]|| Bachmann-Howard Ordinal || <math>\psi(\Omega_{2})</math>|| <math>\mathrm{BMS}(0)(1,1)(2,2)</math>
|-
| [[BO]]|| Buchholz's Ordinal || <math>\psi(\Omega_{\omega})</math>|| <math>\mathrm{BMS}(0)(1,1,1)</math>
|-
| [[TFBO]]|| Takeuti-Feferman-Buchholz Ordinal || <math>\psi(\Omega_{\omega+1})</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1)(3,2)</math>
|-
| [[BIO]]|| Bird's Ordinal<ref>鸟之数阵第四版的极限是它，因此得名</ref>|| <math>\psi(\Omega_{\Omega})</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1)</math>
|-
| [[EBO]]|| Extended Buchholz Ordinal || <math>\psi(I)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1)(2)</math>
|-
| [[JO]]|| Jager's Ordinal || <math>\psi(\Omega_{I+1})</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1)(4,2)</math>
|-
| [[SIO]]|| Small Inaccessible Ordinal || <math>\psi(I_{\omega})</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)</math>
|-
| [[MBO]]|| Mutiply Buchholz Ordinal || <math>\psi(I(\omega,0))=\psi(M^\omega)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(3)</math>
|-
|[[TBO]]
|Transfinitary Buchholz's Ordinal
|<math>\psi(I(1,0,0))=\psi(M^M)</math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(3,1)(2)</math>
|-
| [[SRO]]|| Small Rathjen Ordinal || <math>\psi(\varepsilon_{M+1})</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(3,1,0)(4,2)</math>
|-
| [[SMO]]|| Small Mahlo Ordinal || <math>\psi(M_\omega)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(3,1,1)</math>
|-
|[[SNO]]
|Small 1-Mahlo (N) Ordinal
|<math>\psi(N_\omega)</math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(3,1,1)(3,1,1)</math>
|-
| [[RO]]|| Rathjen's Ordinal || <math>\psi(\varepsilon_{K+1})</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(4,1)(5,2)</math>
|-
|[[SKO]]
|Small Weakly Compact (K) Ordinal
|<math>\psi(K_\omega)</math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)</math>
|-
|[[DO]]
|Duchhart's Ordinal
|<math>\psi(2 \ \rm{aft} \ 4)</math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5,1)(6,2)</math>
|-
| [[SSO]]|| Small Stegert Ordinal || <math>\psi(psd.\Pi_{\omega})=\psi(a_2)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,2)</math>
|-
| [[LSO]]|| Large Stegert Ordinal || <math>\psi(\lambda\alpha.(\alpha\times 2)-\Pi_{0})=\psi(a_2^a)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,2)(3,2)(4,1)(2)</math>
|-
|[[APO]]
|Admissible-parameter free effective cardinal Ordinal
|<math>\psi(\lambda\alpha.(\Omega_{\alpha+1})-\Pi_1)=\psi(a_2^{\Omega_{a+1}}+\psi_{a_2}(a_2^{\Omega_{a+1}})\times\omega)</math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,2)(3,2)(4,1,1)</math>
|-
| [[BGO]]|| TSS 1st Back Gear Ordinal (CN ggg)<ref>Bashicu对BGO的原定义是BMS(0)(1,1,1)(2,2)。BGO指(0)(1,1,1)(2,2,1)是中文googology社区的重命名</ref>|| <math>\psi(\lambda\alpha.(\Omega_{\alpha+2})-\Pi_{1})=\psi(\Omega_{a_2+1}+\psi_{a_2}(\Omega_{a_2+1})\times\omega)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,2,1)</math>
|-
| [[SDO]]|| Small Dropping Ordinal || <math>\psi(\lambda\alpha.(\Omega_{\alpha+\omega})-\Pi_{0}=\psi(\Omega_{a_2+1}\times\omega)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,2,1)(3)</math>
|-
| [[LDO]]|| Large Dropping Ordinal || <math>\psi(\lambda\alpha.(\psi_{I_{\alpha+1}}(0))-\Pi_{0})=\psi(\Omega_{a_2+1}\times a_2)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,2,1)(3,2)</math>
|-
|[[DSO]]
|Doubly +1 Stable Ordinal
|<math>\psi(\lambda\alpha.(\lambda\beta.\beta+1-\Pi_0)-\Pi_0=\psi(a_3) </math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,2,1)(3,3)</math>
|-
|[[TSO]]
|Triply +1 Stable Ordinal
|<math>\psi(\lambda\alpha.(\lambda\beta.(\lambda\gamma.\gamma+1-\Pi_0)-\Pi_0)-\Pi_0=\psi(a_4) </math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,2,1)(3,3,1)(4,4)</math>
|-
| [[LRO|pfec LRO]]|| pfec Large Rathjen Ordinal || <math>\psi(pfec.\omega-\pi-\Pi_{0})=\psi(a_\omega)</math>|| <math>\mathrm{BMS}(0)(1,1,1)(2,2,2)</math>
|-
|[[LRO|SBO]]
|Small Bashicu Ordinal
| <math>\psi(pfec.\omega-\pi-\Pi_{0})=\psi(a_\omega) </math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,2,2)</math>
|-
|[[方括号稳定|pfec M2O]]
|pfec min Σ2 Ordinal
|<math>\psi(pfec.\min(a\prec_{\Sigma_1}b\prec_{\Sigma_2}c)) </math>
|<math>\mathrm{BMS}(0)(1,1,1)(2,2,2)(3,2,2)(4,2,2)(4,2,1)</math>？
|-
|[[LRO]]
|Large Rathjen Ordinal
|<math>F\cap\omega_1^\text{CK},\theta=\omega </math>
|<math>\leqslant\mathrm{BMS}(0)(1,1,1,1)?</math>
|-
|[[TSSO]] / SSPO
|Trio Sequence System Ordinal / Small Simple Projection Ordinal
|<math>\psi(\omega-\text{proj.})=\psi(\sigma S\times \omega)=\psi(H^\omega)</math>
|<math>\mathrm{BMS}(0)(1,1,1,1)</math>
|-
|[[LSPO]]
|Large Simple Projection Ordinal
|<math>\psi(\min\ \alpha\text{ is }\alpha-\text{proj.})=\psi(\sigma S\times S) </math>
|<math>\mathrm{BMS}(0)(1,1,1,1)(2,1,1,1)(3,1)(2)</math>
|-
|[[Q0.5BGO]]
|QSS 0.5th Back Gear Ordinal
|<math>\psi(\psi_S(\sigma S\times S\times \omega+S_2)) </math>
|<math>\rm{BMS}(0)(1,1,1,1)(2,2)</math>
|-
|[[Q1BGO]]
|QSS 1st Back Gear Ordinal
| <math>\psi(\psi_S(\sigma S\times S\times \omega+S_\omega)) </math>
|<math>\mathrm{BMS}(0)(1,1,1,1)(2,2,2)</math>
|-
|[[ESPO]]
|Extend Simple Projection Ordinal
| <math>\psi(\psi_S(\sigma S\times S\times \omega^2)) </math>
|<math>\mathrm{BMS}(0)(1,1,1,1)(2,2,2,1)</math>
|-
|[[BOBO]]
|Big Omega Back Ordinal
| <math>\psi((\omega,0)-P)=\psi(\psi_{H}(H^{H\omega})) </math>
|<math>\mathrm{BMS}(0)(1,1,1,1)(2,2,2,2)</math>
|-
| [[QSSO]]|| Quardo Sequence System Ordinal || <math>\psi(\psi_{H}(H^{H^{\omega}}))</math>|| <math>\mathrm{BMS}(0,0,0,0,0)(1,1,1,1,1)</math>
|-
|[[QSSO|TCAO]]
|Trio Comprehension Axiom Ordinal
|<math>\text{PTO}((\Pi_3^1-CA)_0) </math>
|<math>\geqslant\mathrm{BMS}(0)(1,1,1,1,1)</math>
|-
|QiSSO
|Quinto Sequence System Ordinal
| <math>\psi(\psi_{H}(H^{H^{H^{\omega}}}))</math>
|<math>\mathrm{BMS}(0)(1,1,1,1,1,1)</math>
|-
| [[SHO]] / BMO<ref name=":0">SHO,MHO的名字均来自FataliS1024.但原定义的SHO指的是<math>\varepsilon_0</math>,MHO指的是BMS极限。还有一个LHO指<math>\omega -Y</math>极限。但后来不知为何变成了现在的这个版本，而LHO成为了无定义的名字</ref>|| Small Hydra Ordinal / Bashicu Matrix Ordinal || <math>\psi(\psi_{H}(\varepsilon_{H+1}))?</math>|| <math>Y(1,3)=\lim(\rm BMS)</math>
|-
|βO
|Beta Universe Ordinal
|<math>\rm PTO(Z_2)</math>
|<math>\geqslant Y(1,3)</math>
|-
| [[ΩSSO]]|| Ω Sequence System Ordinal || <math>\psi(\psi_H(\varphi(\Omega,H+1)))?</math>|| <math>Y(1,3,4,2,5,8,10)</math>
|-
|[[LRPO]]
|Large Right Projection Ordinal
|<math>\psi(\psi_{H}(\varphi(H,1)))?</math>
|<math>Y(1,3,4,2,5,8,10,4,9,14,17,10)</math>
|-
| [[GHO]]|| No-Go Hydra Ordinal<ref>原名Guo bu qu de Hydra Ordinal，但过于口语化和非正式。而这个序数本身确实是一个重要的序数。曹知秋将名字改成了现在的版本</ref>|| <math>\psi(\psi_H(\psi_T(T_2\times 2)))?</math>|| <math>Y(1,3,4,3)</math>
|-
|[[DCO]]
|Difference Catching Ordinal
|<math>\psi(\psi_H(\psi_T(T_2\times\psi_T(T_2^2))))?</math>
|<math>Y(1,3,5)</math>
|-
| [[SYO]]|| Small Yukito Ordinal || <math>\omega \rm{ MN}(0)(,,,1)</math>|| <math>\lim(1-Y)=\omega-Y(1,4)</math>
|-
| [[MHO]] / ωYO<ref name=":0" />|| Medium Hydra Ordinal / ω-Y sequence Ordinal || <math>\omega \rm{2MN}(0)(;1)</math>|| <math>\lim(\omega-Y)</math>
|-
| [[CKO]]|| Church-Kleene Ordinal || <math>\omega_{1}^{\rm CK}</math>
|-
| [[FUO]]|| First Uncountable Ordinal || <math>\omega_{1}</math>||
|}

=== 已弃用序数表 ===
{| class="wikitable"
!缩写
!英文全称
!定义
!大小
!命名者
|-
|SMDO
|Small Multidimensional Ordinal
|<math>\omega^\omega</math>
|<math>(0)(1)(2)</math>
|318`4
|-
|SHO
|Small Hydra Ordinal
|<math>\varepsilon_0=\psi(\Omega)</math>
|<math>(0)(1,1)</math>
|FataliS1024
|-
|ESVO
|Extended Small Veblen Ordinal
|<math>\psi\left(\Omega^{\Omega^{\Omega^{\omega}}}\right)</math>
|<math>(0)(1,1)(2,1)(3,1)(4,1)(5)</math>
|
|-
|ELVO
|Extended Large Veblen Ordinal
|<math>\psi\left(\Omega^{\Omega^{\Omega^{\Omega}}}\right)</math>
|<math>(0)(1,1)(2,1)(3,1)(4,1)(5,1)</math>
|
|-
|LDO(旧)
|Large Dropping Ordinal
|<math>\psi(\lambda\alpha.(\Omega_{\alpha\times 2})-\Pi_{0})</math>
|<math>(0)(1,1,1)(2,2,1)(3,1)(2)</math>
|
|-
|EDO
|Extended Dropping Ordinal
|<math>\psi(\lambda\alpha.\psi_{I_{\alpha+1}}(I_{\alpha+1})-\Pi_0)</math>
|<math>(0)(1,1,1)(2,2,1)(3,2)</math>
|
|-
|SEIO
|Small Eveog-Imagined Ordinal
|<math>\Sigma_1\text{ adm.}</math>
|
|
|-
|MEIO
|Medium Eveog-Imagined Ordinal
|<math>\Sigma_2\text{ adm.}</math>
|
|
|-
|LEIO
|Large Eveog-Imagined Ordinal
|<math>\Sigma_3\text{ adm.}</math>
|
|
|-
|SOSO
|Second Order Stable Ordinal
|<math>\psi(1-o-\Sigma_2-\text{stb.})</math>
|
|
|-
|EGO
|Eveog's Ordinal
|<math>\psi(\psi\sigma(\sigma_\omega))</math>
|<math>(0)(1,1,1,1)(2,2,2,1)(3,2,1)(4)</math>
|
|-
|MHO
|Medium Hydra Ordinal
|<math>\lim({\rm BMS})=\lim(0-Y)</math>
|<math>Y(1,3)</math>
|FataliS1024
|-
|LHO
|Large Hydra Ordinal
|<math>\lim(\omega-Y)</math>
|<math>\Omega-Y(1,3,12)</math>
|FataliS1024
|-
|ZDO
|Zeta Differenciating Ordinal
|<math>\text{FOS911 }\Theta(\zeta_0)</math>
|<math>\Omega-Y(1,3,12)</math>
|
|-
|WYO
|Omega Y Ordinal
|<math>\lim(\Omega-Y)</math>
|<math>\Omega-Y(1,\omega)</math>
|318`4
|-
|EYO
|Extended Y Ordinal
|<math>\text{bFOS }\Theta(\text{BHO})</math>
|<math>\text{bFOS }(0)(1)(\omega)(\varepsilon_0)(\text{BHO})</math>
|318`4
|-
|UCO
|Upgrade Catching Ordinal
|<math>\text{sFOS }\Theta(\text{BHO})</math>
|<math>\text{bFOS }\Theta(\text{BO})</math>
|318`4
|-
|XYO
|Extreme Y Ordinal
|<math>\text{bFOS }\Theta(\text{BO})</math>
|<math>\text{bFOS }(0)(1)(\omega)(\varepsilon_0)(\text{BO})</math>
|318`4
|-
|DMO
|Difference Matrix Ordinal
|<math>\text{sFOS }\Theta(\text{BO})</math>
|<math>\text{bFOS }\Theta(\text{SHO})</math>
|318`4
|-
|GYO / 😰O
|Grand Y-Sequence Ordinal / 😰 Ordinal
|<math>\lim(X-Y)</math>
|<math>\text{sFOS }(0)(1)(\omega)(\varepsilon_0)(\text{SHO})</math>
|318`4
|-
|LDCO
|Large Difference Catching Ordinal
|<math>\text{sFOS }\Theta(\text{SYO})</math>
|<math>\text{b2-FOS }\Theta(\zeta_1)</math>
|318`4
|-
|RHO
|Remaining Hydra Ordinal
|<math>\lim(\text{sFOS})</math>
|<math>\text{b2-FOS }\Theta(\varphi(\omega,0))</math>
|318`4
|-
|WFO
|Omega Fundamental Ordinal
|<math>\lim(\text{Weak 2-FOS})</math>
|<math>\text{b2-FOS }\Theta(\Gamma_0)</math>
|318`4
|-
|TMDO
|Tri-Multidimensional Ordinal
|<math>\text{s2-FOS }\Theta(\varphi(\omega,0))</math>
|<math>\omega2-\text{RD}</math>
|318`4
|-
|ERHO
|Extended Remaining hydra Ordinal
|<math>\lim(\text{b2-FOS})</math>
|<math>\omega2+1-\text{RD}</math>
|318`4
|-
|LMDO
|Large Multidimensional Ordinal
|<math>\lim(\omega-\text{FOS})</math>
|<math>\omega^2-\text{RD}</math>
|318`4
|-
|IFO
|Infintesimal Function Ordinal
|<math>\lim(\text{IFS})</math>
|<math>\varepsilon_0-\text{RD}</math>
|318`4
|-
|WRO
|Omega Remaining Ordinal
|<math>\lim(\text{ROS})</math>
|<math>R\ \Omega-Y</math>
|318`4
|-
|SCLO
|Small Code Lift Ordinal
|<math>\sup(n-\text{code})</math>
|
|
|-
|EHO
|Huge Hydra Ordinal
|<math>\lim(\text{pfffz})</math>
|
|夏夜星空
|-
|ROO
|Remaining Omega Ordinal
|<math>R_\omega\text{ remaining}</math>
|
|318`4
|-
|UHO
|Ultimate Hydra Ordinal
|<math>\lim(\text{RSAM})</math>
|
|夏夜星空
|-
|IHO
|Infinite Hydra Ordinal
|<math>\lim(\text{SAM})</math>
|
|夏夜星空
|}
本表取自 [https://docs.qq.com/sheet/DSnFWckliSU5TTE15 Worldly Sheet]：<blockquote>- （SCO/CO/LCO/HCO）谁起不重要，重要的是这是纪念康托尔的，如果没有他所有gggist今天(甚至永远)都走不到一起”

- 你们怎么把它弄成这样了，至少必要的（比如lim fffz/lim X-Y还是要的吧）

- fffz和X-Y公认理想之前搞这么多名字有什么用

- 不然MHO以上全都写成n-RD？- 不对 - 3184为什么要保留他造了那么多没用的序数缩写的黑历史？(bushi) - 不如还是加上毕竟fatalis的SHO/MHO/LHO都有了</blockquote>

==== DNAO ====
DNAO（Disgusting Nonsense Annoyance Ordinal）

定义：
(0)(1,1,1)(2,2,2)(3,3,3)(3,3,0)(4,4,1)(5,5,2)(6,6,2)(7,7,0)(8,8,1)(9,9,2)(10,9,2)(11,9,0)(12,10,1)(13,11,2)(13,11,2)(13,11,1)(14,12,2)(14,11,1)(15,12,2)(15,11,1)(16,12,0)(17,13,1)(18,14,2)(18,14,2)(18,14,1)(19,15,2)(19,14,1)(20,15,2)(20,14,1)(21,15,0)(22,16,1)(23,17,2)(23,17,2)(23,17,1)(24,18,2)(24,17,1)(25,18,2)(25,17,0)(26,18,1)(27,19,2)(27,19,2)(27,19,1)(28,20,2)(28,19,1)(29,20,2)(29,19,0)(30,20,1)(31,21,2)(31,21,2)(31,21,1)(32,22,2)(32,21,1)(33,22,2)(33,21,0)(34,22,1)(35,23,2)(35,23,2)(35,23,1)(36,24,2)(36,23,1)(37,24,2)(37,23,0)(38,24,1)(39,25,2)(40,25,2)(40,25,1)(41,26,2)(41,22,1)(42,23,2)(42,23,2)(42,23,1)(43,24,2)(43,23,1)(44,24,2)(44,23,0)(45,24,1)(46,25,2)(47,25,2)(47,25,1)(48,26,1)(49,27,0)(50,28,1)(51,29,2)(52,29,2)(52,29,1)(53,30,0)(54,31,1)(55,32,2)(56,32,2)(56,32,0)(57,33,1)(58,34,2)(59,34,2)(59,34,0)(60,35,1)(61,36,2)(62,36,2)(62,36,0)(63,37,1)(64,38,2)(65,38,2)(65,38,0)(66,39,1)(67,40,2)(68,40,2)(68,40,0)(69,41,1)(70,42,2)(71,42,2)(71,42,0)(72,43,1)(73,44,0)(74,45,1)(75,44,0)(76,45,1)(77,46,0)(78,47,0)(79,44,0)(80,45,1)(81,46,0)(82,47,0)(83,44,0)(84,45,1)(85,46,0)(86,47,0)(87,44,0)(88,45,1)(89,46,0)(90,47,0)(91,44,0)(92,45,1)(93,46,0)(94,47,0)(95,44,0)(96,45,1)(96,45,1)(96,45,1)(96,45,0)(97,46,0)(98,47,0)(99,48,0)(100,47,0)(101,48,0)(102,47,0)(103,48,0)(104,47,0)(105,48,0)(106,47,0)(107,48,0)(108,45,0)(109,46,0)(110,47,0)(111,47,0)(111,47,0)(111,47,0)(111,47,0)(111,47,0)(111,47,0)(111,46,0)(112,47,0)(113,47,0)(113,47,0)(113,47,0)(113,47,0)(113,47,0)(113,47,0)(113,46,0)(114,47,0)(115,46,0)(116,47,0)(117,46,0)(118,47,0)(119,46,0)(120,45,0)(121,46,0)(122,47,0)(123,47,0)(123,47,0)(123,47,0)(123,47,0)(123,47,0)(123,47,0)(123,46,0)(124,47,0)(125,47,0)(125,47,0)(125,47,0)(125,47,0)(125,47,0)(125,47,0)(125,46,0)(126,47,0)(127,46,0)(128,47,0)(129,46,0)(130,47,0)(131,46,0)(132,45,0)(133,46,0)(134,47,0)(135,47,0)(135,47,0)(135,47,0)(135,47,0)(135,47,0)(135,47,0)(135,46,0)(136,47,0)(137,47,0)(137,47,0)(137,47,0)(137,47,0)(137,47,0)(137,47,0)(137,46,0)(138,47,0)(139,46,0)(140,47,0)(141,46,0)(142,47,0)(143,46,0)(144,45,0)(145,46,0)(146,47,0)(147,47,0)(147,47,0)(147,47,0)(147,47,0)(147,47,0)(147,47,0)(147,46,0)(147,46,0)(147,46,0)(147,46,0)(147,46,0)(147,45,0)(148,46,0)(148,45,0)(149,46,0)(149,45,0)(150,46,0)(150,45,0)(151,45,0)(151,45,0)(150,45,0)(151,45,0)(150,45,0)(151,45,0)(148,45,0)(149,46,0)(149,45,0)(150,46,0)(150,45,0)(151,45,0)(151,45,0)(150,45,0)(151,45,0)(150,45,0)(151,45,0)(148,45,0)(149,46,0)(149,45,0)(150,46,0)(150,45,0)(151,45,0)(151,45,0)(150,45,0)(151,45,0)(150,45,0)(151,45,0)(148,45,0)(149,45,0)(149,45,0)(148,45,0)(149,45,0)(149,45,0)(148,45,0)(149,45,0)(147,45,0)(148,46,0)(148,45,0)(149,46,0)(149,45,0)(150,46,0)(150,45,0)(151,45,0)(151,45,0)(150,45,0)(151,45,0)(148,45,0)(149,46,0)(149,45,0)(150,45,0)(150,45,0)(149,45,0)(150,45,0)(149,45,0)(150,45,0)(149,45,0)(149,45,0)(149,45,0)(146,47,0)(147,47,0)(147,47,0)(147,47,0)(147,47,0)(147,47,0)(147,47,0)(147,46,0)(147,46,0)(147,46,0)(147,46,0)(147,45,0)(148,46,0)(149,47,0)(150,47,0)(150,47,0)(150,47,0)(150,47,0)(150,47,0)(150,47,0)(150,46,0)(150,46,0)(150,46,0)(150,46,0)(150,46,0)(150,45,0)(151,46,0)(151,45,0)(152,46,0)(152,45,0)(153,46,0)(153,45,0)(154,45,0)(154,45,0)(153,45,0)(154,45,0)(153,45,0)(154,45,0)(151,45,0)(152,46,0)(152,45,0)(153,46,0)(153,45,0)(154,45,0)(154,45,0)(153,45,0)(154,45,0)(153,45,0)(154,45,0)(151,45,0)(152,46,0)(152,45,0)(153,46,0)(153,45,0)(154,45,0)(154,45,0)(153,45,0)(154,45,0)(153,45,0)(154,45,0)(151,45,0)(152,45,0)(152,45,0)(151,45,0)(152,45,0)(152,45,0)(151,45,0)(152,45,0)(150,45,0)(151,46,0)(151,45,0)(152,46,0)(152,45,0)(153,46,0)(153,45,0)(154,45,0)(154,45,0)(153,45,0)(154,45,0)(151,45,0)(152,46,0)(152,45,0)(153,45,0)(153,45,0)(152,45,0)(153,45,0)(152,45,0)(153,45,0)(152,45,0)(152,45,0)(152,45,0)(149,47,0)(150,47,0)(150,47,0)(150,47,0)(150,47,0)(150,47,0)(150,47,0)(150,46,0)(150,46,0)(150,46,0)(150,46,0)(150,45,0)(151,46,0)(152,47,0)(152,47,0)(152,47,0)(151,45,0)(152,46,0)(153,47,0)(150,45,0)(151,46,0)(152,47,0)(152,47,0)(152,47,0)(151,45,0)(152,46,0)(153,47,0)(150,45,0)(151,46,0)(152,47,0)(150,45,0)(151,46,0)(152,47,0)(150,45,0)(151,45,0)(152,45,0)(152,45,0)(151,45,0)(152,45,0)(152,45,0)(150,45,0)(149,45,0)
=== 脚注 ===
<references />

证明论序数

2025-09-16T17:24:42Z

QuantumJack1：

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

=== 定义和性质 ===
对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（<math>|T|</math> 或 <math>\text{PTO}(T)</math>）定义为能用超限归纳证明的原始递归良序的序型最大值。

证明论序数满足：

# 对任意递归序数 <math>\beta<|T|</math>，理论 <math>T</math> 能证明“所有序数小于 <math>\beta</math> 的原始递归良序关系都是良序的”；对 <math>\alpha=|T|</math>，理论 <math>T</math> 无法证明“所有序数小于 <math>\alpha</math> 的原始递归良序关系都是良序的”。
# 存在一种递归记号系统，自然表示所有小于 <math>|T|</math> 的序数；理论 <math>T</math> 能通过超限归纳（序数是良序集的序型，满足超限归纳原理：<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\nvdash\perp</math>）；理论 <math>T</math> 能证明所有初等递归函数在小于 <math>|T|</math> 的序数上总停止；对任意递归序数 <math>\beta<|T|</math>，至少不满足上述条件中的一条。
# 证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序。

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

ZFC 相关证明论序数：

* <math>\mathrm{S}_0 = (\mathrm{Ext}) + (\mathrm{Null}) + (\mathrm{Pair}) + (\mathrm{Union}) + (\mathrm{Diff})\ (\text{Rudimentary set theory})</math>
* <math>\mathrm{S}_1 = \mathrm{S}_0 + (\mathrm{Powerset})</math>
* <math>\mathrm{M}_0 = \mathrm{S}_1 + (\Delta_0^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{M}_1 = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Transitive\ Containment})</math>
* <math>\mathrm{KP}^- = \mathrm{S}_0 + (\mathrm{Infinity}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP}^{-\infty} = \mathrm{S}_0 + (\mathrm{Foundation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP} = \mathrm{KP}^{-\infty} + (\mathrm{Infinity}) = \mathrm{KP}^- + (\mathrm{Foundation})</math>
* <math>\mathrm{KPl} = \mathrm{KP} + (\text{universe limit of admissible sets})</math>
* <math>\mathrm{KPi} = \mathrm{KP} + (\text{recursively inaccessible universe})</math>
* <math>\mathrm{KPh} = \mathrm{KP} + (\text{recursively hyperinaccessible universe})</math>
* <math>\mathrm{KPM} = \mathrm{KP} + (\text{recursively Mahlo universe})</math>
* <math>\mathrm{ZBQC} = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\mathrm{Choice})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{MAC} = \mathrm{M}_1 + (\mathrm{Infinity}) + (\mathrm{Choice}) = \mathrm{ZBQC} + (\text{Transitive Containment})</math>
* <math>\mathrm{MOST} = \mathrm{MAC} + (\Delta_0^{\mathrm{set}} - \mathrm{Collection}) = \mathrm{ZBQC} + \mathrm{KP} + (\Sigma_1^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{Z} = \mathrm{S}_1 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\Sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{ZC} = \mathrm{Z} + (\mathrm{Choice}) = \mathrm{ZBQC} + (\sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{MAC} + \forall m (\beth_{\beth_{m}}\text{ exists})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{Z} + (\Pi_2^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{NFU}^* = \mathrm{NFU} + (\mathrm{Counting}) + (\mathrm{Strongly\ Cantorian\ Separation})</math>
* <math>\mathrm{Z} + (\Pi_m^{\mathrm{set}} - \mathrm{Replacement})</math>
* <math>\mathrm{ZF} = \mathrm{Z} + (\Pi_\omega^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{AST}</math> <math>\mathrm{GB}</math>
* <math>\mathrm{ZFC} = \mathrm{ZF} + (\text{Choice})</math> <math>\mathrm{NBG} = \mathrm{GBC} = \mathrm{GB} + (\text{Global Choice})</math>
* <math>\mathrm{ZFC} + (\text{there is a worldly cardinal})</math>
* <math>\mathrm{NBG} + (\text{there is a stationary proper class of worldly cardinals})</math>
* <math>\mathrm{NBG} + (\text{Class Forcing Theorem})</math> <math>\mathrm{NBG} + (\text{Clopen Class Game Determinacy})</math>
* <math>\mathrm{MK} = \mathrm{NBG} + (\Pi_{\infty}^{\mathrm{class}} - \mathrm{CA})</math>
* <math>\mathrm{ZFC} + (\text{there is an inaccessible cardinal})</math> <math>\mathrm{ZFC} + (\Pi_{1}^{1}\ \text{Perfect Set Property})</math> <math>\mathrm{ZFC} + (\Sigma_{3}^{1}\ \text{Lebesgue measurability})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega\ \text{inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\forall\alpha(\omega \leq \alpha \leq \aleph_{\omega} \Rightarrow |\mathrm{V}_{\alpha} \cap L| = |\alpha|))</math>
* <math>\mathrm{ZFC} + (\text{there is a proper class of inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\text{Grothendieck Universe Axiom})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \Sigma_{n}^{\mathrm{set}}\text{-reflecting cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \sigma_{\omega}^{\mathrm{set}}\text{-reflecting cardinal})</math> <math>\mathrm{ZFC} + (\text{Ord is Mahlo})</math>
* <math>\mathrm{ZFC} + (\text{there is an uplifting cardinal})</math> <math>\mathrm{ZFC} + (\text{Resurrection Axioms})</math>
* <math>\mathrm{ZFC} + (\text{there is a Mahlo cardinal})</math>
* <math>\mathrm{SMAH} = \mathrm{ZFC} + (\text{there is a } n\text{-Mahlo cardinal})_{n\in\mathbb{N}}</math> <math>\mathrm{NFUA} = \mathrm{NFU} + (\text{Infinity}) + (\text{Cantorian Sets})</math>
* <math>\mathrm{SMAH}^{+} = \mathrm{ZFC} + \forall n(\text{there is a } n\text{-Mahlo cardinal})</math>
* <math>\mathrm{MK} + (\text{Ord is weakly compact})</math> <math>\mathrm{GPK}_{\infty}^{+} = \mathrm{GPK}^{+} + (\text{Infinity})</math> <math>\mathrm{NFUB} =\mathrm{NFU} +(\text{Infinity}) + (\text{Cantorian Sets}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFC} + (\text{there is a weakly compact cardinal})</math> <math>\mathrm{ZFC} + (\omega_{2}\ \text{has the tree property})</math>
* <math>\mathrm{ZFC} + (\text{there is a totally indescribable cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a subtle cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is an ineffable cardinal})</math>
* <math>\mathrm{ZFC} + \forall\alpha(\alpha < \omega_{1} \Rightarrow \text{there is a } \alpha\text{-Erdős cardinal})</math>
* <math>\mathrm{ZFC} + (0^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (L \models \aleph_{\omega}\ \text{is regular})</math> <math>\mathrm{ZFC} + \forall \alpha (\alpha \geq \omega \Longrightarrow |V_{\alpha} \cap L| = |\alpha|)</math> <math>\mathrm{ZFC} + (\text{parameter-free } \Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x \in \mathbb{R} \Longrightarrow x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{2}^{1}\ \text{universal Baireness})</math>
* <math>\mathrm{ZFC} + (\text{there is an } \omega_{1}\text{-Erdős cardinal})</math> <math>\mathrm{ZFC} + (\text{Chang's Conjecture})</math>
* <math>\mathrm{SRP} = \mathrm{ZFC} + (\text{there is cardinal with the } n\text{-stationary Ramsey property})_{n \in \mathbb{N}}</math>
* <math>\mathrm{SRP}^{+} = \mathrm{ZFC} + \forall n\ (\text{there is a cardinal with the } n\text{-stationary Ramsey property})</math>
* <math>\mathrm{MK} + (\text{Ord is measurable})</math> <math>\mathrm{NFUM} = \mathrm{NFU} + (\text{Infinity}) + (\text{Large Ordinals}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFM} = \mathrm{ZFC} + (\text{there is a measurable cardinal})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is precipitous})</math> <math>\mathrm{ZF} + (\omega_{1}\ \text{is measurable})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = 2)</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{2}}\ \text{is precipitous})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = \kappa^{++})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{ZFC} + (2^{\aleph_{\omega}} = \aleph_{\omega + 2})</math>
* <math>\mathrm{ZFC} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{2} + (\Delta_{2}^{1}\text{-determinacy})\ (\text{conjectural})</math>
* <math>\mathrm{MK} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\text{lightface } \Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{NBG} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + (\text{there is a Woodin cardinal})</math> <math>\mathrm{ZFC} + (\Delta_{2}^{1}\text{-determinacy})</math> <math>\mathrm{ZFC} + (\mathrm{OD} \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is } \omega_{2}\text{-saturated})</math>
* <math>\mathrm{ZFC} + (\text{there are } n\ \text{Woodin cardinals})_{n \in \mathbb{N}}</math> <math>\mathrm{Z}_{2} + (\mathrm{PD})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega \text{ Woodin cardinals})</math> <math>\mathrm{ZF} + (\mathrm{AD})</math> <math>\mathrm{ZFC} + (L(\mathbb{R}) \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{OD}(\mathbb{R}) \models \mathrm{AD})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\omega_1)\text{-strongly compact})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_1} \text{ is } \omega_1\text{-dense})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\mathbb{R})\text{-strongly compact})</math> <math>\mathrm{ZF} + \mathrm{DC} + (\mathrm{AD}_{\mathbb{R}})</math>
* <math>\mathrm{ZFC} + \text{(there is a superstrong cardinal)}</math>
* <math>\mathrm{ZFC} + \text{(there is a subcompact cardinal)}</math> <math>\mathrm{ZFC} + (V = L[\vec{E}]) + \exists\kappa(\neg\square_{\kappa})</math>
* <math>\mathrm{ZFC} + \text{(there is a strongly compact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Proper Forcing Axiom)}</math>
* <math>\mathrm{ZFC} + \text{(there is a supercompact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Martin's Maximum)}</math>
* <math>\mathrm{ZFC} + \forall n \text{(there is a proper class of } C^{(n)}\text{-extendible cardinals)}</math> <math>\mathrm{ZFC} + \text{(Vopěnka's Principle)}</math>
* <math>\mathrm{ZFC} + \text{(there is a high-jump cardinal)}</math>
* <math>\mathrm{HUGE} = \mathrm{ZFC} + \text{( there is a } n\text{-huge cardinal )}_{n\in\mathbb{N}}</math>
* <math>\mathrm{ZFC} + \text{(Wholeness Axiom } \mathrm{WA}_n)</math>
* <math>\mathrm{ZFC} + \mathrm{I}3 = \mathrm{ZFC} + \exists\lambda(E_0(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}2 = \mathrm{ZFC} + \exists\lambda(E_1(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}1 = \mathrm{ZFC} + \exists\lambda(E_{\omega}(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}0</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \exists\lambda\exists j : V_{\lambda + 2} \prec_{\Sigma_{\omega}^{\mathrm{set}}} V_{\lambda + 2}</math>
* <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math>

[[分类:集合论相关]]

证明论序数

2025-09-16T17:22:12Z

QuantumJack1：/* 证明论序数表 */ 排版

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

=== 定义和性质 ===
对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（<math>|T|</math> 或 <math>\text{PTO}(T)</math>）定义为能用超限归纳证明的原始递归良序的序型最大值。

证明论序数满足：

# 对任意递归序数 <math>\beta<|T|</math>，理论 <math>T</math> 能证明“所有序数小于 <math>\beta</math> 的原始递归良序关系都是良序的”；对 <math>\alpha=|T|</math>，理论 <math>T</math> 无法证明“所有序数小于 <math>\alpha</math> 的原始递归良序关系都是良序的”。
# 存在一种递归记号系统，自然表示所有小于 <math>|T|</math> 的序数；理论 <math>T</math> 能通过超限归纳（序数是良序集的序型，满足超限归纳原理：<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\nvdash\perp</math>）；理论 <math>T</math> 能证明所有初等递归函数在小于 <math>|T|</math> 的序数上总停止；对任意递归序数 <math>\beta<|T|</math>，至少不满足上述条件中的一条。
# 证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序。

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

ZFC 相关证明论序数：

* <math>\mathrm{S}_0 = (\mathrm{Ext}) + (\mathrm{Null}) + (\mathrm{Pair}) + (\mathrm{Union}) + (\mathrm{Diff})\ (\text{Rudimentary set theory})</math>
* <math>\mathrm{S}_1 = \mathrm{S}_0 + (\mathrm{Powerset})</math>
* <math>\mathrm{M}_0 = \mathrm{S}_1 + (\Delta_0^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{M}_1 = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Transitive\ Containment})</math>
* <math>\mathrm{KP}^- = \mathrm{S}_0 + (\mathrm{Infinity}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP}^{-\infty} = \mathrm{S}_0 + (\mathrm{Foundation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP} = \mathrm{KP}^{-\infty} + (\mathrm{Infinity}) = \mathrm{KP}^- + (\mathrm{Foundation})</math>
* <math>\mathrm{KPl} = \mathrm{KP} + (\text{universe limit of admissible sets})</math>
* <math>\mathrm{KPi} = \mathrm{KP} + (\text{recursively inaccessible universe})</math>
* <math>\mathrm{KPh} = \mathrm{KP} + (\text{recursively hyperinaccessible universe})</math>
* <math>\mathrm{KPM} = \mathrm{KP} + (\text{recursively Mahlo universe})</math>
* <math>\mathrm{ZBQC} = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\mathrm{Choice})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{MAC} = \mathrm{M}_1 + (\mathrm{Infinity}) + (\mathrm{Choice}) = \mathrm{ZBQC} + (\text{Transitive Containment})</math>
* <math>\mathrm{MOST} = \mathrm{MAC} + (\Delta_0^{\mathrm{set}} - \mathrm{Collection}) = \mathrm{ZBQC} + \mathrm{KP} + (\Sigma_1^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{Z} = \mathrm{S}_1 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\Sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{ZC} = \mathrm{Z} + (\mathrm{Choice}) = \mathrm{ZBQC} + (\sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{MAC} + \forall m (\beth_{\beth_{m}}\text{ exists})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{Z} + (\Pi_2^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{NFU}^* = \mathrm{NFU} + (\mathrm{Counting}) + (\mathrm{Strongly\ Cantorian\ Separation})</math>
* <math>\mathrm{Z} + (\Pi_m^{\mathrm{set}} - \mathrm{Replacement})</math>
* <math>\mathrm{ZF} = \mathrm{Z} + (\Pi_\omega^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{AST}</math> <math>\mathrm{GB}</math>
* <math>\mathrm{ZFC} = \mathrm{ZF} + (\text{Choice})</math> <math>\mathrm{NBG} = \mathrm{GBC} = \mathrm{GB} + (\text{Global Choice})</math>
* <math>\mathrm{ZFC} + (\text{there is a worldly cardinal})</math>
* <math>\mathrm{NBG} + (\text{there is a stationary proper class of worldly cardinals})</math>
* <math>\mathrm{NBG} + (\text{Class Forcing Theorem})</math> <math>\mathrm{NBG} + (\text{Clopen Class Game Determinacy})</math>
* <math>\mathrm{MK} = \mathrm{NBG} + (\Pi_{\infty}^{\mathrm{class}} - \mathrm{CA})</math>
* <math>\mathrm{ZFC} + (\text{there is an inaccessible cardinal})</math> <math>\mathrm{ZFC} + (\Pi_{1}^{1}\ \text{Perfect Set Property})</math> <math>\mathrm{ZFC} + (\Sigma_{3}^{1}\ \text{Lebesgue measurability})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega\ \text{inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\forall\alpha(\omega \leq \alpha \leq \aleph_{\omega} \Rightarrow |\mathrm{V}_{\alpha} \cap L| = |\alpha|))</math>
* <math>\mathrm{ZFC} + (\text{there is a proper class of inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\text{Grothendieck Universe Axiom})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \Sigma_{n}^{\mathrm{set}}\text{-reflecting cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \sigma_{\omega}^{\mathrm{set}}\text{-reflecting cardinal})</math> <math>\mathrm{ZFC} + (\text{Ord is Mahlo})</math>
* <math>\mathrm{ZFC} + (\text{there is an uplifting cardinal})</math> <math>\mathrm{ZFC} + (\text{Resurrection Axioms})</math>
* <math>\mathrm{ZFC} + (\text{there is a Mahlo cardinal})</math>
* <math>\mathrm{SMAH} = \mathrm{ZFC} + (\text{there is a } n\text{-Mahlo cardinal})_{n\in\mathbb{N}}</math> <math>\mathrm{NFUA} = \mathrm{NFU} + (\text{Infinity}) + (\text{Cantorian Sets})</math>
* <math>\mathrm{SMAH}^{+} = \mathrm{ZFC} + \forall n(\text{there is a } n\text{-Mahlo cardinal})</math>
* <math>\mathrm{MK} + (\text{Ord is weakly compact})</math> <math>\mathrm{GPK}_{\infty}^{+} = \mathrm{GPK}^{+} + (\text{Infinity})</math> <math>\mathrm{NFUB} =\mathrm{NFU} +(\text{Infinity}) + (\text{Cantorian Sets}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFC} + (\text{there is a weakly compact cardinal})</math> <math>\mathrm{ZFC} + (\omega_{2}\ \text{has the tree property})</math>
* <math>\mathrm{ZFC} + (\text{there is a totally indescribable cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a subtle cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is an ineffable cardinal})</math>
* <math>\mathrm{ZFC} + \forall\alpha(\alpha < \omega_{1} \Rightarrow \text{there is a } \alpha\text{-Erdős cardinal})</math>
* <math>\mathrm{ZFC} + (0^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (L \models \aleph_{\omega}\ \text{is regular})</math> <math>\mathrm{ZFC} + \forall \alpha (\alpha \geq \omega \Longrightarrow |V_{\alpha} \cap L| = |\alpha|)</math> <math>\mathrm{ZFC} + (\text{parameter-free } \Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x \in \mathbb{R} \Longrightarrow x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{2}^{1}\ \text{universal Baireness})</math>
* <math>\mathrm{ZFC} + (\text{there is an } \omega_{1}\text{-Erdős cardinal})</math> <math>\mathrm{ZFC} + (\text{Chang's Conjecture})</math>
* <math>\mathrm{SRP} = \mathrm{ZFC} + (\text{there is cardinal with the } n\text{-stationary Ramsey property})_{n \in \mathbb{N}}</math>
* <math>\mathrm{SRP}^{+} = \mathrm{ZFC} + \forall n\ (\text{there is a cardinal with the } n\text{-stationary Ramsey property})</math>
* <math>\mathrm{MK} + (\text{Ord is measurable})</math> <math>\mathrm{NFUM} = \mathrm{NFU} + (\text{Infinity}) + (\text{Large Ordinals}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFM} = \mathrm{ZFC} + (\text{there is a measurable cardinal})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is precipitous})</math> <math>\mathrm{ZF} + (\omega_{1}\ \text{is measurable})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = 2)</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{2}}\ \text{is precipitous})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = \kappa^{++})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{ZFC} + (2^{\aleph_{\omega}} = \aleph_{\omega + 2})</math>
* <math>\mathrm{ZFC} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{2} + (\Delta_{2}^{1}\text{-determinacy})\ (\text{conjectural})</math>
* <math>\mathrm{MK} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\text{lightface } \Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{NBG} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + (\text{there is a Woodin cardinal})</math> <math>\mathrm{ZFC} + (\Delta_{2}^{1}\text{-determinacy})</math> <math>\mathrm{ZFC} + (\mathrm{OD} \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is } \omega_{2}\text{-saturated})</math>
* <math>\mathrm{ZFC} + (\text{there are } n\ \text{Woodin cardinals})_{n \in \mathbb{N}}</math> <math>\mathrm{Z}_{2} + (\mathrm{PD})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega \text{ Woodin cardinals})</math> <math>\mathrm{ZF} + (\mathrm{AD})</math> <math>\mathrm{ZFC} + (L(\mathbb{R}) \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{OD}(\mathbb{R}) \models \mathrm{AD})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\omega_1)\text{-strongly compact})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_1} \text{ is } \omega_1\text{-dense})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\mathbb{R})\text{-strongly compact})</math> <math>\mathrm{ZF} + \mathrm{DC} + (\mathrm{AD}_{\mathbb{R}})</math>
* <math>\mathrm{ZFC} + \text{(there is a superstrong cardinal)}</math>
* <math>\mathrm{ZFC} + \text{(there is a subcompact cardinal)}</math> <math>\mathrm{ZFC} + (V = L[\vec{E}]) + \exists\kappa(\neg\square_{\kappa})</math>
* <math>\mathrm{ZFC} + \text{(there is a strongly compact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Proper Forcing Axiom)}</math>
* <math>\mathrm{ZFC} + \text{(there is a supercompact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Martin's Maximum)}</math>
* <math>\mathrm{ZFC} + \forall n \text{(there is a proper class of } C^{(n)}\text{-extendible cardinals)}</math> <math>\mathrm{ZFC} + \text{(Vopěnka's Principle)}</math>
* <math>\mathrm{ZFC} + \text{(there is a high-jump cardinal)}</math>
* <math>\mathrm{HUGE} = \mathrm{ZFC} + \text{( there is a } n\text{-huge cardinal )}_{n\in\mathbb{N}}</math>
* <math>\mathrm{ZFC} + \text{(Wholeness Axiom } \mathrm{WA}_n)</math>
* <math>\mathrm{ZFC} + \mathrm{I}3 = \mathrm{ZFC} + \exists\lambda(E_0(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}2 = \mathrm{ZFC} + \exists\lambda(E_1(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}1 = \mathrm{ZFC} + \exists\lambda(E_{\omega}(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}0</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \exists\lambda\exists j : V_{\lambda + 2} \prec_{\Sigma_{\omega}^{\mathrm{set}}} V_{\lambda + 2}</math>
* <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math>

[[分类:集合论相关]]

证明论序数

2025-09-16T17:07:47Z

QuantumJack1：/* 证明论序数表 */ BMS分析

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

=== 定义和性质 ===
对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（<math>|T|</math> 或 <math>\text{PTO}(T)</math>）定义为能用超限归纳证明的原始递归良序的序型最大值。

证明论序数满足：

# 对任意递归序数 <math>\beta<|T|</math>，理论 <math>T</math> 能证明“所有序数小于 <math>\beta</math> 的原始递归良序关系都是良序的”；对 <math>\alpha=|T|</math>，理论 <math>T</math> 无法证明“所有序数小于 <math>\alpha</math> 的原始递归良序关系都是良序的”。
# 存在一种递归记号系统，自然表示所有小于 <math>|T|</math> 的序数；理论 <math>T</math> 能通过超限归纳（序数是良序集的序型，满足超限归纳原理：<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\nvdash\perp</math>）；理论 <math>T</math> 能证明所有初等递归函数在小于 <math>|T|</math> 的序数上总停止；对任意递归序数 <math>\beta<|T|</math>，至少不满足上述条件中的一条。
# 证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序。

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

ZFC 相关证明论序数：

* <math>\mathrm{S}_0 = (\mathrm{Ext}) + (\mathrm{Null}) + (\mathrm{Pair}) + (\mathrm{Union}) + (\mathrm{Diff})\ (\text{Rudimentary set theory})</math>
* <math>\mathrm{S}_1 = \mathrm{S}_0 + (\mathrm{Powerset})</math>
* <math>\mathrm{M}_0 = \mathrm{S}_1 + (\Delta_0^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{M}_1 = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Transitive\ Containment})</math>
* <math>\mathrm{KP}^- = \mathrm{S}_0 + (\mathrm{Infinity}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP}^{-\infty} = \mathrm{S}_0 + (\mathrm{Foundation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
* <math>\mathrm{KP} = \mathrm{KP}^{-\infty} + (\mathrm{Infinity}) = \mathrm{KP}^- + (\mathrm{Foundation})</math>
* <math>\mathrm{KPl} = \mathrm{KP} + (\text{universe limit of admissible sets})</math>
* <math>\mathrm{KPi} = \mathrm{KP} + (\text{recursively inaccessible universe})</math>
* <math>\mathrm{KPh} = \mathrm{KP} + (\text{recursively hyperinaccessible universe})</math>
* <math>\mathrm{KPM} = \mathrm{KP} + (\text{recursively Mahlo universe})</math>
* <math>\mathrm{ZBQC} = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\mathrm{Choice})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{MAC} = \mathrm{M}_1 + (\mathrm{Infinity}) + (\mathrm{Choice}) = \mathrm{ZBQC} + (\text{Transitive Containment})</math>
* <math>\mathrm{MOST} = \mathrm{MAC} + (\Delta_0^{\mathrm{set}} - \mathrm{Collection}) = \mathrm{ZBQC} + \mathrm{KP} + (\Sigma_1^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{Z} = \mathrm{S}_1 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\Sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{ZC} = \mathrm{Z} + (\mathrm{Choice}) = \mathrm{ZBQC} + (\sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
* <math>\mathrm{MAC} + \forall m (\beth_{\beth_{m}}\text{ exists})</math> <math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
* <math>\mathrm{Z} + (\Pi_2^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{NFU}^* = \mathrm{NFU} + (\mathrm{Counting}) + (\mathrm{Strongly\ Cantorian\ Separation})</math>
* <math>\mathrm{Z} + (\Pi_m^{\mathrm{set}} - \mathrm{Replacement})</math>
* <math>\mathrm{ZF} = \mathrm{Z} + (\Pi_\omega^{\mathrm{set}} - \mathrm{Replacement})</math> <math>\mathrm{AST}</math> <math>\mathrm{GB}</math>
* <math>\mathrm{ZFC} = \mathrm{ZF} + (\text{Choice})</math> <math>\mathrm{NBG} = \mathrm{GBC} = \mathrm{GB} + (\text{Global Choice})</math>
* <math>\mathrm{ZFC} + (\text{there is a worldly cardinal})</math>
* <math>\mathrm{NBG} + (\text{there is a stationary proper class of worldly cardinals})</math>
* <math>\mathrm{NBG} + (\text{Class Forcing Theorem})</math> <math>\mathrm{NBG} + (\text{Clopen Class Game Determinacy})</math>
* <math>\mathrm{MK} = \mathrm{NBG} + (\Pi_{\infty}^{\mathrm{class}} - \mathrm{CA})</math>
* <math>\mathrm{ZFC} + (\text{there is an inaccessible cardinal})</math> <math>\mathrm{ZFC} + (\Pi_{1}^{1}\ \text{Perfect Set Property})</math> <math>\mathrm{ZFC} + (\Sigma_{3}^{1}\ \text{Lebesgue measurability})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega\ \text{inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\forall\alpha(\omega \leq \alpha \leq \aleph_{\omega} \Rightarrow |\mathrm{V}_{\alpha} \cap L| = |\alpha|))</math>
* <math>\mathrm{ZFC} + (\text{there is a proper class of inaccessible cardinals})</math> <math>\mathrm{ZFC} + (\text{Grothendieck Universe Axiom})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \Sigma_{n}^{\mathrm{set}}\text{-reflecting cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a } \sigma_{\omega}^{\mathrm{set}}\text{-reflecting cardinal})</math> <math>\mathrm{ZFC} + (\text{Ord is Mahlo})</math>
* <math>\mathrm{ZFC} + (\text{there is an uplifting cardinal})</math> <math>\mathrm{ZFC} + (\text{Resurrection Axioms})</math>
* <math>\mathrm{ZFC} + (\text{there is a Mahlo cardinal})</math>
* <math>\mathrm{SMAH} = \mathrm{ZFC} + (\text{there is a } n\text{-Mahlo cardinal})_{n\in\mathbb{N}}</math> <math>\mathrm{NFUA} = \mathrm{NFU} + (\text{Infinity}) + (\text{Cantorian Sets})</math>
* <math>\mathrm{SMAH}^{+} = \mathrm{ZFC} + \forall n(\text{there is a } n\text{-Mahlo cardinal})</math>
* <math>\mathrm{MK} + (\text{Ord is weakly compact})</math> <math>\mathrm{GPK}_{\infty}^{+} = \mathrm{GPK}^{+} + (\text{Infinity})</math> <math>\mathrm{NFUB} =\mathrm{NFU} +(\text{Infinity}) + (\text{Cantorian Sets}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFC} + (\text{there is a weakly compact cardinal})</math> <math>\mathrm{ZFC} + (\omega_{2}\ \text{has the tree property})</math>
* <math>\mathrm{ZFC} + (\text{there is a totally indescribable cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is a subtle cardinal})</math>
* <math>\mathrm{ZFC} + (\text{there is an ineffable cardinal})</math>
* <math>\mathrm{ZFC} + \forall\alpha(\alpha < \omega_{1} \Rightarrow \text{there is a } \alpha\text{-Erdős cardinal})</math>
* <math>\mathrm{ZFC} + (0^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (L \models \aleph_{\omega}\ \text{is regular})</math> <math>\mathrm{ZFC} + \forall \alpha (\alpha \geq \omega \Longrightarrow |V_{\alpha} \cap L| = |\alpha|)</math> <math>\mathrm{ZFC} + (\text{parameter-free } \Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x \in \mathbb{R} \Longrightarrow x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{1}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + \forall x\ (x^{\sharp}\ \text{exists})</math> <math>\mathrm{ZFC} + (\Sigma_{2}^{1}\ \text{universal Baireness})</math>
* <math>\mathrm{ZFC} + (\text{there is an } \omega_{1}\text{-Erdős cardinal})</math> <math>\mathrm{ZFC} + (\text{Chang's Conjecture})</math>
* <math>\mathrm{SRP} = \mathrm{ZFC} + (\text{there is cardinal with the } n\text{-stationary Ramsey property})_{n \in \mathbb{N}}</math>
* <math>\mathrm{SRP}^{+} = \mathrm{ZFC} + \forall n\ (\text{there is a cardinal with the } n\text{-stationary Ramsey property})</math>
* <math>\mathrm{MK} + (\text{Ord is measurable})</math> <math>\mathrm{NFUM} = \mathrm{NFU} + (\text{Infinity}) + (\text{Large Ordinals}) + (\text{Small Ordinals})</math>
* <math>\mathrm{ZFM} = \mathrm{ZFC} + (\text{there is a measurable cardinal})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is precipitous})</math> <math>\mathrm{ZF} + (\omega_{1}\ \text{is measurable})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = 2)</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{2}}\ \text{is precipitous})</math>
* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = \kappa^{++})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{ZFC} + (2^{\aleph_{\omega}} = \aleph_{\omega + 2})</math>
* <math>\mathrm{ZFC} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{2} + (\Delta_{2}^{1}\text{-determinacy})\ (\text{conjectural})</math>
* <math>\mathrm{MK} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\text{lightface } \Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{NBG} + (\text{Ord is Woodin})</math> <math>\mathrm{ZFC} + \neg \mathrm{SCH}</math> <math>\mathrm{Z}_{3}+ (\Delta_{2}^{1}\text{-determinacy})</math>
* <math>\mathrm{ZFC} + (\text{there is a Woodin cardinal})</math> <math>\mathrm{ZFC} + (\Delta_{2}^{1}\text{-determinacy})</math> <math>\mathrm{ZFC} + (\mathrm{OD} \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is } \omega_{2}\text{-saturated})</math>
* <math>\mathrm{ZFC} + (\text{there are } n\ \text{Woodin cardinals})_{n \in \mathbb{N}}</math> <math>\mathrm{Z}_{2} + (\mathrm{PD})</math>
* <math>\mathrm{ZFC} + (\text{there are } \omega \text{ Woodin cardinals})</math> <math>\mathrm{ZF} + (\mathrm{AD})</math> <math>\mathrm{ZFC} + (L(\mathbb{R}) \models \mathrm{AD})</math> <math>\mathrm{ZFC} + (\mathrm{OD}(\mathbb{R}) \models \mathrm{AD})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\omega_1)\text{-strongly compact})</math> <math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_1} \text{ is } \omega_1\text{-dense})</math>
* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\mathbb{R})\text{-strongly compact})</math> <math>\mathrm{ZF} + \mathrm{DC} + (\mathrm{AD}_{\mathbb{R}})</math>
* <math>\mathrm{ZFC} + \text{(there is a superstrong cardinal)}</math>
* <math>\mathrm{ZFC} + \text{(there is a subcompact cardinal)}</math> <math>\mathrm{ZFC} + (V = L[\vec{E}]) + \exists\kappa(\neg\square_{\kappa})</math>
* <math>\mathrm{ZFC} + \text{(there is a strongly compact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Proper Forcing Axiom)}</math>
* <math>\mathrm{ZFC} + \text{(there is a supercompact cardinal)}</math> <math>\mathrm{ZFC} + \text{(Martin's Maximum)}</math>
* <math>\mathrm{ZFC} + \forall n \text{(there is a proper class of } C^{(n)}\text{-extendible cardinals)}</math> <math>\mathrm{ZFC} + \text{(Vopěnka's Principle)}</math>
* <math>\mathrm{ZFC} + \text{(there is a high-jump cardinal)}</math>
* <math>\mathrm{HUGE} = \mathrm{ZFC} + \text{( there is a } n\text{-huge cardinal )}_{n\in\mathbb{N}}</math>
* <math>\mathrm{ZFC} + \text{(Wholeness Axiom } \mathrm{WA}_n)</math>
* <math>\mathrm{ZFC} + \mathrm{I}3 = \mathrm{ZFC} + \exists\lambda(E_0(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}2 = \mathrm{ZFC} + \exists\lambda(E_1(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}1 = \mathrm{ZFC} + \exists\lambda(E_{\omega}(\lambda))</math>
* <math>\mathrm{ZFC} + \mathrm{I}0</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \exists\lambda\exists j : V_{\lambda + 2} \prec_{\Sigma_{\omega}^{\mathrm{set}}} V_{\lambda + 2}</math>
* <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math>
* <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math>

[[分类:集合论相关]]

序数超运算

2025-09-16T16:38:50Z

QuantumJack1：+1法超运算分析

序数超运算是对序数使用[[超运算序列|超运算]]的尝试。它虽然是最直观、新人最容易想到的模式，但已经被长期的[[googology]]实践所证明是低效、难以扩展的。

== 原定义 ==
首先，我们仿照[[高德纳箭头]]在自然数上的定义和[[序数#序数的运算|序数运算]]的定义，给出序数使用高德纳箭头的定义：

# <math>\alpha\uparrow^1\beta=\alpha^{\beta}</math>
# <math>\alpha\uparrow^c1=\alpha</math>
# <math>\alpha\uparrow^{c+1}(\beta+1)=\alpha\uparrow^c(\alpha\uparrow^{c+1}\beta)</math>
# <math>\alpha\uparrow^c\lambda=sup\{\alpha\uparrow^c\beta|\beta<\lambda\}</math>

其中<math>\alpha,\beta</math>是任意序数，c是自然数，<math>\lambda</math>是非0极限序数。

这样一来，就有<math>\omega\uparrow^2(\omega+1)=\omega^{\omega\uparrow^2\omega}=sup\{\omega^{\omega\uparrow^2n}|n<\omega\}=sup\{\omega\uparrow^2n|n<\omega\}=\omega\uparrow^2\omega</math>.进一步，对任意<math>\beta\geq\omega</math>，都有<math>\omega\uparrow^2\beta=\omega\uparrow^2\omega</math>.再进一步，对任意的<math>c\geq2,\beta\geq\omega</math>,都有<math>\omega\uparrow^c\beta=\omega\uparrow^2\omega</math>.

这显然不是我们所期待的。

== 左结合法 ==
第一种试图解决问题的方案是左结合法。它借鉴了[[下箭号表示法|下箭头表示法]]，给出序数使用下箭头的定义：

# <math>\alpha\downarrow^1\beta=\alpha^{\beta}</math>
# <math>\alpha\downarrow^c1=\alpha</math>
# <math>\alpha\downarrow^{c+1}(\beta+1)=(\alpha\downarrow^{c+1}\beta)\downarrow\alpha</math>
# <math>\alpha\downarrow^c\lambda=sup\{\alpha\downarrow^c\beta|\beta<\lambda\}</math>

其中<math>\alpha,\beta</math>是任意序数，c是自然数，<math>\lambda</math>是非0极限序数。

于是有：

<math>\omega\downarrow^22=\omega^\omega
</math>

<math>\omega\downarrow^23=\omega^{\omega^2}</math>

<math>\omega\downarrow^2\omega=\omega^{\omega^\omega}</math>

<math>(\omega\downarrow^2\omega)\downarrow^22=\omega^{\omega^{\omega^\omega}}</math>

<math>\omega\downarrow^33=\omega^{\omega^{\omega^{\omega^\omega}}}</math>

<math>\omega\downarrow^34=\omega^{\omega^{\omega^{\omega^{\omega^{\omega^\omega}}}}}</math>

<math>\omega\downarrow^3\omega=\varepsilon_0</math>

<math>(\omega\downarrow^3\omega)\downarrow^22=\varepsilon_0^{\varepsilon_0}</math>

<math>(\omega\downarrow^3\omega)\downarrow^2\omega=\varepsilon_0^{\varepsilon_0^\omega}</math>

<math>(\omega\downarrow^3\omega)\downarrow^32=\varepsilon_0^{\varepsilon_0^{\varepsilon_0}}</math>

<math>(\omega\downarrow^3\omega)\downarrow^33=\varepsilon_0^{\varepsilon_0^{\varepsilon_0^{\varepsilon_0^{\varepsilon_0}}}}</math>

<math>\omega\downarrow^43=\varepsilon_1</math>

<math>\omega\downarrow^44=\varepsilon_2</math>

<math>\omega\downarrow^4\omega=\varepsilon_\omega</math>

<math>(\omega\downarrow^4\omega)\downarrow^3\omega=\varepsilon_{\omega+1}</math>

<math>(\omega\downarrow^4\omega)\downarrow^42=\varepsilon_{\varepsilon_\omega}</math>

<math>(\omega\downarrow^4\omega)\downarrow^43=\varepsilon_{\varepsilon_\omega2}</math>

<math>\omega\downarrow^53=\varepsilon_{\varepsilon_\omega\omega}</math>

<math>\omega\downarrow^54=\varepsilon_{\varepsilon_{\varepsilon_\omega\omega}\omega}</math>

<math>\omega\downarrow^5\omega=\zeta_0</math>

<math>\omega\downarrow^6\omega=\zeta_\omega</math>

<math>\omega\downarrow^7\omega=\varphi(3,0)</math>

<math>\omega\downarrow^{1+2n}\omega=\varphi(n,0)</math>

把下箭头用到序数上，其极限为<math>\varphi(\omega,0)</math>，也符合箭头运算的强度。

但是，左结合的下箭头行为和高德纳箭头差异还是不小，而且两个箭头对应一个<math>\varphi(n,0)</math>还是不太符合我们的预期。

== 攀爬法 ==
第二种试图解决问题的方案是攀爬法。攀爬法提供了一种更强的推广。我们知道，<math>\varepsilon_1</math>的基本列是<math>\{\omega^{\varepsilon_0+1},\omega^{\omega^{\varepsilon_0+1}},\omega^{\omega^{\omega^{\varepsilon_0+1}}},\cdots\}</math>，我们可以将其表示为<math>\{\omega^{\omega^{\omega^{\cdots}}}+1,\omega^{\omega^{\omega^{\cdots}}+1},\omega^{\omega^{\omega^{\cdots}+1}},\cdots\}</math>.在这里我们把<math>\omega</math>的指数塔固定在<math>\omega</math>。在这样的基本列中，+1像在指数塔攀爬一样，攀爬法也因此而得名。在基本列的尽头，+1攀爬到了指数塔的顶端，与原来在顶端的1相加变为2。因此我们得到<math>\varepsilon_1=\underbrace{\omega^{\omega^{\cdots^{2}}}}_{\omega+1 layers}</math>.进一步的，按照攀爬法我们有<math>\varepsilon_{\omega}=\underbrace{\omega^{\omega^{\cdots^{\omega}}}}_{\omega+1 layers}</math>,我们将其记为<math>\omega\uparrow\uparrow(\omega+1)=\varepsilon_{\omega}</math>.

进一步有：

<math>\omega\uparrow\uparrow(\omega+2)=\varepsilon_{\omega^{\omega}}</math>

<math>\omega\uparrow\uparrow(\omega\times2)=\varepsilon_{\varepsilon_0}</math>

<math>\omega\uparrow\uparrow(\omega^2)=\zeta_0</math>

<math>\omega\uparrow\uparrow(\omega^3)=\eta_0</math>

<math>\omega\uparrow\uparrow(\omega^{\omega})=\varphi(\omega,0)</math>

<math>\omega\uparrow\uparrow\omega\uparrow\uparrow\omega=\varphi(\varphi(1,0),0)</math>

<math>\omega\uparrow^34=\varphi(\varphi(\varphi(1,0),0),0)</math>

<math>\omega\uparrow^3\omega=\varphi(1,0,0)</math>

<math>\omega\uparrow^3(\omega+1)=\varphi(1,0,1)</math>

<math>\omega\uparrow^3(\omega^2)=\varphi(1,1,0)</math>

<math>\omega\uparrow^3\omega\uparrow^3\omega=\varphi(1,\varphi(1,0,0),0)</math>

<math>\omega\uparrow^44=\varphi(1,\varphi(1,\varphi(1,0,0),0),0)</math>

<math>\omega\uparrow^4\omega=\varphi(2,0,0)</math>

<math>\omega\uparrow^5\omega=\varphi(3,0,0)</math>

<math>\omega\uparrow^{\omega}\omega=\varphi(\omega,0,0)</math>

由此我们得到了攀爬法序数超运算的极限是<math>\varphi(\omega,0,0)</math>.

但是现在已经证明了，攀爬法是非良序的。因此这一做法得到的推广是不可靠的。

== +1法 ==
第三中试图解决问题的方案是+1法。

它基于一种特别朴素的想法，即：如果<math>\omega\uparrow^c\alpha=\alpha</math>,则修改其值为<math>\omega\uparrow^c(\alpha+1)</math>.显然，这一改变真正起到效果的是指数上的变化。关于+1法序数超运算，我们有：

例如：ω^^(ω+1)如果展开为ω^ω^^ω就会遇到不动点，因此触发上述的+1规则。

<math>\omega\uparrow\uparrow(\omega+1)=\omega^{\omega\uparrow\uparrow\omega+1}=\omega^{\varepsilon_0+1}</math>

然后，以此类推：

<math>\omega\uparrow\uparrow(\omega+2)=\omega^{\omega^{\varepsilon_0+1}}</math>

<math>\omega\uparrow\uparrow(\omega2)=\varepsilon_1</math>

<math>\omega\uparrow\uparrow(\omega3)=\varepsilon_2</math>

<math>\omega\uparrow\uparrow(\omega^2)=\varepsilon_{\omega}</math>

<math>\omega\uparrow^33=\omega\uparrow\uparrow\omega\uparrow\uparrow\omega=\varepsilon_{\varepsilon_0}</math>

<math>\omega\uparrow^3\omega=\zeta_0</math>

到ζ_0后，+1法的展开方式将会比较复杂，并产生一些奇特的基础序列。继续分析：

<math>\omega\uparrow^3(\omega+1)=\omega\uparrow\uparrow(\omega\uparrow^3\omega+1)
=\omega\uparrow(\omega\uparrow\uparrow(\omega\uparrow^3\omega)+1)
=\omega\uparrow(\omega\uparrow^3\omega+1)
=\omega^{\zeta_0+1}</math>

<math>\omega\uparrow\uparrow(\omega\uparrow^3\omega+\omega)=\varepsilon_{\zeta_0+1}</math>

<math>\omega\uparrow\uparrow(\omega\uparrow^3\omega*2)=\varepsilon_{\zeta_02}</math>

<math>\omega\uparrow^3(\omega+2)=\omega\uparrow\uparrow(\omega\uparrow^3(\omega+1))=\varepsilon_{\omega^{\zeta_0+1}}</math>

<math>\omega\uparrow^3(\omega+3)=\varepsilon_{\varepsilon_{\omega^{\zeta_0+1}}}</math>

<math>\omega\uparrow^3(\omega2)=\zeta_1</math>

<math>\omega\uparrow^43=\zeta_{\zeta_0}</math>

<math>\omega\uparrow^4\omega=\eta_0</math>

<math>\omega\uparrow^4(\omega+1)=\omega\uparrow^3(\omega\uparrow^4\omega+1)
=\omega\uparrow\omega\uparrow\uparrow\omega\uparrow^3(\omega\uparrow^4\omega+1)
=\omega\uparrow(\omega\uparrow^4\omega+1)
=\omega^{\eta_0+1}</math>

<math>\omega\uparrow^4(\omega+2)=\omega\uparrow^3(\omega\uparrow^4(\omega+1))=\zeta_{\omega^{\eta_0+1}}</math>

<math>\omega\uparrow^4(\omega2)=\eta_1</math>

<math>\omega\uparrow^5\omega=\varphi(4,0)</math>

<math>\omega\uparrow^{\omega}\omega=\varphi(\omega,0)</math>

于是我们得到其极限为<math>\varphi(\omega,0)</math>。它的优点是它和<math>\varphi</math>函数行为完全一致。但缺点也是这个。这导致了<math>\omega\uparrow\uparrow(\omega+1)=(\omega\uparrow\uparrow\omega)\times\omega</math>这种奇异的结果，某种意义上丢失了超运算自己的特性。因此可以说，+1法序数超运算被<math>\varphi</math>函数上位替代了。+1法序数超运算还可以继续拓展，在某些版本中，其增长率与类似的Veblen 函数及Feferman序数折叠函数类似，例如：

<math>\omega\{\omega\}(\omega2)=\varphi(\omega,1)</math>

<math>\omega\{\omega+1\}\omega=\varphi(\omega+1,0)</math>

<math>\omega\{\omega\uparrow\uparrow\omega\}\omega=\varphi(\varepsilon_0,0)</math>

<math>\omega\{\Omega\}3=\omega\{\omega\{\omega\}\omega\}\omega=\varphi(\varphi(\omega,0),0)</math>

<math>\omega\{\Omega\}\omega=\Gamma_0</math>

<math>\omega\{\Omega+1\}\omega=\varphi(1,1,0)</math>

<math>\omega\{\Omega2\}\omega=\varphi(2,0,0)</math>

<math>\omega\{\Omega^2\}\omega=\varphi(1,0,0,0)</math>

<math>\omega\{\Omega^\omega\}\omega=\psi(\Omega^{\Omega^\omega})</math>

<math>\omega\{\Omega^\Omega\}\omega=\psi(\Omega^{\Omega^\Omega})</math>

<math>\omega\{\Omega\uparrow\uparrow\omega\}\omega=\psi(\Omega_2)</math>

但如此的拓展达到同样序数的难度要明显大于一般的[[序数坍缩函数]]。有些版本引入了更为强大的结构，但已经失去了超运算的特性，其强度主要为引入的更高级序数结构，建议使用以更高级核心的序数记号替代之。

== 总结 ==
到目前为止，序数超运算不是不良定义，就是不理想的。我们不建议在任何地方使用高于<math>\varepsilon_0</math>的序数超运算和更高级别的运算。如果要使用，必须仅仅将它作为形式上的符号，并且明确地说明其具体含义。事实上，我们完全可以使用[[Veblen 函数]]这样的更加强大且清晰的[[序数记号]]来替代它。
[[分类:记号]]
[[分类:入门]]