证明论序数

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

定义和性质

序数是良序集的序型，满足超限归纳原理：$\mathrm{\forall }\alpha (\mathrm{\forall }\beta <\alpha (P(\beta )\Rightarrow P(\alpha ))\Rightarrow \mathrm{\forall }\alpha P(\alpha ))$，其中 $P$ 是任意性质。

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

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

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

证明论序数满足：

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