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

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

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

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

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

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

证明论序数满足：

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

=== 证明论序数表 ===
{| class="wikitable class="article-table" border="0" cellpadding="1" cellspacing="1""
! scope="col" |证明论序数
! scope="col" |算术论体系
! scope="col" |集合论体系
! scope="col" |其他体系
|-
| -
|<math>Q</math>
|<math>\rm KP^-</math>
|
|-
|<math>\omega^2</math>
|<math>\rm RFA</math><br><math>\rm I\Delta_0</math>
|
|
|-
|<math>\omega^3</math>
|<math>\rm RCA_0^*</math><br><math>\rm WKL_0^*</math><br><math>\rm I\Delta_0+exp</math>
|
|
|-
|<math>\omega^n</math>
|<math>{\rm I\Delta_0}+\mathcal{E}_n\text{ is total}</math>
|
|
|-
|<math>\omega^\omega</math>
|<math>\rm RCA_0</math><br><math>\rm WKL_0</math><br><math>\rm PRA</math><br><math>\rm RCA_0^2</math>
|<math>\rm CPRC</math><br><math>\rm KP^-+\Pi_1^{set}\ Fondation+IND</math>
|
|-
|<math>\omega^{\omega^{\omega^\omega}}</math>
|<math>\rm RCA_0+(\Pi_2^0)^--IND</math>
|
|
|-
|<math>\omega\uparrow\uparrow(n+2)</math>
|<math>{\rm I}\Sigma_{n+1}</math>
|
|
|-
|<math>\varepsilon_0</math>
|<math>\rm PA</math><br><math>\rm ACA_0</math><br><math>\rm \Delta_1^1-CA_0</math><br><math>\rm \Sigma_1^1-AC_0</math>
|<math>\rm KP^{-\infty}</math>
|<math>\rm EM_0</math>
|-
|<math>\varepsilon_1</math>
|<math>\rm ACA_0+KPHT</math>
|
|
|-
|<math>\varepsilon_\omega</math>
|<math>\rm ACA_0+iRT</math><br><math>{\rm RCA_0}+\forall Y\forall n\exists X({\rm TJ}(n,X,Y))</math>
|
|
|-
|<math>\varepsilon_{\varepsilon_0}</math>
|<math>\rm ACA</math><br><math>{\rm FP}_n-{\rm ACA'_0}</math><br><math>{\rm FP}_n-{\rm ACA'}</math>
|
|
|-
|<math>\zeta_0</math>
|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm ACA_0+(BR)</math><br><math>\rm p_1(ACA_0)</math>
|
|
|-
|<math>\varphi(2,\varepsilon_0)</math>
|<math>{\rm ACA}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm RFN</math>
|
|
|-
|<math>\varphi(\omega,0)</math>
|<math>\rm \Delta_1^1-CR</math><br><math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm \Sigma_1^1-DC_0</math>
|
|<math>\rm ID_1^\#</math><br><math>\rm EM_0+JR</math><br><math>\rm PID</math><br><math>\rm Acc-ID(Acc)</math><br><math>\rm (\Pi_0^0(P),P\cup N)-ID</math><br><math>\rm (\Pi_0^0(P),P\land N)-ID(Acc)</math>
|-
|<math>\varphi(\nu+1,0)</math>
|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega^\nu,X,Y))</math>
|
|
|-
|<math>\psi(\Omega^{\varepsilon_0})</math>
|<math>\rm \Delta_1^1-CA</math><br><math>\rm \Sigma_1^1-AC</math><br><math>\rm{(\Pi_1^0-CA)}_{<\varepsilon_0}</math>
|
|
|-
|<math>\psi(\Omega^{\psi(\Omega^\omega)})</math>
|
|<math>\rm PRS\ \omega</math>
|
|-
|<math>\Gamma_0</math>
|<math>\rm ATR_0</math><br><math>\rm \Delta_1^1-CA+BR</math><br><math>\rm RCA_0+\Sigma_1^0-RT</math><br><math>\rm RCA_0+\Delta_1^0-RT</math><br><math>\rm RCA_0+\Sigma_1^0-det.</math><br><math>\rm RCA_0+\Delta_1^0-det.</math><br><math>\rm FP_0</math>
|<math>\rm KPi^-</math><br><math>\rm CZF^-+INAC</math>
|<math>\widehat{\rm ID}_{<\omega}</math><br><math>\widehat{\rm ID}^*</math><br><math>{\rm ML}_{<\omega}</math><br><math>\rm MLU</math><br><math>\rm U(PA)</math>
|-
|<math>\varphi(1,0,\omega^\omega)</math>
|
|<math>\rm KPl_0+(\Sigma_1-I_\omega)</math>
|
|-
|<math>\varphi(1,0,\varepsilon_0)</math>
|<math>\rm ATR</math>
|
|<math>\widehat{\rm ID}_\omega</math>
|-
|<math>\psi(\Omega^{\Omega+1})</math>
|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ATR_0})</math>
|
|
|-
|<math>\psi(\Omega^{\Omega+\omega})</math>
|<math>\rm ATR_0+\Sigma_1^1-DC</math>
|
|<math>\widehat{\rm ID}_{<\omega^\omega}</math>
|-
|<math>\psi(\Omega^{\Omega+\varepsilon_0})</math>
|<math>\rm ATR+\Sigma_1^1-DC</math>
|
|<math>\widehat{\rm ID}_{<\varepsilon_0}</math>
|-
|<math>\psi(\Omega^{\Omega+\Gamma_0})</math>
|
|
|<math>\widehat{\rm ID}_{<\Gamma_0}</math><br><math>\rm MLS</math>
|-
|<math>\varphi(2,0,0)</math>
|<math>\rm FTR_0</math>
|<math>\rm KPh^-</math>
|<math>\rm Aut(\widehat{ID})</math>
|-
|<math>\varphi(2,0,\varepsilon_0)</math>
|<math>\rm FTR</math>
|
|
|-
|<math>\varphi(2,\varepsilon_0,0)</math>
|
|<math>\rm KPh^0+(F-I_\omega)</math>
|
|-
|<math>\psi(\Omega^{\Omega\omega})</math>
|
|<math>\rm KPM^-</math>
|
|-
|<math>\varphi(\varepsilon_0,0,0)</math>
|<math>\rm \Sigma_1^1-TDC</math>
|
|
|-
|<math>\varphi(1,0,0,0)</math>
|<math>\rm p_1(\Sigma_1^1-TDC_0)</math>
|
|
|-
|<math>\psi(\Omega^{\Omega^\omega})</math>
|<math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm p_3(ACA_0)</math>
|
|<math>\rm FIT</math><br><math>\rm TID</math>
|-
|<math>\vartheta(\Omega^\Omega)</math>
|<math>\rm p_1(p_3(ACA_0))</math>
|
|
|-
|<math>\theta_{(n+2)(\Omega^\omega)}0</math>
|<math>{\rm ACA_0}+\Pi_{n+2}^1-{\rm BI}</math><br><math>\Pi_{n+1}^1-{\rm RFN}</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0^-</math>
|<math>{\rm KP}\omega^-+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math>
|
|-
|<math>\theta_{(n+2)(\Omega^\omega)}0</math>
|<math>{\rm ACA}+\Pi_{n+2}^1-{\rm BI}</math><br><math>(\Pi_{n+2}^1-{\rm BI})^-</math>
|<math>{\rm KP}\omega^-+{\rm IND}+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math>
|
|-
|<math>\psi(\psi_1(0))</math>
|<math>\rm ACA+BI</math><br><math>\rm ACA_0+\Pi_1^1-CA^-</math><br><math>\rm \Pi_1^0-FXP_0</math>
|<math>\rm KP</math><br><math>\rm KP+\Pi_2^{set}-Reflection</math><br><math>\rm KP+(BI^*)</math><br><math>\rm KP+(ATR_0^*)</math><br><math>\rm CZF</math><br><math>{\rm KP}\omega_2\upharpoonright+\Delta_1-{\rm CA}+s\Pi_1^1-{\rm ref}</math>
|<math>\rm ID_1</math><br><math>\rm ID_1^2</math><br><math>\rm ML_1\ V</math>
|-
|<math>\psi(\Omega_2)</math>
|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ACA+BI})</math>
|
|
|-
|<math>\psi(\Omega_2^{\Omega_2})</math>
|<math>\rm ATR_0^\bullet</math><br><math>\rm FP_0^\bullet</math><br><math>\rm \Sigma_1^1-DC_0^\bullet+(SUB^\bullet)</math><br><math>\rm \Sigma_1^1-AC_0^\bullet+(SUB^\bullet)</math>
|
|<math>\widehat{\rm ID}_{<\omega}^\bullet</math><math>\mathcal{U}({\rm ID_1})</math>
|-
|<math>\psi(\psi_2(0))</math>
|
|<math>\rm KP+\exists\omega_1^{CK}</math>
|<math>\rm ID_2</math><br><math>\rm ID_2^2</math>
|-
|<math>\psi(\Omega_\omega)</math>
|<math>\rm \Pi_1^1-CA_0</math><br><math>\rm \Delta_2^1-CA_0</math><br><math>\rm RCA_0+\Sigma_1^0\land\Pi_1^0-det.</math><br><math>\rm RCA_0+\Delta_2^0-RT</math>
|<math>{\rm KPl}^r</math><br><math>{\rm KPi}^r</math><br><math>{\rm KP}\beta^r</math>
|<math>{\rm ID}_{<\omega}</math><br><math>({\rm ID}_{<\omega}^2)_0</math>
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|

|}