证明论序数:修订间差异
来自Googology Wiki
更多操作
QuantumJack1(留言 | 贡献) →证明论序数表: BMS分析 |
QuantumJack1(留言 | 贡献) 无编辑摘要 |
||
| (未显示同一用户的2个中间版本) | |||
| 第451行: | 第451行: | ||
|- | |- | ||
|<math>\Psi_\mathbb{X}^{\varepsilon_{\xi_n+1}}</math> | |<math>\Psi_\mathbb{X}^{\varepsilon_{\xi_n+1}}</math> | ||
|(0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5 | |(0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5,1)(6,2) | ||
|<math>{\rm ACA+BI}+\Pi_{n+5}^1-\beta\text{-model-Reflection}</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>{\rm KP}+\Pi_{n+4}^{\rm set}\text{-Reflection}</math> | ||
| 第481行: | 第481行: | ||
|- | |- | ||
|<math>\mathcal{I}_\omega\cap\omega_1^{\rm CK}</math> | |<math>\mathcal{I}_\omega\cap\omega_1^{\rm CK}</math> | ||
| | |(0)(1,1,1,1)? | ||
|<math>\rm \Pi_2^1-CA_0</math><br><math>\rm \Delta_3^1-CA_0</math> | |<math>\rm \Pi_2^1-CA_0</math><br><math>\rm \Delta_3^1-CA_0</math> | ||
| | | | ||
| 第487行: | 第487行: | ||
|- | |- | ||
|<math>\mathcal{I}_{\omega+1}\cap\omega_1^{\rm CK}</math> | |<math>\mathcal{I}_{\omega+1}\cap\omega_1^{\rm CK}</math> | ||
| | |(0)(1,1,1,1)(2,1,1)(3,2,2)? | ||
|<math>\rm \Pi_2^1-CA+BI</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>\rm KP+\Sigma_1^{set}-Separation</math><br><math>{\rm KPi}+\forall\alpha\exists\beta(\beta>\alpha)(\beta\text{ stable})</math> | ||
| 第541行: | 第541行: | ||
|- | |- | ||
| | | | ||
| | |<math> \qquad \qquad \qquad \qquad \qquad </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> | |<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> | ||
2025年9月17日 (三) 01:41的最新版本
证明论序数(或称证明论强度序数,Proof-Theoretic Ordinal)是衡量形式理论强度的核心工具,通过将理论映射到序数上,刻画其能证明的良序关系的复杂度。该概念源于希尔伯特的证明论计划,旨在通过有限方法证明数学基础理论的一致性,后由阿克曼(Wilhelm Ackermann)和根岑(Gerhard Gentzen)发展为序数分析技术。
定义和性质
对形式理论 ,其证明论序数 ( 或 )定义为能用超限归纳证明的原始递归良序的序型最大值。
证明论序数满足:
- 对任意递归序数 ,理论 能证明“所有序数小于 的原始递归良序关系都是良序的”;对 ,理论 无法证明“所有序数小于 的原始递归良序关系都是良序的”。
- 存在一种递归记号系统,自然表示所有小于 的序数;理论 能通过超限归纳(序数是良序集的序型,满足超限归纳原理:,其中 是任意性质)到 ,证明自身的一致性(即 );理论 能证明所有初等递归函数在小于 的序数上总停止;对任意递归序数 ,至少不满足上述条件中的一条。
- 证明论序数必为递归序数(recursive ordinal),即存在递归关系定义其良序。
证明论序数表
| 证明论序数(OCF及其他记号) | 证明论序数(BMS及其他记号) | 算术论体系 | 集合论体系 | 其他体系 |
|---|---|---|---|---|
| (0)(1) | ||||
| (0)(1)(1) | ||||
| (0)(1)(1)(1) | ||||
| (0)(1)^n | ||||
| (0)(1)(2) | ||||
| (0)(1)(2)(3)(4) | ||||
| (0)(1)(2)...(n+2) | ||||
| (0)(1,1) | ||||
| (0)(1,1)(1,1) | ||||
| (0)(1,1)(2) | ||||
| (0)(1,1)(2)(3,1) | ||||
| (0)(1,1)(2,1) | ||||
| (0)(1,1)(2,1)(2)(3,1) | ||||
| (0)(1,1)(2,1)(3) | ||||
| (0)(1,1)(2,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3)(4,1)(5,1)(6) | ||||
| (0)(1,1)(2,1)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2)(3) | ||||
| (0)(1,1)(2,1)(3,1)(2)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3)(4,1)(5,1)(6,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3,1)(2)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3,1)(2,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3,1)(3) | ||||
| (0)(1,1)(2,1)(3,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3,1)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(4) | ||||
| (0)(1,1)(2,1)(3,1)(4,1) | ||||
| (0)(1,1)(2,2) | ||||
| (0)(1,1)(2,2)(3,2) | ||||
| (0)(1,1)(2,2)(3,2)(4,2) | ||||
| (0)(1,1)(2,2)(3,3) | ||||
| (0)(1,1,1) | ||||
| (0)(1,1,1)(2)(3) | ||||
| (0)(1,1,1)(2)(3,1) | ||||
| (0)(1,1,1)(2,1) | ||||
| (0)(1,1,1)(2,1)(3) | ||||
| (0)(1,1,1)(2,1)(3)(4) | ||||
| (0)(1,1,1)(2,1)(3,2) | ||||
| (0)(1,1,1)(2,1,1)(3) | ||||
| (0)(1,1,1)(2,1,1)(3)(4,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(2) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(2)(3,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(2,1)(3,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(3) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(3)(4,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(4,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(4,2,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(4,1)(5,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5,1)(6,2) | ||||
| (0)(1,1,1)(2,2) | ||||
| (0)(1,1,1)(2,2)(3,2)(4,1)(2) | ||||
| (0)(1,1,1,1)? | ||||
| (0)(1,1,1,1)(2,1,1)(3,2,2)? | ||||
| >=Y(1,3) | ||||
ZFC 相关证明论序数: