证明论序数：修订间差异

2025年7月27日 (日) 13:21的最新版本

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

定义和性质

对形式理论 $T$ ，其证明论序数 $| T |_{ord}$ （ $| T |$ 或 $PTO (T)$ ）定义为能用超限归纳证明的原始递归良序的序型最大值。

证明论序数满足：

对任意递归序数 $β < | T |$ ，理论 $T$ 能证明“所有序数小于 $β$ 的原始递归良序关系都是良序的”；对 $α = | T |$ ，理论 $T$ 无法证明“所有序数小于 $α$ 的原始递归良序关系都是良序的”。
存在一种递归记号系统，自然表示所有小于 $| T |$ 的序数；理论 $T$ 能通过超限归纳（序数是良序集的序型，满足超限归纳原理： $\forall α (\forall β < α (P (β) \Rightarrow P (α)) \Rightarrow \forall α P (α))$ ，其中 $P$ 是任意性质）到 $| T |$ ，证明自身的一致性（即 $T ⊬ ⊥$ ）；理论 $T$ 能证明所有初等递归函数在小于 $| T |$ 的序数上总停止；对任意递归序数 $β < | T |$ ，至少不满足上述条件中的一条。
证明论序数必为递归序数（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$

ZFC 相关证明论序数：

$S_{0} = (E x t) + (N u l l) + (P a i r) + (U n i o n) + (D i f f) (Rudimentary set theory)$
$S_{1} = S_{0} + (P o w e r s e t)$
$M_{0} = S_{1} + (Δ_{0}^{s e t} - S e p a r a t i o n)$
$M_{1} = M_{0} + (R e g u l a r i t y) + (T r a n s i t i v e C o n t a i n m e n t)$
${K P}^{-} = S_{0} + (I n f i n i t y) + (Δ_{0}^{s e t} - S e p a r a t i o n) + (Δ_{0}^{s e t} - C o l l e c t i o n)$
${K P}^{- \infty} = S_{0} + (F o u n d a t i o n) + (Δ_{0}^{s e t} - S e p a r a t i o n) + (Δ_{0}^{s e t} - C o l l e c t i o n)$
$K P = {K P}^{- \infty} + (I n f i n i t y) = {K P}^{-} + (F o u n d a t i o n)$
$K P l = K P + (universe limit of admissible sets)$
$K P i = K P + (recursively inaccessible universe)$
$K P h = K P + (recursively hyperinaccessible universe)$
$K P M = K P + (recursively Mahlo universe)$
$Z B Q C = M_{0} + (R e g u l a r i t y) + (I n f i n i t y) + (C h o i c e)$
$N F U + (I n f i n i t y) + (C h o i c e)$
$M A C = M_{1} + (I n f i n i t y) + (C h o i c e) = Z B Q C + (Transitive Containment)$
$M O S T = M A C + (Δ_{0}^{s e t} - C o l l e c t i o n) = Z B Q C + K P + (Σ_{1}^{s e t} - S e p a r a t i o n)$
$Z = S_{1} + (R e g u l a r i t y) + (I n f i n i t y) + (Σ_{ω}^{s e t} - S e p a r a t i o n)$
$Z C = Z + (C h o i c e) = Z B Q C + (σ_{ω}^{s e t} - S e p a r a t i o n)$
$M A C + \forall m (ℶ_{ℶ_{m}} exists)$
$N F U + (I n f i n i t y) + (C h o i c e)$
$Z + (Π_{2}^{s e t} - R e p l a c e m e n t)$
${N F U}^{*} = N F U + (C o u n t i n g) + (S t r o n g l y C a n t o r i a n S e p a r a t i o n)$
$Z + (Π_{m}^{s e t} - R e p l a c e m e n t)$
$Z F = Z + (Π_{ω}^{s e t} - R e p l a c e m e n t)$
$A S T$
$G B$
$Z F C = Z F + (Choice)$
$N B G = G B C = G B + (Global Choice)$
$Z F C + (there is a worldly cardinal)$
$N B G + (there is a stationary proper class of worldly cardinals)$
$N B G + (Class Forcing Theorem)$
$N B G + (Clopen Class Game Determinacy)$
$M K = N B G + (Π_{\infty}^{c l a s s} - C A)$
$Z F C + (there is an inaccessible cardinal)$
$Z F C + (Π_{1}^{1} Perfect Set Property)$
$Z F C + (Σ_{3}^{1} Lebesgue measurability)$
$Z F C + (there are ω inaccessible cardinals)$
$Z F C + (\forall α (ω \leq α \leq ℵ_{ω} \Rightarrow | V_{α} \cap L | = | α |))$
$Z F C + (there is a proper class of inaccessible cardinals)$
$Z F C + (Grothendieck Universe Axiom)$
$Z F C + (there is a Σ_{n}^{s e t} -reflecting cardinal)$
$Z F C + (there is a σ_{ω}^{s e t} -reflecting cardinal)$
$Z F C + (Ord is Mahlo)$
$Z F C + (there is an uplifting cardinal)$
$Z F C + (Resurrection Axioms)$
$Z F C + (there is a Mahlo cardinal)$
$S M A H = Z F C + (there is a n -Mahlo cardinal)_{n \in ℕ}$
$N F U A = N F U + (Infinity) + (Cantorian Sets)$
${S M A H}^{+} = Z F C + \forall n (there is a n -Mahlo cardinal)$
$M K + (Ord is weakly compact)$
${G P K}_{\infty}^{+} = {G P K}^{+} + (Infinity)$
$N F U B = N F U + (Infinity) + (Cantorian Sets) + (Small Ordinals)$
$Z F C + (there is a weakly compact cardinal)$
$Z F C + (ω_{2} has the tree property)$
$Z F C + (there is a totally indescribable cardinal)$
$Z F C + (there is a subtle cardinal)$
$Z F C + (there is an ineffable cardinal)$
$Z F C + \forall α (α < ω_{1} \Rightarrow there is a α -Erdős cardinal)$
$Z F C + (0^{♯} exists)$
$Z F C + (L ⊨ ℵ_{ω} is regular)$
$Z F C + \forall α (α \geq ω ⟹ | V_{α} \cap L | = | α |)$
$Z F C + (parameter-free Σ_{1}^{1} -determinacy)$
$Z F C + \forall x (x \in ℝ ⟹ x^{♯} exists)$
$Z F C + (Σ_{1}^{1} -determinacy)$
$Z F C + \forall x (x^{♯} exists)$
$Z F C + (Σ_{2}^{1} universal Baireness)$
$Z F C + (there is an ω_{1} -Erdős cardinal)$
$Z F C + (Chang's Conjecture)$
$S R P = Z F C + (there is cardinal with the n -stationary Ramsey property)_{n \in ℕ}$
${S R P}^{+} = Z F C + \forall n (there is a cardinal with the n -stationary Ramsey property)$
$M K + (Ord is measurable)$
$N F U M = N F U + (Infinity) + (Large Ordinals) + (Small Ordinals)$
$Z F M = Z F C + (there is a measurable cardinal)$
$Z F C + ({N S}_{ω_{1}} is precipitous)$
$Z F + (ω_{1} is measurable)$
$Z F C + (there is a measurable cardinal κ such that o (κ) = 2)$
$Z F C + ({N S}_{ω_{2}} is precipitous)$
$Z F C + (there is a measurable cardinal κ such that o (κ) = κ^{+ +})$
$Z F C + \neg S C H$
$Z F C + (2^{ℵ_{ω}} = ℵ_{ω + 2})$
$Z F C + (Ord is Woodin)$
$Z F C + \neg S C H$
$Z_{2} + (Δ_{2}^{1} -determinacy) (conjectural)$
$M K + (Ord is Woodin)$
$Z F C + \neg S C H$
$Z_{3} + (lightface Δ_{2}^{1} -determinacy)$
$N B G + (Ord is Woodin)$
$Z F C + \neg S C H$
$Z_{3} + (Δ_{2}^{1} -determinacy)$
$Z F C + (there is a Woodin cardinal)$
$Z F C + (Δ_{2}^{1} -determinacy)$
$Z F C + (O D ⊨ A D)$
$Z F C + ({N S}_{ω_{1}} is ω_{2} -saturated)$
$Z F C + (there are n Woodin cardinals)_{n \in ℕ}$
$Z_{2} + (P D)$
$Z F C + (there are ω Woodin cardinals)$
$Z F + (A D)$
$Z F C + (L (ℝ) ⊨ A D)$
$Z F C + (O D (ℝ) ⊨ A D)$
$Z F + D C + (ω_{1} is 𝒫 (ω_{1}) -strongly compact)$
$Z F C + ({N S}_{ω_{1}} is ω_{1} -dense)$
$Z F + D C + (ω_{1} is 𝒫 (ℝ) -strongly compact)$
$Z F + D C + ({A D}_{ℝ})$
$Z F C + (there is a superstrong cardinal)$
$Z F C + (there is a subcompact cardinal)$
$Z F C + (V = L [\vec{E}]) + \exists κ (\neg ◻_{κ})$
$Z F C + (there is a strongly compact cardinal)$
$Z F C + (Proper Forcing Axiom)$
$Z F C + (there is a supercompact cardinal)$
$Z F C + (Martin's Maximum)$
$Z F C + \forall n (there is a proper class of C^{(n)} -extendible cardinals)$
$Z F C + (Vopěnka's Principle)$
$Z F C + (there is a high-jump cardinal)$
$H U G E = Z F C + ( there is a n {-huge cardinal )}_{n \in ℕ}$
$Z F C + (Wholeness Axiom {W A}_{n})$
$Z F C + I 3 = Z F C + \exists λ (E_{0} (λ))$
$Z F C + I 2 = Z F C + \exists λ (E_{1} (λ))$
$Z F C + I 1 = Z F C + \exists λ (E_{ω} (λ))$
$Z F C + I 0$
$Z F + D C + \exists λ \exists j : V_{λ + 2} ≺_{Σ_{ω}^{s e t}} V_{λ + 2}$
${Z F}_{j} + D C + (there is a Reinhardt cardinal )$
$Z F + D C + (there is a Berkeley cardinal)$

@@ 第2行： / 第2行： @@
 === 定义和性质 ===
-序数是良序集的序型，满足超限归纳原理：<math>\forall\alpha(\forall\beta<\alpha(P(\beta)\Rightarrow P(\alpha))\Rightarrow\forall\alpha P(\alpha))</math>，其中 <math>P</math> 是任意性质。
+对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（<math>|T|</math> 或 <math>\text{PTO}(T)</math>）定义为能用超限归纳证明的原始递归良序的序型最大值。
-对形式理论 <math>T</math>，其证明论序数 <math>|T|_{\text{ord}}</math>（在 googology 语境中，可写为 <math>\text{PTO}(T)</math>）定义为满足以下条件的最小序数 <math>\alpha</math>：
-# 存在一种自然表示序数 <math><\alpha</math> 的递归记号系统
-# 通过超限归纳至 <math>\alpha</math>，可证明 <math>T</math> 的一致性（即 <math>T\nvdash\perp</math>）
-# <math>T</math> 能证明所有初等递归函数在 <math><\alpha</math> 的序数上总停止
-或者说，是理论 <math>T</math> 能用超限归纳证明的原始递归良序的序型最大值。
 证明论序数满足：
-# '''不可达性'''（Inaccessibility）：若 <math>|T|_\text{ord}=\alpha</math>，则 <math>T</math> 无法证明“存在序数 <math>\beta</math> 使得 <math>\beta=\alpha</math>”的良序性
+# 对任意递归序数 <math>\beta<|T|</math>，理论 <math>T</math> 能证明“所有序数小于 <math>\beta</math> 的原始递归良序关系都是良序的”；对 <math>\alpha=|T|</math>，理论 <math>T</math> 无法证明“所有序数小于 <math>\alpha</math> 的原始递归良序关系都是良序的”。
-# '''递归性'''（Recursivity）：证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序
+# 存在一种递归记号系统，自然表示所有小于 <math>|T|</math> 的序数；理论 <math>T</math> 能通过超限归纳（序数是良序集的序型，满足超限归纳原理：<math>\forall\alpha(\forall\beta<\alpha(P(\beta)\Rightarrow P(\alpha))\Rightarrow\forall\alpha P(\alpha))</math>，其中 <math>P</math> 是任意性质）到 <math>|T|</math>，证明自身的一致性（即 <math>T\nvdash\perp</math>）；理论 <math>T</math> 能证明所有初等递归函数在小于 <math>|T|</math> 的序数上总停止；对任意递归序数 <math>\beta<|T|</math>，至少不满足上述条件中的一条。
+# 证明论序数必为递归序数（recursive ordinal），即存在递归关系定义其良序。
 === 证明论序数表 ===
@@ 第24行： / 第17行： @@
 ! scope="col" |其他体系
 |-
-| -
+|
 |<math>Q</math>
 |<math>\rm KP^-</math>
@@ 第30行： / 第23行： @@
 |-
 |<math>\omega^2</math>
-|<math>\rm RFA</math>
+|<math>\rm RFA</math><br><math>\rm I\Delta_0</math>
-<math>\rm I\Delta_0</math>
 |
 |
 |-
 |<math>\omega^3</math>
-|<math>\rm RCA_0^*</math>
+|<math>\rm RCA_0^*</math><br><math>\rm WKL_0^*</math><br><math>\rm I\Delta_0+exp</math>
-<math>\rm WKL_0^*</math>
-<math>\rm I\Delta_0+exp</math>
 |
 |
@@ 第48行： / 第38行： @@
 |-
 |<math>\omega^\omega</math>
-|<math>\rm RCA_0</math>
+|<math>\rm RCA_0</math><br><math>\rm WKL_0</math><br><math>\rm PRA</math><br><math>\rm RCA_0^2</math>
-<math>\rm WKL_0</math>
+|<math>\rm CPRC</math><br><math>\rm KP^-+\Pi_1^{set}\ Fondation+IND</math>
-<math>\rm PRA</math>
-<math>\rm RCA_0^2</math>
-|<math>\rm CPRC</math>
-<math>\rm KP^-+\Pi_1^{set}\ Fondation+IND</math>
 |
 |-
@@ 第67行： / 第53行： @@
 |-
 |<math>\varepsilon_0</math>
-|<math>\rm PA</math>
+|<math>\rm PA</math><br><math>\rm ACA_0</math><br><math>\rm \Delta_1^1-CA_0</math><br><math>\rm \Sigma_1^1-AC_0</math>
-<math>\rm ACA_0</math>
-<math>\rm \Delta_1^1-CA_0</math>
-<math>\rm \Sigma_1^1-AC_0</math>
 |<math>\rm KP^{-\infty}</math>
 |<math>\rm EM_0</math>
@@ 第80行： / 第63行： @@
 |-
 |<math>\varepsilon_\omega</math>
-|<math>\rm ACA_0+iRT</math>
+|<math>\rm ACA_0+iRT</math><br><math>{\rm RCA_0}+\forall Y\forall n\exists X({\rm TJ}(n,X,Y))</math>
-<math>{\rm RCA_0}+\forall Y\forall n\exists X({\rm TJ}(n,X,Y))</math>
 |
 |
 |-
 |<math>\varepsilon_{\varepsilon_0}</math>
-|<math>\rm ACA</math>
+|<math>\rm ACA</math><br><math>{\rm FP}_n-{\rm ACA'_0}</math><br><math>{\rm FP}_n-{\rm ACA'}</math>
-<math>{\rm FP}_n-{\rm ACA'_0}</math>
-<math>{\rm FP}_n-{\rm ACA'}</math>
 |
 |
 |-
 |<math>\zeta_0</math>
-|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math>
+|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm ACA_0+(BR)</math><br><math>\rm p_1(ACA_0)</math>
-<math>\rm ACA_0+(BR)</math>
-<math>\rm p_1(ACA_0)</math>
 |
 |
 |-
 |<math>\varphi(2,\varepsilon_0)</math>
-|<math>{\rm ACA}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math>
+|<math>{\rm ACA}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm RFN</math>
-<math>\rm RFN</math>
 |
 |
 |-
 |<math>\varphi(\omega,0)</math>
-|<math>\rm \Delta_1^1-CR</math>
+|<math>\rm \Delta_1^1-CR</math><br><math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm \Sigma_1^1-DC_0</math>
-<math>\rm RCA_0^*+\Pi_1^1-CA^-</math>
-<math>\rm \Sigma_1^1-DC_0</math>
 |
-|<math>\rm ID_1^\#</math>
+|<math>\rm ID_1^\#</math><br><math>\rm EM_0+JR</math><br><math>\rm PID</math><br><math>\rm Acc-ID(Acc)</math><br><math>\rm (\Pi_0^0(P),P\cup N)-ID</math><br><math>\rm (\Pi_0^0(P),P\land N)-ID(Acc)</math>
-<math>\rm EM_0+JR</math>
-<math>\rm PID</math>
-<math>\rm Acc-ID(Acc)</math>
-<math>\rm (\Pi_0^0(P),P\cup N)-ID</math>
-<math>\rm (\Pi_0^0(P),P\land N)-ID(Acc)</math>
 |-
 |<math>\varphi(\nu+1,0)</math>
@@ 第123行： / 第93行： @@
 |-
 |<math>\psi(\Omega^{\varepsilon_0})</math>
-|<math>\rm \Delta_1^1-CA</math>
+|<math>\rm \Delta_1^1-CA</math><br><math>\rm \Sigma_1^1-AC</math><br><math>\rm{(\Pi_1^0-CA)}_{<\varepsilon_0}</math>
-<math>\rm \Sigma_1^1-AC</math>
-<math>\rm{(\Pi_1^0-CA)}_{<\varepsilon_0}</math>
 |
 |
@@ 第135行： / 第103行： @@
 |-
 |<math>\Gamma_0</math>
-|<math>\rm ATR_0</math>
+|<math>\rm ATR_0</math><br><math>\rm \Delta_1^1-CA+BR</math><br><math>\rm RCA_0+\Sigma_1^0-RT</math><br><math>\rm RCA_0+\Delta_1^0-RT</math><br><math>\rm RCA_0+\Sigma_1^0-det.</math><br><math>\rm RCA_0+\Delta_1^0-det.</math><br><math>\rm FP_0</math>
-<math>\rm \Delta_1^1-CA+BR</math>
+|<math>\rm KPi^-</math><br><math>\rm CZF^-+INAC</math>
-<math>\rm RCA_0+\Sigma_1^0-RT</math>
+|<math>\widehat{\rm ID}_{<\omega}</math><br><math>\widehat{\rm ID}^*</math><br><math>{\rm ML}_{<\omega}</math><br><math>\rm MLU</math><br><math>\rm U(PA)</math>
-<math>\rm RCA_0+\Delta_1^0-RT</math>
-<math>\rm RCA_0+\Sigma_1^0-det.</math>
-<math>\rm RCA_0+\Delta_1^0-det.</math>
-<math>\rm FP_0</math>
-|<math>\rm KPi^-</math>
-<math>\rm CZF^-+INAC</math>
-|<math>\widehat{\rm ID}_{<\omega}</math>
-<math>\widehat{\rm ID}^*</math>
-<math>{\rm ML}_{<\omega}</math>
-<math>\rm MLU</math>
-<math>\rm U(PA)</math>
 |-
+|<math>\varphi(1,0,\omega^\omega)</math>
 |
-|
+|<math>\rm KPl_0+(\Sigma_1-I_\omega)</math>
-|
 |
 |-
+|<math>\varphi(1,0,\varepsilon_0)</math>
+|<math>\rm ATR</math>
 |
-|
+|<math>\widehat{\rm ID}_\omega</math>
-|
-|
 |-
-|
+|<math>\psi(\Omega^{\Omega+1})</math>
-|
+|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ATR_0})</math>
 |
 |
 |-
+|<math>\psi(\Omega^{\Omega+\omega})</math>
+|<math>\rm ATR_0+\Sigma_1^1-DC</math>
 |
-|
+|<math>\widehat{\rm ID}_{<\omega^\omega}</math>
-|
-|
 |-
+|<math>\psi(\Omega^{\Omega+\varepsilon_0})</math>
+|<math>\rm ATR+\Sigma_1^1-DC</math>
 |
-|
+|<math>\widehat{\rm ID}_{<\varepsilon_0}</math>
-|
-|
 |-
+|<math>\psi(\Omega^{\Omega+\Gamma_0})</math>
 |
 |
-|
+|<math>\widehat{\rm ID}_{<\Gamma_0}</math><br><math>\rm MLS</math>
-|
 |-
-|
+|<math>\varphi(2,0,0)</math>
-|
+|<math>\rm FTR_0</math>
-|
+|<math>\rm KPh^-</math>
-|
+|<math>\rm Aut(\widehat{ID})</math>
 |-
-|
+|<math>\varphi(2,0,\varepsilon_0)</math>
-|
+|<math>\rm FTR</math>
 |
 |
 |-
+|<math>\varphi(2,\varepsilon_0,0)</math>
 |
-|
+|<math>\rm KPh^0+(F-I_\omega)</math>
-|
 |
 |-
+|<math>\psi(\Omega^{\Omega\omega})</math>
 |
-|
+|<math>\rm KPM^-</math>
-|
 |
 |-
-|
+|<math>\varphi(\varepsilon_0,0,0)</math>
-|
+|<math>\rm \Sigma_1^1-TDC</math>
 |
 |
 |-
-|
+|<math>\varphi(1,0,0,0)</math>
-|
+|<math>\rm p_1(\Sigma_1^1-TDC_0)</math>
 |
 |
 |-
+|<math>\psi(\Omega^{\Omega^\omega})</math>
+|<math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm p_3(ACA_0)</math>
 |
-|
+|<math>\rm FIT</math><br><math>\rm TID</math>
-|
-|
 |-
-|
+|<math>\vartheta(\Omega^\Omega)</math>
-|
+|<math>\rm p_1(p_3(ACA_0))</math>
 |
 |
 |-
-|
+|<math>\theta_{(n+2)(\Omega^\omega)}0</math>
-|
+|<math>{\rm ACA_0}+\Pi_{n+2}^1-{\rm BI}</math><br><math>\Pi_{n+1}^1-{\rm RFN}</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0^-</math>
-|
+|<math>{\rm KP}\omega^-+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math>
 |
 |-
-|
+|<math>\theta_{(n+2)(\Omega^\omega)}0</math>
-|
+|<math>{\rm ACA}+\Pi_{n+2}^1-{\rm BI}</math><br><math>(\Pi_{n+2}^1-{\rm BI})^-</math>
-|
+|<math>{\rm KP}\omega^-+{\rm IND}+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math>
 |
 |-
-|
+|<math>\psi(\psi_1(0))</math>
-|
+|<math>\rm ACA+BI</math><br><math>\rm ACA_0+\Pi_1^1-CA^-</math><br><math>\rm \Pi_1^0-FXP_0</math>
-|
+|<math>\rm KP</math><br><math>\rm KP+\Pi_2^{set}-Reflection</math><br><math>\rm KP+(BI^*)</math><br><math>\rm KP+(ATR_0^*)</math><br><math>\rm CZF</math><br><math>{\rm KP}\omega_2\upharpoonright+\Delta_1-{\rm CA}+s\Pi_1^1-{\rm ref}</math>
-|
+|<math>\rm ID_1</math><br><math>\rm ID_1^2</math><br><math>\rm ML_1\ V</math>
 |-
-|
+|<math>\psi(\Omega_2)</math>
-|
+|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ACA+BI})</math>
 |
 |
 |-
+|<math>\psi(\Omega_2^{\Omega_2})</math>
+|<math>\rm ATR_0^\bullet</math><br><math>\rm FP_0^\bullet</math><br><math>\rm \Sigma_1^1-DC_0^\bullet+(SUB^\bullet)</math><br><math>\rm \Sigma_1^1-AC_0^\bullet+(SUB^\bullet)</math>
 |
-|
+|<math>\widehat{\rm ID}_{<\omega}^\bullet</math><math>\mathcal{U}({\rm ID_1})</math>
-|
-|
 |-
+|<math>\psi(\psi_2(0))</math>
 |
-|
+|<math>\rm KP+\exists\omega_1^{CK}</math>
-|
+|<math>\rm ID_2</math><br><math>\rm ID_2^2</math>
-|
 |-
-|
+|<math>\psi(\Omega_\omega)</math>
-|
+|<math>\rm \Pi_1^1-CA_0</math><br><math>\rm \Delta_2^1-CA_0</math><br><math>\rm RCA_0+\Sigma_1^0\land\Pi_1^0-det.</math><br><math>\rm RCA_0+\Delta_2^0-RT</math>
-|
+|<math>{\rm KPl}^r</math><br><math>{\rm KPi}^r</math><br><math>{\rm KP}\beta^r</math>
-|
+|<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><br><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>\rm KPl</math>
-|
+|<math>\rm ID_\omega</math><br><math>\rm BID_\omega^2</math>
 |-
-|
+|<math>\psi(\Omega_{\omega^\omega})</math>
-|
+|<math>\rm \Delta_2^1-CR</math><br><math>\rm (\Pi_1^1-CA_{<\omega^\omega})</math>
-|
+|<math>{\rm KPl}_{\omega^\omega}^r</math>
-|
+|<math>\rm ID_{<\omega^\omega}</math>
 |-
-|
+|<math>\psi(\Omega_{\varepsilon_0})</math>
-|
+|<math>\rm \Delta_2^1-CA</math><br><math>\rm \Sigma_2^1-AC</math><br><math>\rm (\Pi_1^1-CA_{<\varepsilon_0})</math>
-|
+|<math>{\rm KPl}_{\varepsilon_0}^r</math><br><math>\rm W-KPi</math><br><math>{\rm W-KP}\beta</math>
-|
+|<math>\rm ID_{<\varepsilon_0}</math><br><math>\rm ID_{<\varepsilon_0}^2</math><br><math>\rm BID_{<\varepsilon_0}^2</math>
 |-
-|
+|<math>\psi(\Omega_{\nu\cdot\omega})</math>
-|
+|<math>\rm (\Pi_1^1-CA_\nu^+)_0</math>
-|
+|<math>{\rm KPl}_{\nu+}^r</math>
-|
+|<math>\rm ID_{<\nu\cdot\omega}</math><br><math>\rm (PID_\nu^2)_0</math>
 |-
-|
+|<math>\psi(\Omega_\gamma\cdot\omega)</math>
-|
+|<math>\rm (\Pi_1^1-CA_{\gamma-})_0</math>
-|
+|<math>{\rm KPl}_\gamma^r</math>
-|
+|<math>\rm (NUID_\gamma^2)_0</math>
 |-
-|
+|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\varepsilon_0))</math>
-|
+|<math>\rm \Pi_1^1-CA_\nu^+</math>
-|
+|<math>\rm W-KPl_{\nu+}</math>
-|
+|<math>\rm W-ID_{\nu\cdot\omega}</math><br><math>\rm PID_\nu^2</math>
 |-
-|
+|<math>\psi(\Omega_\gamma\cdot\varepsilon_0)</math>
-|
+|<math>\rm (\Pi_1^1-CA_\gamma)</math><br><math>\rm \Pi_1^1-CA_{\gamma-}</math>
-|
+|<math>\rm W-KPl_\gamma</math>
-|
+|<math>\rm W-ID_\gamma</math><br><math>\rm ID_\gamma^2</math><br><math>\rm NUID_\gamma^2</math>
 |-
+|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\Omega))</math>
+|<math>\rm \Pi_1^1-CA_\nu^++BR</math>
 |
-|
+|<math>\rm PID_\nu^2+BR</math>
-|
-|
 |-
+|<math>\psi(\Omega_\gamma\cdot\Omega)</math>
+|<math>\rm \Pi_1^1-CA_{\gamma-}+BR</math>
 |
-|
+|<math>\rm NUID_\gamma^2+BR</math>
-|
-|
 |-
+|<math>\psi(\Omega_{\omega^\gamma})</math>
+|<math>\rm (\Pi_1^1-CA_{\omega\gamma})_0</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})+BI</math>
 |
-|
+|<math>\rm (ID_{\omega^\gamma}^2)_0</math><br><math>\rm ID_{<\omega^\gamma}</math><br><math>\rm BID_{<\omega^\gamma}^2</math><br><math>\rm (ID_{<\nu}^2)+BI</math>
-|
-|
 |-
-|
+|<math>\psi(\psi_\nu(0))</math>
-|
+|<math>\rm (\Pi_1^1-CA_\nu)_0</math>
-|
+|<math>\rm KPl_\nu</math>
-|
+|<math>\rm ID_\nu</math><br><math>\rm (ID_\nu^2)_0</math>
 |-
+|<math>\psi(\psi_\nu(\varepsilon_0))</math>
+|<math>\rm \Pi_1^1-CA_\nu</math>
 |
-|
+|<math>\rm ID_\nu^2</math>
-|
-|
 |-
+|<math>\psi(\psi_\nu(\Omega))</math>
+|<math>\rm \Pi_1^1-CA_\nu+BR</math>
 |
-|
+|<math>\rm ID_\nu^2+BR</math>
-|
-|
 |-
+|<math>\psi(\psi_\nu(\psi_\nu(0)))</math>
 |
 |
-|
+|<math>\rm BID_\nu^2</math>
-|
 |-
-|
+|<math>\psi(\psi_{\nu+1}(0))</math>
-|
+|<math>\rm \Pi_1^1-CA_\nu+BI</math>
-|
+|<math>\rm KPl_{\nu+1}</math>
-|
+|<math>\rm ID_{\nu+1}</math><br><math>\rm ID_\nu^2+BI</math>
 |-
-|
+|<math>\psi(\psi_{\nu\cdot\omega}(0))</math>
-|
+|<math>\rm \Pi_1^1-CA_\nu^++BI</math>
-|
+|<math>\rm KPl_{\nu+}</math>
-|
+|<math>\rm ID_{\nu\cdot\omega}</math><br><math>\rm PID_\nu^2+BI</math><br><math>\rm PBID_\nu^2</math>
 |-
-|
+|<math>\psi(\psi_\gamma(0))</math>
-|
+|<math>\rm (\Pi_1^1-CA_\gamma)_0</math><br><math>\rm (\Pi_1^1-CA_\gamma)+BI</math><br><math>\rm \Pi_1^1-CA_{\gamma-}+BI</math>
-|
+|<math>\rm KPl_\gamma</math>
-|
+|<math>\rm ID_\gamma</math><br><math>\rm (ID_\gamma^2)_0</math><br><math>{\rm ID}_\gamma^i(\mathcal{O}){\rm BID}_\nu^2</math><br><math>\rm ID_\gamma^2+BI</math><br><math>\rm NUID_\gamma^2+BI</math>
 |-
+|<math>\psi(\psi_\Omega(0))</math>
 |
-|
+|<math>\rm KPl^*</math><br><math>{\rm KPl}_\Omega^r</math>
-|
+|<math>\rm ID_{\prec*}</math><br><math>\rm BID^{2*}</math><br><math>\rm ID^{2*}+BI^2</math>
-|
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_I(0))</math>
-|
+|<math>\rm \Pi_1^1-TR_0</math><br><math>\rm \Pi_1^1-TR_0+\Delta_2^1-CA_0</math><br><math>\rm \Delta_2^1-CA+BI(impl\ \Sigma_2^1)</math><br><math>\rm \Delta_2^1-CA+BR(impl\ \Sigma_2^1)</math><br><math>\rm RCA_0+\Delta_2^0-det.</math><br><math>\rm RCA_0+\Delta_1^1-RT</math>
-|
+|<math>{\rm Aut-KPl}^r</math><br><math>{\rm Aut-KPl}^r+{\rm KPi}^r</math><br><math>\rm KPi^\omega+FOUNDR(impl-\Sigma)</math><br><math>\rm KPi^\omega+FOUND(impl-\Sigma)</math>
-|
+|<math>{\rm Aut-ID}_0^{pos}</math><br><math>{\rm Aut-ID}_0^{mon}</math>
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_I(0)\cdot\varepsilon_0)</math>
-|
+|<math>\rm \Pi_1^1-TR</math>
-|
+|<math>\rm W-Aut-KPl</math>
-|
+|<math>{\rm Aut-ID}^{pos}</math><br><math>{\rm Aut-ID}^{mon}</math><br><math>\rm Aut-KPl^\omega</math>
 |-
-|
+|<math>\psi_{\Omega_1}(\psi_{\Omega_{\psi_I(0)+1}}(0))</math>
-|
+|<math>\rm \Pi_1^1-TR+BI</math>
-|
+|<math>\rm Aut-KPl</math>
-|
+|<math>{\rm Aut-ID}_2^{pos}</math><br><math>{\rm Aut-ID}_2^{mon}</math><br><math>\rm Aut-BID</math>
 |-
+|<math>\psi_{\Omega_1}(\psi_I(I^\omega))</math>
+|<math>\rm \Delta_2^1-TR_0</math><br><math>\rm \Sigma_2^1-TRDC_0</math><br><math>\rm \Delta_2^1-CA_0+\Sigma_2^1-BI</math>
 |
-|
+|<math>{\rm KPi}^r+(\Sigma-{\rm FOUND})</math><br><math>{\rm KPi}^r+(\Sigma-{\rm REC})</math>
-|
-|
 |-
+|<math>\psi_{\Omega_1}(\psi_I(I^{\varepsilon_0}))</math>
+|<math>\rm \Delta_2^1-TR</math><br><math>\rm \Sigma_2^1-TRDC</math><br><math>\rm \Delta_2^1-CA+\Sigma_2^1-BI</math>
 |
-|
+|<math>\rm KPi^\omega+(\Sigma-FOUND)</math><br><math>\rm KPi^\omega+(\Sigma-REC)</math>
-|
-|
 |-
-|
+|<math>\psi_{\Omega_1}(\varepsilon_{I+1})</math>
-|
+|<math>\rm \Delta_2^1-CA+BI</math><br><math>\rm \Sigma_2^1-AC+BI</math>
-|
+|<math>\rm KPi</math><br><math>{\rm KP}\beta</math><br><math>\rm CZF+REA</math>
-|
+|<math>\rm T_0</math>
-|-
-|
-|
-|
-|
-|-
-|
-|
-|
-|
 |-
+|<math>\psi_{\Omega_1}(\Omega_{I+\omega})</math>
 |
-|
+|<math>\rm KPi^+</math>
-|
+|<math>\rm ML_1\ W</math><br><math>\rm KP_1\ W</math><br><math>\rm IARI</math>
-|
 |-
-|
+|<math>\psi_{\Omega_1}(\varepsilon_{M+1})</math>
-|
+|<math>\rm \Delta_2^1-CA+BI+(M)</math>
-|
+|<math>\rm KPM</math><br><math>\rm CZFM</math>
 |
 |-
+|<math>\psi_{\Omega_1}(\Omega_{M+\omega})</math>
 |
-|
+|<math>\rm KPM^+</math>
-|
+|<math>\rm MLM</math><br><math>\rm Agda</math>
-|
 |-
-|
+|<math>\Psi_{\Omega_1}^0(\varepsilon_{K+1})</math>
-|
+|<math>{\rm ACA+BI}+\Pi_4^1-\beta\text{-model-Reflection}</math>
-|
+|<math>{\rm KP}+\Pi_3^{\rm set}\text{-Reflection}</math>
 |
 |-
-|
+|<math>\Psi_\mathbb{X}^{\varepsilon_{\xi_n+1}}</math>
-|
+|<math>{\rm ACA+BI}+\Pi_{n+5}^1-\beta\text{-model-Reflection}</math>
-|
+|<math>{\rm KP}+\Pi_{n+4}^{\rm set}\text{-Reflection}</math>
 |
 |-
-|
+|<math>\Psi_\mathbb{X}^{\varepsilon_{\Xi+1}}</math>
-|
+|<math>{\rm ACA+BI}-\beta\text{-model-Reflection}</math>
-|
+|<math>{\rm KP}+\Pi_\omega^{\rm set}\text{-Reflection}</math>
 |
 |-
+|<math>\Psi_\mathbb{H}^{\varepsilon_{\Upsilon+1}}</math>
 |
-|
+|<math>{\rm KPi}+\forall\alpha\exists\kappa(L_\kappa\prec_1L_{\kappa+\alpha})</math>
-|
 |
 |-
-|
+|<math>\psi(\Omega_{\mathbb{S}+\omega})</math>
-|
+|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-CA^-</math>
-|
+|<math>{\rm KPl}^r+\exists M(\text{Trans}(M)\land M\prec_1 V)</math>
 |
 |-
-|
+|<math>\Psi_\mathbb{K}^{\varepsilon_{I+1}}</math>
-|
+|<math>\rm \Delta_2^1-CA+BI+\Pi_2^1-CA^-</math>
-|
+|<math>{\rm KPi}+\exists M(\text{Trans}(M)\land M\prec_1 V)</math>
 |
 |-
-|
+|<math>\mathcal{I}_\omega\cap\omega_1^{\rm CK}</math>
-|
+|<math>\rm \Pi_2^1-CA_0</math><br><math>\rm \Delta_3^1-CA_0</math>
 |
 |
 |-
-|
+|<math>\mathcal{I}_{\omega+1}\cap\omega_1^{\rm CK}</math>
-|
+|<math>\rm \Pi_2^1-CA+BI</math>
-|
+|<math>\rm KP+\Sigma_1^{set}-Separation</math><br><math>{\rm KPi}+\forall\alpha\exists\beta(\beta>\alpha)(\beta\text{ stable})</math>
 |
 |-
-|
+|<math>\mathcal{I}_{\varepsilon_0}\cap\omega_1^{\rm CK}</math>
-|
+|<math>\rm \Delta_3^1-CA</math><br><math>\rm \Sigma_3^1-AC</math>
 |
 |
 |-
-|
+|<math>\text{maybe }\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math>
-|
+|<math>\rm \Delta_3^1-CA+BI</math><br><math>\rm \Sigma_3^1-AC+BI</math><br><math>\rm \Sigma_3^1-DC+BI</math>
-|
+|<math>{\rm KP}+\Delta_2^{\rm set}\text{-Separation}</math>
 |
 |-
+|<math>\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math>
 |
-|
+|<math>{\rm KP}+\Pi_1^{\rm set}\text{-Collection}</math>
-|
 |
 |-
 |
-|
+|<math>\Pi_{n+3}^1{\rm-CA+BI}</math>
-|
+|<math>{\rm KP}+\Sigma_{n+2}^{\rm set}\text{-Separation}</math>
 |
 |-
 |
-|
+|<math>\Pi_{n+3}^1{\rm-CA}+\Sigma_{n+3}^1{\rm-AC+BI}</math>
-|
+|<math>{\rm KP^-}+\Sigma_{n+2}^{\rm set}\text{-Separation}+\Sigma_{n+2}^{\rm set}\text{-Collection}</math>
 |
 |-
 |
-|
+|<math>\rm Z_2=\Pi_\infty^1-CA</math><br><math>\rm \Delta_1^2-CA_0</math><br><math>\rm Z_2+\Sigma_\infty^1-AC</math>
-|
+|<math>{\rm KP}+\Sigma_\omega^{\rm set}\text{-Separation}</math><br><math>{\rm KP^-}+\Sigma_\omega^{\rm set}\text{-Separation}+\Sigma_\omega^{\rm set}\text{-Collection}</math><br><math>\rm ZFC^-=ZFC-Powerset</math>
 |
 |-
 |
-|
+|<math>{\rm Z}_{n+3}=\Pi_\infty^{n+2}{\rm-CA}</math><br><math>\Delta_1^{n+3}{\rm-CA_0}</math>
-|
+|<math>{\rm ZFC^-+V=L+}\exists\omega_{n+1}</math>
 |
 |-
 |
-|
+|<math>\rm Z_\infty=\Pi_0^\infty-CA</math>
-|
+|<math>\rm Z</math><br><math>\rm ZC</math><br><math>\rm IZ</math>
 |
 |-
 |
 |
+|<math>\rm IZF=CZF+Powerset+\Pi_\omega^{set}-Reflection</math><br><math>\rm ZF=CZF+LEM=IZF+LEM</math><br><math>\rm ZFC</math><br><math>\rm ZFC+V=L</math><br><math>\rm AST</math><br><math>\rm IST</math><br><math>\rm NBG=GBC</math><br><math>\rm GB</math>
 |
-|
+|}
+ZFC 相关证明论序数：
+* <math>\mathrm{S}_0 = (\mathrm{Ext}) + (\mathrm{Null}) + (\mathrm{Pair}) + (\mathrm{Union}) + (\mathrm{Diff})\ (\text{Rudimentary set theory})</math>
+* <math>\mathrm{S}_1 = \mathrm{S}_0 + (\mathrm{Powerset})</math>
+* <math>\mathrm{M}_0 = \mathrm{S}_1 + (\Delta_0^{\mathrm{set}} - \mathrm{Separation})</math>
+* <math>\mathrm{M}_1 = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Transitive\ Containment})</math>
+* <math>\mathrm{KP}^- = \mathrm{S}_0 + (\mathrm{Infinity}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
+* <math>\mathrm{KP}^{-\infty} = \mathrm{S}_0 + (\mathrm{Foundation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Separation}) + (\Delta_0^{\mathrm{set}} - \mathrm{Collection})</math>
+* <math>\mathrm{KP} = \mathrm{KP}^{-\infty} + (\mathrm{Infinity}) = \mathrm{KP}^- + (\mathrm{Foundation})</math>
+* <math>\mathrm{KPl} = \mathrm{KP} + (\text{universe limit of admissible sets})</math>
+* <math>\mathrm{KPi} = \mathrm{KP} + (\text{recursively inaccessible universe})</math>
+* <math>\mathrm{KPh} = \mathrm{KP} + (\text{recursively hyperinaccessible universe})</math>
+* <math>\mathrm{KPM} = \mathrm{KP} + (\text{recursively Mahlo universe})</math>
+* <math>\mathrm{ZBQC} = \mathrm{M}_0 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\mathrm{Choice})</math><br><math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
+* <math>\mathrm{MAC} = \mathrm{M}_1 + (\mathrm{Infinity}) + (\mathrm{Choice}) = \mathrm{ZBQC} + (\text{Transitive Containment})</math>
+* <math>\mathrm{MOST} = \mathrm{MAC} + (\Delta_0^{\mathrm{set}} - \mathrm{Collection}) = \mathrm{ZBQC} + \mathrm{KP} + (\Sigma_1^{\mathrm{set}} - \mathrm{Separation})</math>
+* <math>\mathrm{Z} = \mathrm{S}_1 + (\mathrm{Regularity}) + (\mathrm{Infinity}) + (\Sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
+* <math>\mathrm{ZC} = \mathrm{Z} + (\mathrm{Choice}) = \mathrm{ZBQC} + (\sigma_\omega^{\mathrm{set}} - \mathrm{Separation})</math>
+* <math>\mathrm{MAC} + \forall m (\beth_{\beth_{m}}\text{ exists})</math><br><math>\mathrm{NFU} + (\mathrm{Infinity}) + (\mathrm{Choice})</math>
+* <math>\mathrm{Z} + (\Pi_2^{\mathrm{set}} - \mathrm{Replacement})</math><br><math>\mathrm{NFU}^* = \mathrm{NFU} + (\mathrm{Counting}) + (\mathrm{Strongly\ Cantorian\ Separation})</math>
+* <math>\mathrm{Z} + (\Pi_m^{\mathrm{set}} - \mathrm{Replacement})</math>
+* <math>\mathrm{ZF} = \mathrm{Z} + (\Pi_\omega^{\mathrm{set}} - \mathrm{Replacement})</math><br><math>\mathrm{AST}</math><br><math>\mathrm{GB}</math>
+* <math>\mathrm{ZFC} = \mathrm{ZF} + (\text{Choice})</math><br><math>\mathrm{NBG} = \mathrm{GBC} = \mathrm{GB} + (\text{Global Choice})</math>
+* <math>\mathrm{ZFC} + (\text{there is a worldly cardinal})</math>
+* <math>\mathrm{NBG} + (\text{there is a stationary proper class of worldly cardinals})</math>
+* <math>\mathrm{NBG} + (\text{Class Forcing Theorem})</math><br><math>\mathrm{NBG} + (\text{Clopen Class Game Determinacy})</math>
+* <math>\mathrm{MK} = \mathrm{NBG} + (\Pi_{\infty}^{\mathrm{class}} - \mathrm{CA})</math>
+* <math>\mathrm{ZFC} + (\text{there is an inaccessible cardinal})</math><br><math>\mathrm{ZFC} + (\Pi_{1}^{1}\ \text{Perfect Set Property})</math><br><math>\mathrm{ZFC} + (\Sigma_{3}^{1}\ \text{Lebesgue measurability})</math>
+* <math>\mathrm{ZFC} + (\text{there are } \omega\ \text{inaccessible cardinals})</math><br><math>\mathrm{ZFC} + (\forall\alpha(\omega \leq \alpha \leq \aleph_{\omega} \Rightarrow |\mathrm{V}_{\alpha} \cap L| = |\alpha|))</math>
+* <math>\mathrm{ZFC} + (\text{there is a proper class of inaccessible cardinals})</math><br><math>\mathrm{ZFC} + (\text{Grothendieck Universe Axiom})</math>
+* <math>\mathrm{ZFC} + (\text{there is a } \Sigma_{n}^{\mathrm{set}}\text{-reflecting cardinal})</math>
+* <math>\mathrm{ZFC} + (\text{there is a } \sigma_{\omega}^{\mathrm{set}}\text{-reflecting cardinal})</math><br><math>\mathrm{ZFC} + (\text{Ord is Mahlo})</math>
+* <math>\mathrm{ZFC} + (\text{there is an uplifting cardinal})</math><br><math>\mathrm{ZFC} + (\text{Resurrection Axioms})</math>
+* <math>\mathrm{ZFC} + (\text{there is a Mahlo cardinal})</math>
+* <math>\mathrm{SMAH} = \mathrm{ZFC} + (\text{there is a } n\text{-Mahlo cardinal})_{n\in\mathbb{N}}</math><br><math>\mathrm{NFUA} = \mathrm{NFU} + (\text{Infinity}) + (\text{Cantorian Sets})</math>
+* <math>\mathrm{SMAH}^{+} = \mathrm{ZFC} + \forall n(\text{there is a } n\text{-Mahlo cardinal})</math>
+* <math>\mathrm{MK} + (\text{Ord is weakly compact})</math><br><math>\mathrm{GPK}_{\infty}^{+} = \mathrm{GPK}^{+} + (\text{Infinity})</math><br><math>\mathrm{NFUB} =\mathrm{NFU} +(\text{Infinity}) + (\text{Cantorian Sets}) + (\text{Small Ordinals})</math>
+* <math>\mathrm{ZFC} + (\text{there is a weakly compact cardinal})</math><br><math>\mathrm{ZFC} + (\omega_{2}\ \text{has the tree property})</math>
+* <math>\mathrm{ZFC} + (\text{there is a totally indescribable cardinal})</math>
+* <math>\mathrm{ZFC} + (\text{there is a subtle cardinal})</math>
+* <math>\mathrm{ZFC} + (\text{there is an ineffable cardinal})</math>
+* <math>\mathrm{ZFC} + \forall\alpha(\alpha < \omega_{1} \Rightarrow \text{there is a } \alpha\text{-Erdős cardinal})</math>
+* <math>\mathrm{ZFC} + (0^{\sharp}\ \text{exists})</math><br><math>\mathrm{ZFC} + (L \models \aleph_{\omega}\ \text{is regular})</math><br><math>\mathrm{ZFC} + \forall \alpha (\alpha \geq \omega \Longrightarrow |V_{\alpha} \cap L| = |\alpha|)</math><br><math>\mathrm{ZFC} + (\text{parameter-free } \Sigma_{1}^{1}\text{-determinacy})</math>
+* <math>\mathrm{ZFC} + \forall x\ (x \in \mathbb{R} \Longrightarrow x^{\sharp}\ \text{exists})</math><br><math>\mathrm{ZFC} + (\Sigma_{1}^{1}\text{-determinacy})</math>
+* <math>\mathrm{ZFC} + \forall x\ (x^{\sharp}\ \text{exists})</math><br><math>\mathrm{ZFC} + (\Sigma_{2}^{1}\ \text{universal Baireness})</math>
+* <math>\mathrm{ZFC} + (\text{there is an } \omega_{1}\text{-Erdős cardinal})</math><br><math>\mathrm{ZFC} + (\text{Chang's Conjecture})</math>
+* <math>\mathrm{SRP} = \mathrm{ZFC} + (\text{there is cardinal with the } n\text{-stationary Ramsey property})_{n \in \mathbb{N}}</math>
+* <math>\mathrm{SRP}^{+} = \mathrm{ZFC} + \forall n\ (\text{there is a cardinal with the } n\text{-stationary Ramsey property})</math>
+* <math>\mathrm{MK} + (\text{Ord is measurable})</math><br><math>\mathrm{NFUM} = \mathrm{NFU} + (\text{Infinity}) + (\text{Large Ordinals}) + (\text{Small Ordinals})</math>
+* <math>\mathrm{ZFM} = \mathrm{ZFC} + (\text{there is a measurable cardinal})</math><br><math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is precipitous})</math><br><math>\mathrm{ZF} + (\omega_{1}\ \text{is measurable})</math>
+* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = 2)</math><br><math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{2}}\ \text{is precipitous})</math>
+* <math>\mathrm{ZFC} + (\text{there is a measurable cardinal } \kappa\ \text{such that } o(\kappa) = \kappa^{++})</math><br><math>\mathrm{ZFC} + \neg \mathrm{SCH}</math><br><math>\mathrm{ZFC} + (2^{\aleph_{\omega}} = \aleph_{\omega + 2})</math>
+* <math>\mathrm{ZFC} + (\text{Ord is Woodin})</math><br><math>\mathrm{ZFC} + \neg \mathrm{SCH}</math><br><math>\mathrm{Z}_{2} + (\Delta_{2}^{1}\text{-determinacy})\ (\text{conjectural})</math>
+* <math>\mathrm{MK} + (\text{Ord is Woodin})</math><br><math>\mathrm{ZFC} + \neg \mathrm{SCH}</math><br><math>\mathrm{Z}_{3}+ (\text{lightface } \Delta_{2}^{1}\text{-determinacy})</math>
+* <math>\mathrm{NBG} + (\text{Ord is Woodin})</math><br><math>\mathrm{ZFC} + \neg \mathrm{SCH}</math><br><math>\mathrm{Z}_{3}+ (\Delta_{2}^{1}\text{-determinacy})</math>
+* <math>\mathrm{ZFC} + (\text{there is a Woodin cardinal})</math><br><math>\mathrm{ZFC} + (\Delta_{2}^{1}\text{-determinacy})</math><br><math>\mathrm{ZFC} + (\mathrm{OD} \models \mathrm{AD})</math><br><math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_{1}}\ \text{is } \omega_{2}\text{-saturated})</math>
+* <math>\mathrm{ZFC} + (\text{there are } n\ \text{Woodin cardinals})_{n \in \mathbb{N}}</math><br><math>\mathrm{Z}_{2} + (\mathrm{PD})</math>
+* <math>\mathrm{ZFC} + (\text{there are } \omega \text{ Woodin cardinals})</math><br><math>\mathrm{ZF} + (\mathrm{AD})</math><br><math>\mathrm{ZFC} + (L(\mathbb{R}) \models \mathrm{AD})</math><br><math>\mathrm{ZFC} + (\mathrm{OD}(\mathbb{R}) \models \mathrm{AD})</math>
+* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\omega_1)\text{-strongly compact})</math><br><math>\mathrm{ZFC} + (\mathrm{NS}_{\omega_1} \text{ is } \omega_1\text{-dense})</math>
+* <math>\mathrm{ZF} + \mathrm{DC} + (\omega_1 \text{ is } \mathcal{P}(\mathbb{R})\text{-strongly compact})</math><br><math>\mathrm{ZF} + \mathrm{DC} + (\mathrm{AD}_{\mathbb{R}})</math>
+* <math>\mathrm{ZFC} + \text{(there is a superstrong cardinal)}</math>
+* <math>\mathrm{ZFC} + \text{(there is a subcompact cardinal)}</math><br><math>\mathrm{ZFC} + (V = L[\vec{E}]) + \exists\kappa(\neg\square_{\kappa})</math>
+* <math>\mathrm{ZFC} + \text{(there is a strongly compact cardinal)}</math><br><math>\mathrm{ZFC} + \text{(Proper Forcing Axiom)}</math>
+* <math>\mathrm{ZFC} + \text{(there is a supercompact cardinal)}</math><br><math>\mathrm{ZFC} + \text{(Martin's Maximum)}</math>
+* <math>\mathrm{ZFC} + \forall n \text{(there is a proper class of } C^{(n)}\text{-extendible cardinals)}</math><br><math>\mathrm{ZFC} + \text{(Vopěnka's Principle)}</math>
+* <math>\mathrm{ZFC} + \text{(there is a high-jump cardinal)}</math>
+* <math>\mathrm{HUGE} = \mathrm{ZFC} + \text{( there is a } n\text{-huge cardinal )}_{n\in\mathbb{N}}</math>
+* <math>\mathrm{ZFC} + \text{(Wholeness Axiom } \mathrm{WA}_n)</math>
+* <math>\mathrm{ZFC} + \mathrm{I}3 = \mathrm{ZFC} + \exists\lambda(E_0(\lambda))</math>
+* <math>\mathrm{ZFC} + \mathrm{I}2 = \mathrm{ZFC} + \exists\lambda(E_1(\lambda))</math>
+* <math>\mathrm{ZFC} + \mathrm{I}1 = \mathrm{ZFC} + \exists\lambda(E_{\omega}(\lambda))</math>
+* <math>\mathrm{ZFC} + \mathrm{I}0</math>
+* <math>\mathrm{ZF} + \mathrm{DC} + \exists\lambda\exists j : V_{\lambda + 2} \prec_{\Sigma_{\omega}^{\mathrm{set}}} V_{\lambda + 2}</math>
+* <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math>
+* <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math>
-|}
+[[分类:集合论相关]]