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

'''证明论序数'''（或称证明论强度序数，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>
<math>\rm I\Delta_0</math>
|
|
|-
|<math>\omega^3</math>
|<math>\rm RCA_0^*</math>
<math>\rm WKL_0^*</math>
<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>
<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>
|<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>
<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>
|<math>\rm ACA_0+KPHT</math>
|
|
|-
|<math>\varepsilon_\omega</math>
|<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>
|<math>\rm ACA</math>
<math>{\rm FP}_n-{\rm ACA'_0}</math>
<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>
<math>\rm ACA_0+(BR)</math>
<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>
<math>\rm RFN</math>
|
|
|-
|<math>\varphi(\omega,0)</math>
|<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>
|<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>
|
|<math>\rm PRS\ \omega</math>
|
|-
|<math>\Gamma_0</math>
|<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>
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|
|-
|
|
|
|

|}