证明论序数：修订间差异

2025年7月21日 (一) 22:13的版本

证明论序数（或称证明论强度序数，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$
$ψ (Ω_{ω^{ω}})$	$Δ_{2}^{1} - C R$ $(Π_{1}^{1} - C A_{< ω^{ω}})$
$ψ (Ω_{ε_{0}})$	$Δ_{2}^{1} - C A$ $Σ_{2}^{1} - A C$ $(Π_{1}^{1} - C A_{< ε_{0}})$
$ψ (Ω_{ν \cdot ω})$	$(Π_{1}^{1} - C A_{ν}^{+})_{0}$
$ψ (Ω_{γ} \cdot ω)$	$(Π_{1}^{1} - C A_{γ -})_{0}$
$ψ (Ω_{ν \cdot ω} \cdot ε_{0}))$	$Π_{1}^{1} - C A_{ν}^{+}$
$ψ (Ω_{γ} \cdot ε_{0})$	$(Π_{1}^{1} - C A_{γ})$ $Π_{1}^{1} - C A_{γ -}$
$ψ (Ω_{ν \cdot ω} \cdot Ω))$	$Π_{1}^{1} - C A_{ν}^{+} + B R$
$ψ (Ω_{γ} \cdot Ω)$	$Π_{1}^{1} - C A_{γ -} + B R$
$ψ (Ω_{ω^{γ}})$
$ψ (ψ_{ν} (0))$
$ψ (ψ_{ν} (ε_{0}))$
$ψ (ψ_{ν} (Ω))$
$ψ (ψ_{ν} (ψ_{ν} (0)))$
$ψ (ψ_{ν + 1} (0))$
$ψ (ψ_{ν \cdot ω} (0))$
$ψ (ψ_{γ} (0))$
$ψ (ψ_{Ω} (0))$
$ψ_{Ω_{1}} (ψ_{I} (0))$
$ψ_{Ω_{1}} (ψ_{I} (0) \cdot ε_{0})$
$ψ_{Ω_{1}} (ψ_{Ω_{ψ_{I} (0) + 1}} (0))$
$ψ_{Ω_{1}} (ψ_{I} (I^{ω}))$
$ψ_{Ω_{1}} (ψ_{I} (I^{ε_{0}}))$
$ψ_{Ω_{1}} (ε_{I + 1})$
$ψ_{Ω_{1}} (Ω_{I + ω})$
$ψ_{Ω_{1}} (ε_{M + 1})$
$ψ_{Ω_{1}} (Ω_{M + ω})$

@@ 第219行： / 第219行： @@
 |<math>{\rm ID}_{<\omega}</math><br><math>({\rm ID}_{<\omega}^2)_0</math>
 |-
-|
+|<math>\psi(\Omega_\omega\cdot\omega^\omega)</math>
-|
+|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-IND</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_\omega\cdot\varepsilon_0)</math>
-|
+|<math>\rm \Pi_1^1-CA</math>
-|
+|<math>\rm W-KPl</math>
-|
+|<math>\rm W-ID_\omega</math>
+<math>\rm ID_{<\omega}^2</math>
 |-
-|
+|<math>\psi(\Omega_\omega\cdot\Omega)</math>
-|
+|<math>\rm \Pi_1^1-CA+BR</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_\omega^\omega)</math>
-|
+|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_\omega^{\omega^\omega})</math>
-|
+|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI+\Pi_3^1-IND</math>
 |
 |
 |-
-|
+|<math>\psi(\psi_\omega(0))</math>
-|
+|<math>\rm \Pi_1^1-CA+BI</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_{\omega^\omega})</math>
-|
+|<math>\rm \Delta_2^1-CR</math>
+<math>\rm (\Pi_1^1-CA_{<\omega^\omega})</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_{\varepsilon_0})</math>
-|
+|<math>\rm \Delta_2^1-CA</math>
+<math>\rm \Sigma_2^1-AC</math>
+<math>\rm (\Pi_1^1-CA_{<\varepsilon_0})</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_{\nu\cdot\omega})</math>
-|
+|<math>\rm (\Pi_1^1-CA_\nu^+)_0</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_\gamma\cdot\omega)</math>
-|
+|<math>\rm (\Pi_1^1-CA_{\gamma-})_0</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\varepsilon_0))</math>
-|
+|<math>\rm \Pi_1^1-CA_\nu^+</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_\gamma\cdot\varepsilon_0)</math>
-|
+|<math>\rm (\Pi_1^1-CA_\gamma)</math>
+<math>\rm \Pi_1^1-CA_{\gamma-}</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\Omega))</math>
-|
+|<math>\rm \Pi_1^1-CA_\nu^++BR</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_\gamma\cdot\Omega)</math>
-|
+|<math>\rm \Pi_1^1-CA_{\gamma-}+BR</math>
 |
 |
 |-
-|
+|<math>\psi(\Omega_{\omega^\gamma})</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_\nu(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_\nu(\varepsilon_0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_\nu(\Omega))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_\nu(\psi_\nu(0)))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_{\nu+1}(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_{\nu\cdot\omega}(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_\gamma(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi(\psi_\Omega(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_I(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_I(0)\cdot\varepsilon_0)</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_{\Omega_{\psi_I(0)+1}}(0))</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_I(I^\omega))</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_I(I^{\varepsilon_0}))</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\varepsilon_{I+1})</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\Omega_{I+\omega})</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\varepsilon_{M+1})</math>
 |
 |
 |
 |-
-|
+|<math>\psi_{\Omega_1}(\Omega_{M+\omega})</math>
 |
 |