打开/关闭菜单
打开/关闭外观设置菜单
打开/关闭个人菜单
未登录
未登录用户的IP地址会在进行任意编辑后公开展示。

证明论序数

来自Googology Wiki

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

定义和性质

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

证明论序数满足:

  1. 对任意递归序数 β<|T|,理论 T 能证明“所有序数小于 β 的原始递归良序关系都是良序的”;对 α=|T|,理论 T 无法证明“所有序数小于 α 的原始递归良序关系都是良序的”。
  2. 存在一种递归记号系统,自然表示所有小于 |T| 的序数;理论 T 能通过超限归纳(序数是良序集的序型,满足超限归纳原理:∀α(∀β<α(P(β)⇒P(α))⇒∀αP(α)),其中 P 是任意性质)到 |T|,证明自身的一致性(即 T⊬⊥);理论 T 能证明所有初等递归函数在小于 |T| 的序数上总停止;对任意递归序数 β<|T|,至少不满足上述条件中的一条。
  3. 证明论序数必为递归序数(recursive ordinal),即存在递归关系定义其良序。

证明论序数表

证明论序数(OCF及其他记号) 证明论序数(BMS及其他记号) 算术论体系 集合论体系 其他体系
ω (0)(1) Q KP−
ω2 (0)(1)(1) RFA
IΔ0
ω3 (0)(1)(1)(1) RCA0*
WKL0*
IΔ0+exp
ωn (0)(1)^n IΔ0+ℰn is total
ωω (0)(1)(2) RCA0
WKL0
PRA
RCA02
CPRC
KP−+Π1set Fondation+IND
ωωωω (0)(1)(2)(3)(4) RCA0+(Π20)−−IND
ω↑↑(n+2) (0)(1)(2)...(n+2) IΣn+1
ε0 (0)(1,1) PA
ACA0
Δ11−CA0
Σ11−AC0
KP−∞ EM0
ε1 (0)(1,1)(1,1) ACA0+KPHT
εω (0)(1,1)(2) ACA0+iRT
RCA0+∀Y∀n∃X(TJ(n,X,Y))
εε0 (0)(1,1)(2)(3,1) ACA
FPn−ACA'0
FPn−ACA′
ζ0 (0)(1,1)(2,1) ACA0+∀X∃Y(TJ(ω,X,Y))
ACA0+(BR)
p1(ACA0)
φ(2,ε0) (0)(1,1)(2,1)(2)(3,1) ACA+∀X∃Y(TJ(ω,X,Y))
RFN
φ(ω,0) (0)(1,1)(2,1)(3) Δ11−CR
RCA0*+Π11−CA−
Σ11−DC0
ID1#
EM0+JR
PID
Acc−ID(Acc)
(Π00(P),P∪N)−ID
(Π00(P),P∧N)−ID(Acc)
φ(ν+1,0) ACA0+∀X∃Y(TJ(ων,X,Y))
ψ(Ωε0) (0)(1,1)(2,1)(3)(4,1) Δ11−CA
Σ11−AC
(Π10−CA)<ε0
ψ(Ωψ(Ωω)) (0)(1,1)(2,1)(3)(4,1)(5,1)(6) PRS ω
Γ0 (0)(1,1)(2,1)(3,1) ATR0
Δ11−CA+BR
RCA0+Σ10−RT
RCA0+Δ10−RT
RCA0+Σ10−det.
RCA0+Δ10−det.
FP0
KPi−
CZF−+INAC
ID^<ω
ID^*
ML<ω
MLU
U(PA)
φ(1,0,ωω) (0)(1,1)(2,1)(3,1)(2)(3) KPl0+(Σ1−Iω)
φ(1,0,ε0) (0)(1,1)(2,1)(3,1)(2)(3,1) ATR ID^ω
ψ(ΩΩ+1) (0)(1,1)(2,1)(3,1)(2,1) RCA0+∀X∃M(X∈M∧M⊨ωATR0)
ψ(ΩΩ+ω) (0)(1,1)(2,1)(3,1)(2,1)(3) ATR0+Σ11−DC ID^<ωω
ψ(ΩΩ+ε0) (0)(1,1)(2,1)(3,1)(2,1)(3)(4,1) ATR+Σ11−DC ID^<ε0
ψ(ΩΩ+Γ0) (0)(1,1)(2,1)(3,1)(2,1)(3)(4,1)(5,1)(6,1) ID^<Γ0
MLS
φ(2,0,0) (0)(1,1)(2,1)(3,1)(2,1)(3,1) FTR0 KPh− Aut(ID^)
φ(2,0,ε0) (0)(1,1)(2,1)(3,1)(2,1)(3,1)(2)(3,1) FTR
φ(2,ε0,0) (0)(1,1)(2,1)(3,1)(2,1)(3,1)(2,1)(3)(4,1) KPh0+(F−Iω)
ψ(ΩΩω) (0)(1,1)(2,1)(3,1)(3) KPM−
φ(ε0,0,0) (0)(1,1)(2,1)(3,1)(3)(4,1) Σ11−TDC
φ(1,0,0,0) (0)(1,1)(2,1)(3,1)(3,1) p1(Σ11−TDC0)
ψ(ΩΩω) (0)(1,1)(2,1)(3,1)(4) RCA0*+Π11−CA−
p3(ACA0)
FIT
TID
ϑ(ΩΩ) (0)(1,1)(2,1)(3,1)(4,1) p1(p3(ACA0))
θ(n+2)(Ωω)0 ACA0+Πn+21−BI
Πn+11−RFN
(Πn+21−BI)0
(Πn+21−BI)0−
KPω−+Πn+2set−Foundation
θ(n+2)(Ωω)0 ACA+Πn+21−BI
(Πn+21−BI)−
KPω−+IND+Πn+2set−Foundation
ψ(ψ1(0)) (0)(1,1)(2,2) ACA+BI
ACA0+Π11−CA−
Π10−FXP0
KP
KP+Π2set−Reflection
KP+(BI*)
KP+(ATR0*)
CZF
KPω2↾+Δ1−CA+sΠ11−ref
ID1
ID12
ML1 V
ψ(Ω2) (0)(1,1)(2,2)(3,2) RCA0+∀X∃M(X∈M∧M⊨ωACA+BI)
ψ(Ω2Ω2) (0)(1,1)(2,2)(3,2)(4,2) ATR0∙
FP0∙
Σ11−DC0∙+(SUB∙)
Σ11−AC0∙+(SUB∙)
ID^<ω∙𝒰(ID1)
ψ(ψ2(0)) (0)(1,1)(2,2)(3,3) KP+∃ω1CK ID2
ID22
ψ(Ωω) (0)(1,1,1) Π11−CA0
Δ21−CA0
RCA0+Σ10∧Π10−det.
RCA0+Δ20−RT
KPlr
KPir
KPβr
ID<ω
(ID<ω2)0
ψ(Ωω⋅ωω) (0)(1,1,1)(2)(3) Π11−CA0+Π21−IND
ψ(Ωω⋅ε0) (0)(1,1,1)(2)(3,1) Π11−CA W−KPl W−IDω
ID<ω2
ψ(Ωω⋅Ω) (0)(1,1,1)(2,1) Π11−CA+BR
ψ(Ωωω) (0)(1,1,1)(2,1)(3) Π11−CA0+Π21−BI
ψ(Ωωωω) (0)(1,1,1)(2,1)(3)(4) Π11−CA0+Π21−BI+Π31−IND
ψ(ψω(0)) (0)(1,1,1)(2,1)(3,2) Π11−CA+BI KPl IDω
BIDω2
ψ(Ωωω) (0)(1,1,1)(2,1,1)(3) Δ21−CR
(Π11−CA<ωω)
KPlωωr ID<ωω
ψ(Ωε0) (0)(1,1,1)(2,1,1)(3)(4,1) Δ21−CA
Σ21−AC
(Π11−CA<ε0)
KPlε0r
W−KPi
W−KPβ
ID<ε0
ID<ε02
BID<ε02
ψ(Ων⋅ω) (Π11−CAν+)0 KPlν+r ID<ν⋅ω
(PIDν2)0
ψ(Ωγ⋅ω) (Π11−CAγ−)0 KPlγr (NUIDγ2)0
ψ(Ων⋅ω⋅ε0)) Π11−CAν+ W−KPlν+ W−IDν⋅ω
PIDν2
ψ(Ωγ⋅ε0) (Π11−CAγ)
Π11−CAγ−
W−KPlγ W−IDγ
IDγ2
NUIDγ2
ψ(Ων⋅ω⋅Ω)) Π11−CAν++BR PIDν2+BR
ψ(Ωγ⋅Ω) Π11−CAγ−+BR NUIDγ2+BR
ψ(Ωωγ) (Π11−CAωγ)0
(Π11−CA<ωγ)
(Π11−CA<ωγ)+BI
(IDωγ2)0
ID<ωγ
BID<ωγ2
(ID<ν2)+BI
ψ(ψν(0)) (Π11−CAν)0 KPlν IDν
(IDν2)0
ψ(ψν(ε0)) Π11−CAν IDν2
ψ(ψν(Ω)) Π11−CAν+BR IDν2+BR
ψ(ψν(ψν(0))) BIDν2
ψ(ψν+1(0)) Π11−CAν+BI KPlν+1 IDν+1
IDν2+BI
ψ(ψν⋅ω(0)) Π11−CAν++BI KPlν+ IDν⋅ω
PIDν2+BI
PBIDν2
ψ(ψγ(0)) (Π11−CAγ)0
(Π11−CAγ)+BI
Π11−CAγ−+BI
KPlγ IDγ
(IDγ2)0
IDγi(𝒪)BIDν2
IDγ2+BI
NUIDγ2+BI
ψ(ψΩ(0)) (0)(1,1,1)(2,1,1)(3,1) KPl*
KPlΩr
ID≺*
BID2*
ID2*+BI2
ψΩ1(ψI(0)) (0)(1,1,1)(2,1,1)(3,1)(2) Π11−TR0
Π11−TR0+Δ21−CA0
Δ21−CA+BI(impl Σ21)
Δ21−CA+BR(impl Σ21)
RCA0+Δ20−det.
RCA0+Δ11−RT
Aut−KPlr
Aut−KPlr+KPir
KPiω+FOUNDR(impl−Σ)
KPiω+FOUND(impl−Σ)
Aut−ID0pos
Aut−ID0mon
ψΩ1(ψI(0)⋅ε0) (0)(1,1,1)(2,1,1)(3,1)(2)(3,1) Π11−TR W−Aut−KPl Aut−IDpos
Aut−IDmon
Aut−KPlω
ψΩ1(ψΩψI(0)+1(0)) (0)(1,1,1)(2,1,1)(3,1)(2,1)(3,2) Π11−TR+BI Aut−KPl Aut−ID2pos
Aut−ID2mon
Aut−BID
ψΩ1(ψI(Iω)) (0)(1,1,1)(2,1,1)(3,1)(3) Δ21−TR0
Σ21−TRDC0
Δ21−CA0+Σ21−BI
KPir+(Σ−FOUND)
KPir+(Σ−REC)
ψΩ1(ψI(Iε0)) (0)(1,1,1)(2,1,1)(3,1)(3)(4,1) Δ21−TR
Σ21−TRDC
Δ21−CA+Σ21−BI
KPiω+(Σ−FOUND)
KPiω+(Σ−REC)
ψΩ1(εI+1) (0)(1,1,1)(2,1,1)(3,1)(4,2) Δ21−CA+BI
Σ21−AC+BI
KPi
KPβ
CZF+REA
T0
ψΩ1(ΩI+ω) (0)(1,1,1)(2,1,1)(3,1)(4,2,1) KPi+ ML1 W
KP1 W
IARI
ψΩ1(εM+1) (0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2) Δ21−CA+BI+(M) KPM
CZFM
ψΩ1(ΩM+ω) (0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2,1) KPM+ MLM
Agda
ΨΩ10(εK+1) (0)(1,1,1)(2,1,1)(3,1,1)(4,1)(5,2) ACA+BI+Π41−β-model-Reflection KP+Π3set-Reflection
Ψ𝕏εξn+1 (0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5,1)(6,2)? ACA+BI+Πn+51−β-model-Reflection KP+Πn+4set-Reflection
Ψ𝕏εΞ+1 (0)(1,1,1)(2,2) ACA+BI−β-model-Reflection KP+Πωset-Reflection
ΨℍεΥ+1 (0)(1,1,1)(2,2)(3,2)(4,1)(2) KPi+∀α∃κ(Lκ≺1Lκ+α)
ψ(Ω𝕊+ω) Π11−CA0+Π21−CA− KPlr+∃M(Trans(M)∧M≺1V)
Ψ𝕂εI+1 Δ21−CA+BI+Π21−CA− KPi+∃M(Trans(M)∧M≺1V)
ℐω∩ω1CK (0)(1,1,1,1)? Π21−CA0
Δ31−CA0
ℐω+1∩ω1CK (0)(1,1,1,1)(2,1,1)(3,2,2)? Π21−CA+BI KP+Σ1set−Separation
KPi+∀α∃β(β>α)(β stable)
ℐε0∩ω1CK (0)(1,1,1,1)(2,1,1,1)(3)(4,1)? Δ31−CA
Σ31−AC
maybe ψΩ(ε𝕀+1) Δ31−CA+BI
Σ31−AC+BI
Σ31−DC+BI
KP+Δ2set-Separation
ψΩ(ε𝕀+1) KP+Π1set-Collection
Πn+31−CA+BI KP+Σn+2set-Separation
Πn+31−CA+Σn+31−AC+BI KP−+Σn+2set-Separation+Σn+2set-Collection
≥Y(1,3) Z2=Π∞1−CA
Δ12−CA0
Z2+Σ∞1−AC
KP+Σωset-Separation
KP−+Σωset-Separation+Σωset-Collection
ZFC−=ZFC−Powerset
>ω-Y(1,ω) KP+ω1
Π12−CA0
Zn+3=Π∞n+2−CA
Δ1n+3−CA0
ZFC−+V=L+∃ωn+1
Z∞=Π0∞−CA Z
ZC
IZ
IZF=CZF+Powerset+Πωset−Reflection
ZF=CZF+LEM=IZF+LEM
ZFC
ZFC+V=L
AST
IST
NBG=GBC
GB

ZFC 相关证明论序数: 注意:看不懂的,其实这个是从上往下,从弱到强排序的

  • S0=(Ext)+(Null)+(Pair)+(Union)+(Diff) (Rudimentary set theory)
  • S1=S0+(Powerset)
  • M0=S1+(Δ0set−Separation)
  • M1=M0+(Regularity)+(Transitive Containment)
  • KP−=S0+(Infinity)+(Δ0set−Separation)+(Δ0set−Collection)
  • KP−∞=S0+(Foundation)+(Δ0set−Separation)+(Δ0set−Collection)
  • KP=KP−∞+(Infinity)=KP−+(Foundation)
  • KPl=KP+(universe limit of admissible sets)
  • KPi=KP+(recursively inaccessible universe)
  • KPh=KP+(recursively hyperinaccessible universe)
  • KPM=KP+(recursively Mahlo universe)
  • ZBQC=M0+(Regularity)+(Infinity)+(Choice)
    NFU+(Infinity)+(Choice)
  • MAC=M1+(Infinity)+(Choice)=ZBQC+(Transitive Containment)
  • MOST=MAC+(Δ0set−Collection)=ZBQC+KP+(Σ1set−Separation)
  • Z=S1+(Regularity)+(Infinity)+(Σωset−Separation)
  • ZC=Z+(Choice)=ZBQC+(σωset−Separation)
  • MAC+∀m(ℶℶm exists)
    NFU+(Infinity)+(Choice)
  • Z+(Π2set−Replacement)
    NFU*=NFU+(Counting)+(Strongly Cantorian Separation)
  • Z+(Πmset−Replacement)
  • ZF=Z+(Πωset−Replacement)
    AST
    GB
  • ZFC=ZF+(Choice)
    NBG=GBC=GB+(Global Choice)
  • ZFC+(there is a worldly cardinal)
  • NBG+(there is a stationary proper class of worldly cardinals)
  • NBG+(Class Forcing Theorem)
    NBG+(Clopen Class Game Determinacy)
  • MK=NBG+(Π∞class−CA)
  • ZFC+(there is an inaccessible cardinal)
    ZFC+(Π11 Perfect Set Property)
    ZFC+(Σ31 Lebesgue measurability)
  • ZFC+(there are ω inaccessible cardinals)
    ZFC+(∀α(ω≤α≤ℵω⇒|Vα∩L|=|α|))
  • ZFC+(there is a proper class of inaccessible cardinals)
    ZFC+(Grothendieck Universe Axiom)
  • ZFC+(there is a Σnset-reflecting cardinal)
  • ZFC+(there is a σωset-reflecting cardinal)
    ZFC+(Ord is Mahlo)
  • ZFC+(there is an uplifting cardinal)
    ZFC+(Resurrection Axioms)
  • ZFC+(there is a Mahlo cardinal)
  • SMAH=ZFC+(there is a n-Mahlo cardinal)n∈ℕ
    NFUA=NFU+(Infinity)+(Cantorian Sets)
  • SMAH+=ZFC+∀n(there is a n-Mahlo cardinal)
  • MK+(Ord is weakly compact)
    GPK∞+=GPK++(Infinity)
    NFUB=NFU+(Infinity)+(Cantorian Sets)+(Small Ordinals)
  • ZFC+(there is a weakly compact cardinal)
    ZFC+(ω2 has the tree property)
  • ZFC+(there is a totally indescribable cardinal)
  • ZFC+(there is a subtle cardinal)
  • ZFC+(there is an ineffable cardinal)
  • ZFC+∀α(α<ω1⇒there is a α-Erdős cardinal)
  • ZFC+(0♯ exists)
    ZFC+(L⊨ℵω is regular)
    ZFC+∀α(α≥ω⟹|Vα∩L|=|α|)
    ZFC+(parameter-free Σ11-determinacy)
  • ZFC+∀x (x∈ℝ⟹x♯ exists)
    ZFC+(Σ11-determinacy)
  • ZFC+∀x (x♯ exists)
    ZFC+(Σ21 universal Baireness)
  • ZFC+(there is an ω1-Erdős cardinal)
    ZFC+(Chang's Conjecture)
  • SRP=ZFC+(there is cardinal with the n-stationary Ramsey property)n∈ℕ
  • SRP+=ZFC+∀n (there is a cardinal with the n-stationary Ramsey property)
  • MK+(Ord is measurable)
    NFUM=NFU+(Infinity)+(Large Ordinals)+(Small Ordinals)
  • ZFM=ZFC+(there is a measurable cardinal)
    ZFC+(NSω1 is precipitous)
    ZF+(ω1 is measurable)
  • ZFC+(there is a measurable cardinal κ such that o(κ)=2)
    ZFC+(NSω2 is precipitous)
  • ZFC+(there is a measurable cardinal κ such that o(κ)=κ++)
    ZFC+¬SCH
    ZFC+(2ℵω=ℵω+2)
  • ZFC+(Ord is Woodin)
    ZFC+¬SCH
    Z2+(Δ21-determinacy) (conjectural)
  • MK+(Ord is Woodin)
    ZFC+¬SCH
    Z3+(lightface Δ21-determinacy)
  • NBG+(Ord is Woodin)
    ZFC+¬SCH
    Z3+(Δ21-determinacy)
  • ZFC+(there is a Woodin cardinal)
    ZFC+(Δ21-determinacy)
    ZFC+(OD⊨AD)
    ZFC+(NSω1 is ω2-saturated)
  • ZFC+(there are n Woodin cardinals)n∈ℕ
    Z2+(PD)
  • ZFC+(there are ω Woodin cardinals)
    ZF+(AD)
    ZFC+(L(ℝ)⊨AD)
    ZFC+(OD(ℝ)⊨AD)
  • ZF+DC+(ω1 is 𝒫(ω1)-strongly compact)
    ZFC+(NSω1 is ω1-dense)
  • ZF+DC+(ω1 is 𝒫(ℝ)-strongly compact)
    ZF+DC+(ADℝ)
  • ZFC+(there is a superstrong cardinal)
  • ZFC+(there is a subcompact cardinal)
    ZFC+(V=L[E→])+∃κ(¬◻κ)
  • ZFC+(there is a strongly compact cardinal)
    ZFC+(Proper Forcing Axiom)
  • ZFC+(there is a supercompact cardinal)
    ZFC+(Martin's Maximum)
  • ZFC+∀n(there is a proper class of C(n)-extendible cardinals)
    ZFC+(Vopěnka's Principle)
  • ZFC+(there is a high-jump cardinal)
  • HUGE=ZFC+( there is a n-huge cardinal )n∈ℕ
  • ZFC+(Wholeness Axiom WAn)
  • ZFC+I3=ZFC+∃λ(E0(λ))
  • ZFC+I2=ZFC+∃λ(E1(λ))
  • ZFC+I1=ZFC+∃λ(Eω(λ))
  • ZFC+I0
  • ZF+DC+∃λ∃j:Vλ+2≺ΣωsetVλ+2
  • ZFj+DC+(there is a Reinhardt cardinal )
  • ZF+DC+(there is a Berkeley cardinal)

主流观点认为倒数第三个是相容的(只需要ZFC+I0是相容的),但是倒数第二和倒数第一个是不相容的(只需要终极L猜想成立即可)