证明论序数

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

定义和性质

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

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

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

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

证明论序数满足：

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

证明论序数表

证明论序数	算术论体系	集合论体系	其他体系
-	$Q$	$K P^{-}$
$ω^{2}$	$R F A$ $I Δ_{0}$
$ω^{3}$	$R C A_{0}^{}$ $W K L_{0}^{}$ $I Δ_{0} + e x p$
$ω^{n}$	$I Δ_{0} + ℰ_{n} is total$
$ω^{ω}$	$R C A_{0}$ $W K L_{0}$ $P R A$ $R C A_{0}^{2}$	$C P R C$ $K P^{-} + Π_{1}^{s e t} F o n d a t i o n + I N D$
$ω^{ω^{ω^{ω}}}$	$R C A_{0} + (Π_{2}^{0})^{-} - I N D$
$ω ↑ ↑ (n + 2)$	$I Σ_{n + 1}$
$ε_{0}$	$P A$ $A C A_{0}$ $Δ_{1}^{1} - C A_{0}$ $Σ_{1}^{1} - A C_{0}$	$K P^{- \infty}$	$E M_{0}$
$ε_{1}$	$A C A_{0} + K P H T$
$ε_{ω}$	$A C A_{0} + i R T$ $R C A_{0} + \forall Y \forall n \exists X (T J (n, X, Y))$
$ε_{ε_{0}}$	$A C A$ ${F P}_{n} - A C A'_{0}$ ${F P}_{n} - A C A^{'}$
$ζ_{0}$	$A C A_{0} + \forall X \exists Y (T J (ω, X, Y))$ $A C A_{0} + (B R)$ $p_{1} (A C A_{0})$
$φ (2, ε_{0})$	$A C A + \forall X \exists Y (T J (ω, X, Y))$ $R F N$
$φ (ω, 0)$	$Δ_{1}^{1} - C R$ $R C A_{0}^{*} + Π_{1}^{1} - C A^{-}$ $Σ_{1}^{1} - D C_{0}$		$I D_{1}^{#}$ $E M_{0} + J R$ $P I D$ $A c c - I D (A c c)$ $(Π_{0}^{0} (P), P \cup N) - I D$ $(Π_{0}^{0} (P), P \land N) - I D (A c c)$
$φ (ν + 1, 0)$	$A C A_{0} + \forall X \exists Y (T J (ω^{ν}, X, Y))$
$ψ (Ω^{ε_{0}})$	$Δ_{1}^{1} - C A$ $Σ_{1}^{1} - A C$ ${(Π_{1}^{0} - C A)}_{< ε_{0}}$
$ψ (Ω^{ψ (Ω^{ω})})$		$P R S ω$
$Γ_{0}$	$A T R_{0}$ $Δ_{1}^{1} - C A + B R$ $R C A_{0} + Σ_{1}^{0} - R T$ $R C A_{0} + Δ_{1}^{0} - R T$ $R C A_{0} + Σ_{1}^{0} - d e t .$ $R C A_{0} + Δ_{1}^{0} - d e t .$ $F P_{0}$	$K P i^{-}$ $C Z F^{-} + I N A C$	${\hat{I D}}_{< ω}$ ${\hat{I D}}^{*}$ ${M L}_{< ω}$ $M L U$ $U (P A)$
$φ (1, 0, ω^{ω})$		$K P l_{0} + (Σ_{1} - I_{ω})$
$φ (1, 0, ε_{0})$	$A T R$		${\hat{I D}}_{ω}$
$ψ (Ω^{Ω + 1})$	$R C A_{0} + \forall X \exists M (X \in M \land M ⊨_{ω} A T R_{0})$
$ψ (Ω^{Ω + ω})$	$A T R_{0} + Σ_{1}^{1} - D C$		${\hat{I D}}_{< ω^{ω}}$
$ψ (Ω^{Ω + ε_{0}})$	$A T R + Σ_{1}^{1} - D C$		${\hat{I D}}_{< ε_{0}}$
$ψ (Ω^{Ω + Γ_{0}})$			${\hat{I D}}_{< Γ_{0}}$ $M L S$
$φ (2, 0, 0)$	$F T R_{0}$	$K P h^{-}$	$A u t (\hat{I D})$
$φ (2, 0, ε_{0})$	$F T R$
$φ (2, ε_{0}, 0)$		$K P h^{0} + (F - I_{ω})$
$ψ (Ω^{Ω ω})$		$K P M^{-}$
$φ (ε_{0}, 0, 0)$	$Σ_{1}^{1} - T D C$
$φ (1, 0, 0, 0)$	$p_{1} (Σ_{1}^{1} - T D C_{0})$
$ψ (Ω^{Ω^{ω}})$	$R C A_{0}^{*} + Π_{1}^{1} - C A^{-}$ $p_{3} (A C A_{0})$		$F I T$ $T I D$
$ϑ (Ω^{Ω})$	$p_{1} (p_{3} (A C A_{0}))$
$θ_{(n + 2) (Ω^{ω})} 0$	$A C A_{0} + Π_{n + 2}^{1} - B I$ $Π_{n + 1}^{1} - R F N$ $(Π_{n + 2}^{1} - B I)_{0}$ $(Π_{n + 2}^{1} - B I)_{0}^{-}$	$K P ω^{-} + Π_{n + 2}^{s e t} - F o u n d a t i o n$
$θ_{(n + 2) (Ω^{ω})} 0$	$A C A + Π_{n + 2}^{1} - B I$ $(Π_{n + 2}^{1} - B I)^{-}$	$K P ω^{-} + I N D + Π_{n + 2}^{s e t} - F o u n d a t i o n$
$ψ (ψ_{1} (0))$	$A C A + B I$ $A C A_{0} + Π_{1}^{1} - C A^{-}$ $Π_{1}^{0} - F X P_{0}$	$K P$ $K P + Π_{2}^{s e t} - R e f l e c t i o n$ $K P + (B I^{})$ $K P + (A T R_{0}^{})$ $C Z F$ $K P ω_{2} ↾ + Δ_{1} - C A + s Π_{1}^{1} - r e f$	$I D_{1}$ $I D_{1}^{2}$ $M L_{1} V$
$ψ (Ω_{2})$	$R C A_{0} + \forall X \exists M (X \in M \land M ⊨_{ω} A C A + B I)$
$ψ (Ω_{2}^{Ω_{2}})$	$A T R_{0}^{∙}$ $F P_{0}^{∙}$ $Σ_{1}^{1} - D C_{0}^{∙} + (S U B^{∙})$ $Σ_{1}^{1} - A C_{0}^{∙} + (S U B^{∙})$		${\hat{I D}}_{< ω}^{∙}$ $𝒰 (I D_{1})$
$ψ (ψ_{2} (0))$		$K P + \exists ω_{1}^{C K}$	$I D_{2}$ $I D_{2}^{2}$
$ψ (Ω_{ω})$	$Π_{1}^{1} - C A_{0}$ $Δ_{2}^{1} - C A_{0}$ $R C A_{0} + Σ_{1}^{0} \land Π_{1}^{0} - d e t .$ $R C A_{0} + Δ_{2}^{0} - R T$	${K P l}^{r}$ ${K P i}^{r}$ $K P β^{r}$	${I D}_{< ω}$ $({I D}_{< ω}^{2})_{0}$
$ψ (Ω_{ω} \cdot ω^{ω})$	$Π_{1}^{1} - C A_{0} + Π_{2}^{1} - I N D$
$ψ (Ω_{ω} \cdot ε_{0})$	$Π_{1}^{1} - C A$	$W - K P l$	$W - I D_{ω}$ $I D_{< ω}^{2}$
$ψ (Ω_{ω} \cdot Ω)$	$Π_{1}^{1} - C A + B R$
$ψ (Ω_{ω}^{ω})$	$Π_{1}^{1} - C A_{0} + Π_{2}^{1} - B I$
$ψ (Ω_{ω}^{ω^{ω}})$	$Π_{1}^{1} - C A_{0} + Π_{2}^{1} - B I + Π_{3}^{1} - I N D$
$ψ (ψ_{ω} (0))$	$Π_{1}^{1} - C A + B I$	$K P l$	$I D_{ω}$ $B I D_{ω}^{2}$
$ψ (Ω_{ω^{ω}})$	$Δ_{2}^{1} - C R$ $(Π_{1}^{1} - C A_{< ω^{ω}})$	${K P l}_{ω^{ω}}^{r}$	$I D_{< ω^{ω}}$
$ψ (Ω_{ε_{0}})$	$Δ_{2}^{1} - C A$ $Σ_{2}^{1} - A C$ $(Π_{1}^{1} - C A_{< ε_{0}})$	${K P l}_{ε_{0}}^{r}$ $W - K P i$ $W - K P β$	$I D_{< ε_{0}}$ $I D_{< ε_{0}}^{2}$ $B I D_{< ε_{0}}^{2}$
$ψ (Ω_{ν \cdot ω})$	$(Π_{1}^{1} - C A_{ν}^{+})_{0}$	${K P l}_{ν +}^{r}$	$I D_{< ν \cdot ω}$ $(P I D_{ν}^{2})_{0}$
$ψ (Ω_{γ} \cdot ω)$	$(Π_{1}^{1} - C A_{γ -})_{0}$	${K P l}_{γ}^{r}$	$(N U I D_{γ}^{2})_{0}$
$ψ (Ω_{ν \cdot ω} \cdot ε_{0}))$	$Π_{1}^{1} - C A_{ν}^{+}$	$W - K P l_{ν +}$	$W - I D_{ν \cdot ω}$ $P I D_{ν}^{2}$
$ψ (Ω_{γ} \cdot ε_{0})$	$(Π_{1}^{1} - C A_{γ})$ $Π_{1}^{1} - C A_{γ -}$	$W - K P l_{γ}$	$W - I D_{γ}$ $I D_{γ}^{2}$ $N U I D_{γ}^{2}$
$ψ (Ω_{ν \cdot ω} \cdot Ω))$	$Π_{1}^{1} - C A_{ν}^{+} + B R$		$P I D_{ν}^{2} + B R$
$ψ (Ω_{γ} \cdot Ω)$	$Π_{1}^{1} - C A_{γ -} + B R$		$N U I D_{γ}^{2} + B R$
$ψ (Ω_{ω^{γ}})$	$(Π_{1}^{1} - C A_{ω γ})_{0}$ $(Π_{1}^{1} - C A_{< ω γ})$ $(Π_{1}^{1} - C A_{< ω γ}) + B I$		$(I D_{ω^{γ}}^{2})_{0}$ $I D_{< ω^{γ}}$ $B I D_{< ω^{γ}}^{2}$ $(I D_{< ν}^{2}) + B I$
$ψ (ψ_{ν} (0))$	$(Π_{1}^{1} - C A_{ν})_{0}$	$K P l_{ν}$	$I D_{ν}$ $(I D_{ν}^{2})_{0}$
$ψ (ψ_{ν} (ε_{0}))$	$Π_{1}^{1} - C A_{ν}$		$I D_{ν}^{2}$
$ψ (ψ_{ν} (Ω))$	$Π_{1}^{1} - C A_{ν} + B R$		$I D_{ν}^{2} + B R$
$ψ (ψ_{ν} (ψ_{ν} (0)))$			$B I D_{ν}^{2}$
$ψ (ψ_{ν + 1} (0))$	$Π_{1}^{1} - C A_{ν} + B I$	$K P l_{ν + 1}$	$I D_{ν + 1}$ $I D_{ν}^{2} + B I$
$ψ (ψ_{ν \cdot ω} (0))$	$Π_{1}^{1} - C A_{ν}^{+} + B I$	$K P l_{ν +}$	$I D_{ν \cdot ω}$ $P I D_{ν}^{2} + B I$ $P B I D_{ν}^{2}$
$ψ (ψ_{γ} (0))$	$(Π_{1}^{1} - C A_{γ})_{0}$ $(Π_{1}^{1} - C A_{γ}) + B I$ $Π_{1}^{1} - C A_{γ -} + B I$	$K P l_{γ}$	$I D_{γ}$ $(I D_{γ}^{2})_{0}$ ${I D}_{γ}^{i} (𝒪) {B I D}_{ν}^{2}$ $I D_{γ}^{2} + B I$ $N U I D_{γ}^{2} + B I$
$ψ (ψ_{Ω} (0))$		$K P l^{*}$ ${K P l}_{Ω}^{r}$	$I D_{≺ }$ $B I D^{2 }$ $I D^{2 *} + B I^{2}$
$ψ_{Ω_{1}} (ψ_{I} (0))$	$Π_{1}^{1} - T R_{0}$ $Π_{1}^{1} - T R_{0} + Δ_{2}^{1} - C A_{0}$ $Δ_{2}^{1} - C A + B I (i m p l Σ_{2}^{1})$ $Δ_{2}^{1} - C A + B R (i m p l Σ_{2}^{1})$ $R C A_{0} + Δ_{2}^{0} - d e t .$ $R C A_{0} + Δ_{1}^{1} - R T$	${A u t - K P l}^{r}$ ${A u t - K P l}^{r} + {K P i}^{r}$ $K P i^{ω} + F O U N D R (i m p l - Σ)$ $K P i^{ω} + F O U N D (i m p l - Σ)$	${A u t - I D}_{0}^{p o s}$ ${A u t - I D}_{0}^{m o n}$
$ψ_{Ω_{1}} (ψ_{I} (0) \cdot ε_{0})$	$Π_{1}^{1} - T R$	$W - A u t - K P l$	${A u t - I D}^{p o s}$ ${A u t - I D}^{m o n}$ $A u t - K P l^{ω}$
$ψ_{Ω_{1}} (ψ_{Ω_{ψ_{I} (0) + 1}} (0))$	$Π_{1}^{1} - T R + B I$	$A u t - K P l$	${A u t - I D}_{2}^{p o s}$ ${A u t - I D}_{2}^{m o n}$ $A u t - B I D$
$ψ_{Ω_{1}} (ψ_{I} (I^{ω}))$	$Δ_{2}^{1} - T R_{0}$ $Σ_{2}^{1} - T R D C_{0}$ $Δ_{2}^{1} - C A_{0} + Σ_{2}^{1} - B I$		${K P i}^{r} + (Σ - F O U N D)$ ${K P i}^{r} + (Σ - R E C)$
$ψ_{Ω_{1}} (ψ_{I} (I^{ε_{0}}))$	$Δ_{2}^{1} - T R$ $Σ_{2}^{1} - T R D C$ $Δ_{2}^{1} - C A + Σ_{2}^{1} - B I$		$K P i^{ω} + (Σ - F O U N D)$ $K P i^{ω} + (Σ - R E C)$
$ψ_{Ω_{1}} (ε_{I + 1})$	$Δ_{2}^{1} - C A + B I$ $Σ_{2}^{1} - A C + B I$	$K P i$ $K P β$ $C Z F + R E A$	$T_{0}$
$ψ_{Ω_{1}} (Ω_{I + ω})$		$K P i^{+}$	$M L_{1} W$ $K P_{1} W$ $I A R I$
$ψ_{Ω_{1}} (ε_{M + 1})$	$Δ_{2}^{1} - C A + B I + (M)$	$K P M$ $C Z F M$
$ψ_{Ω_{1}} (Ω_{M + ω})$		$K P M^{+}$	$M L M$ $A g d a$
$Ψ_{Ω_{1}}^{0} (ε_{K + 1})$	$A C A + B I + Π_{4}^{1} - β -model-Reflection$	$K P + Π_{3}^{s e t} -Reflection$
$Ψ_{𝕏}^{ε_{ξ_{n} + 1}}$	$A C A + B I + Π_{n + 5}^{1} - β -model-Reflection$	$K P + Π_{n + 4}^{s e t} -Reflection$
$Ψ_{𝕏}^{ε_{Ξ + 1}}$	$A C A + B I - β -model-Reflection$	$K P + Π_{ω}^{s e t} -Reflection$
$Ψ_{ℍ}^{ε_{Υ + 1}}$		$K P i + \forall α \exists κ (L_{κ} ≺_{1} L_{κ + α})$
$ψ (Ω_{𝕊 + ω})$	$Π_{1}^{1} - C A_{0} + Π_{2}^{1} - C A^{-}$	${K P l}^{r} + \exists M (Trans (M) \land M ≺_{1} V)$
$Ψ_{𝕂}^{ε_{I + 1}}$	$Δ_{2}^{1} - C A + B I + Π_{2}^{1} - C A^{-}$	$K P i + \exists M (Trans (M) \land M ≺_{1} V)$
$ℐ_{ω} \cap ω_{1}^{C K}$	$Π_{2}^{1} - C A_{0}$ $Δ_{3}^{1} - C A_{0}$
$ℐ_{ω + 1} \cap ω_{1}^{C K}$	$Π_{2}^{1} - C A + B I$	$K P + Σ_{1}^{s e t} - S e p a r a t i o n$ $K P i + \forall α \exists β (β > α) (β stable)$
$ℐ_{ε_{0}} \cap ω_{1}^{C K}$	$Δ_{3}^{1} - C A$ $Σ_{3}^{1} - A C$
$maybe ψ_{Ω} (ε_{𝕀 + 1})$	$Δ_{3}^{1} - C A + B I$ $Σ_{3}^{1} - A C + B I$ $Σ_{3}^{1} - D C + B I$	$K P + Δ_{2}^{s e t} -Separation$
$ψ_{Ω} (ε_{𝕀 + 1})$		$K P + Π_{1}^{s e t} -Collection$
	$Π_{n + 3}^{1} - C A + B I$	$K P + Σ_{n + 2}^{s e t} -Separation$
	$Π_{n + 3}^{1} - C A + Σ_{n + 3}^{1} - A C + B I$	$K P^{-} + Σ_{n + 2}^{s e t} -Separation + Σ_{n + 2}^{s e t} -Collection$
	$Z_{2} = Π_{\infty}^{1} - C A$ $Δ_{1}^{2} - C A_{0}$ $Z_{2} + Σ_{\infty}^{1} - A C$	$K P + Σ_{ω}^{s e t} -Separation$ $K P^{-} + Σ_{ω}^{s e t} -Separation + Σ_{ω}^{s e t} -Collection$ $Z F C^{-} = Z F C - P o w e r s e t$
	$Z_{n + 3} = Π_{\infty}^{n + 2} - C A$ $Δ_{1}^{n + 3} - C A_{0}$	$Z F C^{-} + V = L + \exists ω_{n + 1}$
	$Z_{\infty} = Π_{0}^{\infty} - C A$	$Z$ $Z C$ $I Z$
		$I Z F = C Z F + P o w e r s e t + Π_{ω}^{s e t} - R e f l e c t i o n$ $Z F = C Z F + L E M = I Z F + L E M$ $Z F C$ $Z F C + V = L$ $A S T$ $I S T$ $N B G = G B C$ $G B$