证明论序数

证明论序数（或称证明论强度序数，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{)}$
$\phi (1,0,{\omega }^{\omega })$		$\mathrm{K}\mathrm{P}{\mathrm{l}}_{\mathrm{0}}\mathrm{+}\mathrm{(}{\mathrm{\Sigma }}_{\mathrm{1}}\mathrm{-}{\mathrm{I}}_{\mathrm{\omega }}\mathrm{)}$
$\phi (1,0,{\epsilon }_0)$	$\mathrm{A}\mathrm{T}\mathrm{R}$		${\widehat{\mathrm{I}\mathrm{D}}}_{\omega }$
$\psi ({\mathrm{\Omega }}^{\mathrm{\Omega }+1})$	$\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}+\mathrm{\forall }X\mathrm{\exists }M(X\in M\wedge M{\models }_{\omega }\mathrm{A}\mathrm{T}{\mathrm{R}}_{\mathrm{0}})$
$\psi ({\mathrm{\Omega }}^{\mathrm{\Omega }+\omega })$	$\mathrm{A}\mathrm{T}{\mathrm{R}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{D}\mathrm{C}$		${\widehat{\mathrm{I}\mathrm{D}}}_{<{\omega }^{\omega }}$
$\psi ({\mathrm{\Omega }}^{\mathrm{\Omega }+{\epsilon }_0})$	$\mathrm{A}\mathrm{T}\mathrm{R}\mathrm{+}{\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{D}\mathrm{C}$		${\widehat{\mathrm{I}\mathrm{D}}}_{<{\epsilon }_0}$
$\psi ({\mathrm{\Omega }}^{\mathrm{\Omega }+{\mathrm{\Gamma }}_0})$			${\widehat{\mathrm{I}\mathrm{D}}}_{<{\mathrm{\Gamma }}_0}$ $\mathrm{M}\mathrm{L}\mathrm{S}$
$\phi (2,0,0)$	$\mathrm{F}\mathrm{T}{\mathrm{R}}_{\mathrm{0}}$	$\mathrm{K}\mathrm{P}{\mathrm{h}}^{\mathrm{-}}$	$\mathrm{A}\mathrm{u}\mathrm{t}\mathrm{(}\widehat{\mathrm{I}\mathrm{D}}\mathrm{)}$
$\phi (2,0,{\epsilon }_0)$	$\mathrm{F}\mathrm{T}\mathrm{R}$
$\phi (2,{\epsilon }_0,0)$		$\mathrm{K}\mathrm{P}{\mathrm{h}}^{\mathrm{0}}\mathrm{+}\mathrm{(}\mathrm{F}\mathrm{-}{\mathrm{I}}_{\mathrm{\omega }}\mathrm{)}$
$\psi ({\mathrm{\Omega }}^{\mathrm{\Omega }\omega })$		$\mathrm{K}\mathrm{P}{\mathrm{M}}^{\mathrm{-}}$
$\phi ({\epsilon }_0,0,0)$	${\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{T}\mathrm{D}\mathrm{C}$
$\phi (1,0,0,0)$	${\mathrm{p}}_{\mathrm{1}}\mathrm{(}{\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{T}\mathrm{D}{\mathrm{C}}_{\mathrm{0}}\mathrm{)}$
$\psi ({\mathrm{\Omega }}^{{\mathrm{\Omega }}^{\omega }})$	$\mathrm{R}\mathrm{C}{A}_{\mathrm{0}}^{\mathrm{*}}\mathrm{+}{\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}{\mathrm{A}}^{\mathrm{-}}$ ${\mathrm{p}}_{\mathrm{3}}\mathrm{(}\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{)}$		$\mathrm{F}\mathrm{I}\mathrm{T}$ $\mathrm{T}\mathrm{I}\mathrm{D}$
$\vartheta ({\mathrm{\Omega }}^{\mathrm{\Omega }})$	${\mathrm{p}}_{\mathrm{1}}\mathrm{(}{\mathrm{p}}_{\mathrm{3}}\mathrm{(}\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{)}\mathrm{)}$
${\theta }_{(n+2)({\mathrm{\Omega }}^{\omega })}0$	$\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}+{\mathrm{\Pi }}_{n+2}^1-\mathrm{B}\mathrm{I}$ ${\mathrm{\Pi }}_{n+1}^1-\mathrm{R}\mathrm{F}\mathrm{N}$ $({\mathrm{\Pi }}_{n+2}^1-\mathrm{B}\mathrm{I}{)}_0$ $({\mathrm{\Pi }}_{n+2}^1-\mathrm{B}\mathrm{I}{)}_0^{-}$	$\mathrm{K}\mathrm{P}{\omega }^{-}+{\mathrm{\Pi }}_{n+2}^{\mathrm{s}\mathrm{e}\mathrm{t}}-\mathrm{F}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$
${\theta }_{(n+2)({\mathrm{\Omega }}^{\omega })}0$	$\mathrm{A}\mathrm{C}\mathrm{A}+{\mathrm{\Pi }}_{n+2}^1-\mathrm{B}\mathrm{I}$ $({\mathrm{\Pi }}_{n+2}^1-\mathrm{B}\mathrm{I}{)}^{-}$	$\mathrm{K}\mathrm{P}{\omega }^{-}+\mathrm{I}\mathrm{N}\mathrm{D}+{\mathrm{\Pi }}_{n+2}^{\mathrm{s}\mathrm{e}\mathrm{t}}-\mathrm{F}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$
$\psi ({\psi }_1(0))$	$\mathrm{A}\mathrm{C}\mathrm{A}\mathrm{+}\mathrm{B}\mathrm{I}$ $\mathrm{A}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}{\mathrm{A}}^{\mathrm{-}}$ ${\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{F}\mathrm{X}{\mathrm{P}}_{\mathrm{0}}$	$\mathrm{K}\mathrm{P}$ $\mathrm{K}\mathrm{P}\mathrm{+}{\mathrm{\Pi }}_{\mathrm{2}}^{\mathrm{s}\mathrm{e}\mathrm{t}}\mathrm{-}\mathrm{R}\mathrm{e}\mathrm{f}\mathrm{l}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$ $\mathrm{K}\mathrm{P}\mathrm{+}\mathrm{(}\mathrm{B}{\mathrm{I}}^{\mathrm{*}}\mathrm{)}$ $\mathrm{K}\mathrm{P}\mathrm{+}\mathrm{(}\mathrm{A}\mathrm{T}{R}_{\mathrm{0}}^{\mathrm{*}}\mathrm{)}$ $\mathrm{C}\mathrm{Z}\mathrm{F}$ $\mathrm{K}\mathrm{P}{\omega }_2\upharpoonright +{\mathrm{\Delta }}_1-\mathrm{C}\mathrm{A}+s{\mathrm{\Pi }}_1^1-\mathrm{r}\mathrm{e}\mathrm{f}$	$\mathrm{I}{\mathrm{D}}_{\mathrm{1}}$ $\mathrm{I}{D}_{\mathrm{1}}^{\mathrm{2}}$ $\mathrm{M}{\mathrm{L}}_{\mathrm{1}}\mathrm{V}$
$\psi ({\mathrm{\Omega }}_2)$	$\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}+\mathrm{\forall }X\mathrm{\exists }M(X\in M\wedge M{\models }_{\omega }\mathrm{A}\mathrm{C}\mathrm{A}\mathrm{+}\mathrm{B}\mathrm{I})$
$\psi ({\mathrm{\Omega }}_2^{{\mathrm{\Omega }}_2})$	$\mathrm{A}\mathrm{T}{R}_{\mathrm{0}}^{\mathrm{\bullet }}$ $\mathrm{F}{P}_{\mathrm{0}}^{\mathrm{\bullet }}$ ${\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{D}{C}_{\mathrm{0}}^{\mathrm{\bullet }}\mathrm{+}\mathrm{(}\mathrm{S}\mathrm{U}{\mathrm{B}}^{\mathrm{\bullet }}\mathrm{)}$ ${\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{A}{C}_{\mathrm{0}}^{\mathrm{\bullet }}\mathrm{+}\mathrm{(}\mathrm{S}\mathrm{U}{\mathrm{B}}^{\mathrm{\bullet }}\mathrm{)}$		${\widehat{\mathrm{I}\mathrm{D}}}_{<\omega }^{\bullet }$${𝒰}(\mathrm{I}{\mathrm{D}}_{\mathrm{1}})$
$\psi ({\psi }_2(0))$		$\mathrm{K}\mathrm{P}\mathrm{+}\mathrm{\exists }{\omega }_{\mathrm{1}}^{\mathrm{C}\mathrm{K}}$	$\mathrm{I}{\mathrm{D}}_{\mathrm{2}}$ $\mathrm{I}{D}_{\mathrm{2}}^{\mathrm{2}}$
$\psi ({\mathrm{\Omega }}_{\omega })$	${\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{1}}\mathrm{-}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}$ ${\mathrm{\Delta }}_{\mathrm{2}}^{\mathrm{1}}\mathrm{-}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Sigma }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{\wedge }{\mathrm{\Pi }}_{\mathrm{1}}^{\mathrm{0}}\mathrm{-}\mathrm{d}\mathrm{e}\mathrm{t}\mathrm{.}$ $\mathrm{R}\mathrm{C}{\mathrm{A}}_{\mathrm{0}}\mathrm{+}{\mathrm{\Delta }}_{\mathrm{2}}^{\mathrm{0}}\mathrm{-}\mathrm{R}\mathrm{T}$	${\mathrm{K}\mathrm{P}\mathrm{l}}^r$ ${\mathrm{K}\mathrm{P}\mathrm{i}}^r$ $\mathrm{K}\mathrm{P}{\beta }^r$	${\mathrm{I}\mathrm{D}}_{<\omega }$ $({\mathrm{I}\mathrm{D}}_{<\omega }^2{)}_0$