证明论序数(或称证明论强度序数,Proof-Theoretic Ordinal)是衡量形式理论强度的核心工具,通过将理论映射到序数上,刻画其能证明的良序关系的复杂度。该概念源于希尔伯特的证明论计划,旨在通过有限方法证明数学基础理论的一致性,后由阿克曼(Wilhelm Ackermann)和根岑(Gerhard Gentzen)发展为序数分析技术。
对形式理论 T,其证明论序数 |T|ord(|T| 或 PTO(T))定义为能用超限归纳证明的原始递归良序的序型最大值。
证明论序数满足:
ZFC 相关证明论序数: