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

'''证明论序数'''（或称证明论强度序数，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），即存在递归关系定义其良序