证明论序数
| 证明论序数 | |
|---|---|
| 术语名称 | 证明论序数 |
| 英语名称 | proof-theoretic ordinal |
| 别名 | PTO |
通过形式系统的理论中能刻画的最复杂的良序来刻画理论的强度，该理论能表示的全体良序，其上界的序型，称为理论的证明论序数(proof-theoretic ordinal)。
定义
对理论 [math]\displaystyle{ T }[/math] ，若存在一个序数序列，对序数 [math]\displaystyle{ \alpha }[/math] ，对每个 [math]\displaystyle{ \beta\lt \alpha }[/math] ，理论 [math]\displaystyle{ T }[/math] 中可证明初始片段是良序的，则称 [math]\displaystyle{ \alpha }[/math] 是一个可表示序数。理论 [math]\displaystyle{ T }[/math] 中全体可表示序数的上界 [math]\displaystyle{ \operatorname{sup}\{\alpha\mid \alpha\text{可表示}\} }[/math] 称为理论 [math]\displaystyle{ T }[/math] 的证明论序数(proof-theoretic ordinal)，记作 [math]\displaystyle{ \mathsf{PTO}(T) }[/math] 。
举例
- Robinson 算术 [math]\displaystyle{ Q }[/math] （去掉自然数归纳公理模式的 Peano 算术），目前已知最弱的算术系统，有 [math]\displaystyle{ \mathsf{PTO}(Q)=\omega }[/math] 。
- Peano 算术 [math]\displaystyle{ \mathsf{PTO}(PA)=\varepsilon_0 }[/math] 。
- ZF 能用来证明能指出的全体良序集，其证明论强度不能通过序数分析衡量，需要使用模型论强度。 ZFC 在此基础上更强。
| 序数 | ||
|---|---|---|
| 构造 | 0 、后继序数、极限序数 | |
| 分类 | 有限序数（自然数）、可数序数、不可数序数；初始序数 | |
| 名称 | 不可分解点或不动点 | |
| 基本运算 | 后继 | 第一个超限序数 / [math]\displaystyle{ \omega }[/math] |
| 上确界 | - | |
| 算术运算 | 加法 [math]\displaystyle{ + }[/math] | 加性不可分解序数 / [math]\displaystyle{ \gamma }[/math] 数 |
| 乘法 [math]\displaystyle{ \cdot }[/math] | 乘性不可分解序数 / [math]\displaystyle{ \delta }[/math] 数 | |
| 乘方 [math]\displaystyle{ \bullet^\bullet }[/math] | [math]\displaystyle{ \varepsilon }[/math] 数 | |
| 更高阶运算 | [math]\displaystyle{ \zeta }[/math] 数、 [math]\displaystyle{ \theta }[/math] 数…… | |
| 其他运算 | Cantor 标准型 | - |
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |