证明论序数

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

证明论序数表

证明论序数	算术论体系	集合论体系	其他体系
-	$Q$	$\mathrm{K}{\mathrm{P}}^{\mathrm{-}}$
${\omega }^2$	$\mathrm{R}\mathrm{F}\mathrm{A}$ $\mathrm{I}{\mathrm{\Delta }}_{\mathrm{0}}$
${\omega }^3$	$\mathrm{R}\mathrm{C}{A}_{\mathrm{0}}^{\mathrm{*}}$ $\mathrm{W}\mathrm{K}{L}_{\mathrm{0}}^{\mathrm{*}}$ $\mathrm{I}{\mathrm{\Delta }}_{\mathrm{0}}\mathrm{+}\mathrm{e}\mathrm{x}\mathrm{p}$
${\omega }^n$	$\mathrm{I}{\mathrm{\Delta }}_{\mathrm{0}}+{{ℰ}}_n\text{ is total}$
${\omega }^{\omega }$	$\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}$ $\mathrm{W}\mathrm{K}{\mathrm{L}}_{\mathrm{0}}$ $\mathrm{P}\mathrm{R}\mathrm{A}$ $\mathrm{R}\mathrm{C}{A}_{\mathrm{0}}^{\mathrm{2}}$	$\mathrm{C}\mathrm{P}\mathrm{R}\mathrm{C}$ $\mathrm{K}{\mathrm{P}}^{\mathrm{-}}\mathrm{+}{\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{s}\mathrm{e}\mathrm{t}}\mathrm{F}\mathrm{o}\mathrm{n}\mathrm{d}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{+}\mathrm{I}\mathrm{N}\mathrm{D}$
${\omega }^{{\omega }^{{\omega }^{\omega }}}$	$\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}\mathrm{(}{\mathrm{\Pi }}_{\mathrm{2}}^{\mathrm{0}}{\mathrm{)}}^{\mathrm{-}}\mathrm{-}\mathrm{I}\mathrm{N}\mathrm{D}$
$\omega \uparrow \uparrow (n+2)$	$\mathrm{I}{\mathrm{\Sigma }}_{n+1}$
${\epsilon }_0$	$\mathrm{P}\mathrm{A}$ $\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}$ ${\mathrm{\Delta }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}$ ${\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{A}{\mathrm{C}}_{\mathrm{0}}$	$\mathrm{K}{\mathrm{P}}^{\mathrm{-}\mathrm{\infty }}$	$\mathrm{E}{\mathrm{M}}_{\mathrm{0}}$
${\epsilon }_1$	$\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}\mathrm{K}\mathrm{P}\mathrm{H}\mathrm{T}$
${\epsilon }_{\omega }$	$\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}\mathrm{i}\mathrm{R}\mathrm{T}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}+\mathrm{\forall }Y\mathrm{\forall }n\mathrm{\exists }X(\mathrm{T}\mathrm{J}(n,X,Y))$
${\epsilon }_{{\epsilon }_0}$	$\mathrm{A}\mathrm{C}\mathrm{A}$ ${\mathrm{F}\mathrm{P}}_n-\mathrm{A}\mathrm{C}\mathrm{A}{\mathrm{\text{'}}}_{\mathrm{0}}$ ${\mathrm{F}\mathrm{P}}_n-\mathrm{A}\mathrm{C}{\mathrm{A}}^{\prime }$
${\zeta }_0$	$\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}+\mathrm{\forall }X\mathrm{\exists }Y(\mathrm{T}\mathrm{J}(\omega ,X,Y))$ $\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}\mathrm{(}\mathrm{B}\mathrm{R}\mathrm{)}$ ${\mathrm{p}}_{\mathrm{1}}\mathrm{(}\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{)}$
$\phi (2,{\epsilon }_0)$	$\mathrm{A}\mathrm{C}\mathrm{A}+\mathrm{\forall }X\mathrm{\exists }Y(\mathrm{T}\mathrm{J}(\omega ,X,Y))$ $\mathrm{R}\mathrm{F}\mathrm{N}$
$\phi (\omega ,0)$	${\mathrm{\Delta }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}\mathrm{R}$ $\mathrm{R}\mathrm{C}{A}_{\mathrm{0}}^{\mathrm{*}}\mathrm{+}{\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}{\mathrm{A}}^{\mathrm{-}}$ ${\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{D}{\mathrm{C}}_{\mathrm{0}}$		$\mathrm{I}{D}_{\mathrm{1}}^{\mathrm{\#}}$ $\mathrm{E}{\mathrm{M}}_{\mathrm{0}}\mathrm{+}\mathrm{J}\mathrm{R}$ $\mathrm{P}\mathrm{I}\mathrm{D}$ $\mathrm{A}\mathrm{c}\mathrm{c}\mathrm{-}\mathrm{I}\mathrm{D}\mathrm{(}\mathrm{A}\mathrm{c}\mathrm{c}\mathrm{)}$ $\mathrm{(}{\mathrm{\Pi }}_{\mathrm{0}}^{\mathrm{0}}\mathrm{(}\mathrm{P}\mathrm{)},\mathrm{P}\mathrm{\cup }\mathrm{N}\mathrm{)}\mathrm{-}\mathrm{I}\mathrm{D}$ $\mathrm{(}{\mathrm{\Pi }}_{\mathrm{0}}^{\mathrm{0}}\mathrm{(}\mathrm{P}\mathrm{)},\mathrm{P}\mathrm{\wedge }\mathrm{N}\mathrm{)}\mathrm{-}\mathrm{I}\mathrm{D}\mathrm{(}\mathrm{A}\mathrm{c}\mathrm{c}\mathrm{)}$
$\phi (\nu +1,0)$	$\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}+\mathrm{\forall }X\mathrm{\exists }Y(\mathrm{T}\mathrm{J}({\omega }^{\nu },X,Y))$
$\psi ({\mathrm{\Omega }}^{{\epsilon }_0})$	${\mathrm{\Delta }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}\mathrm{A}$ ${\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{A}\mathrm{C}$ ${\mathrm{(}{\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{C}\mathrm{A}\mathrm{)}}_{<{\mathrm{\epsilon }}_{\mathrm{0}}}$
$\psi ({\mathrm{\Omega }}^{\psi ({\mathrm{\Omega }}^{\omega })})$		$\mathrm{P}\mathrm{R}\mathrm{S}\mathrm{\omega }$
${\mathrm{\Gamma }}_0$	$\mathrm{A}\mathrm{T}{\mathrm{R}}_{\mathrm{0}}$ ${\mathrm{\Delta }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}\mathrm{A}\mathrm{+}\mathrm{B}\mathrm{R}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{R}\mathrm{T}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Delta }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{R}\mathrm{T}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{d}\mathrm{e}\mathrm{t}\mathrm{.}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Delta }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{d}\mathrm{e}\mathrm{t}\mathrm{.}$ $\mathrm{F}{\mathrm{P}}_{\mathrm{0}}$	$\mathrm{K}\mathrm{P}{\mathrm{i}}^{\mathrm{-}}$ $\mathrm{C}\mathrm{Z}{\mathrm{F}}^{\mathrm{-}}\mathrm{+}\mathrm{I}\mathrm{N}\mathrm{A}\mathrm{C}$	${\widehat{\mathrm{I}\mathrm{D}}}_{<\omega }$ ${\widehat{\mathrm{I}\mathrm{D}}}^{*}$ ${\mathrm{M}\mathrm{L}}_{<\omega }$ $\mathrm{M}\mathrm{L}\mathrm{U}$ $\mathrm{U}\mathrm{(}\mathrm{P}\mathrm{A}\mathrm{)}$