形式主义与多宇宙观（一） (6-6)

绝大多数的相对一致性证明，包括利用力迫法得到的关于集合论诸公理系统间的相对一致性证明甚至可以在原始递归算术（PRA）中得到，即上述证明转换程序往往是原始递归的。

按照一般理解，原始递归算术符合希尔伯特对有穷数学的要求。

因此，科里所谓关于形式系统之间关系的“元数学”大多可以被希尔伯特有穷数学覆盖。

我们知道，任何Σº₁的真命题都在皮亚诺算术甚至更弱的算术系统中可证明。

哥德尔不完全性定理告诉我们，任何一致的且足够的算术公理系统中总有不可证的∏º₁真命题。

但无论如何，关于形式系统的上述“元数学”命题不会超出一阶算术的范围。

科里在关于什么是“元数学”的界定中，的确还留下了进一步解释的空间。

他认为“涉及关系到外在（extraneous，相对于形式系统本身而言）考量或无穷主义假设的元定理，例如对塔斯基和哥德尔关于一阶谓词逻辑完全性证明的语义研究”[10]也可以被算作元数学。

笔者未能在科里的著作中找到关于这类元定理的明确例子。

我们知道哥德尔完全性定理需要至少在二阶算术语言中陈述，并且可以在二阶算术公理系统WKL0中被证明。

另一方面，我们不能无限扩大对这部分“元数学”的解释。

一般被认为，下行的勒文海姆-斯寇伦定理是哥德尔完全性定理证明的推论。

但其证明中使用了某种形式的选择公理。

准确地说，在 ZF 基础之上，针对可数语言的下行的勒文海姆-斯寇伦定理与依赖选择公理（dependent choice，DC）是等价的；而针对任意基数语言的下行的勒文海姆-斯寇伦定理与选择公理等价[11]。

显然，科里不会承认选择公理是否为真也是他所谓的关于形式系统“元数学”的问题。

① ε0是一个可数无穷的序数，它是序数序列ω, ωω, ωωω……的极限。

根岑（Gerhard Gentzen）基于ε0下的归纳原理证明了皮亚诺算术的一致性。

这被认为是希尔伯特纲领在哥德尔定理之后最重要的成就，也是现代证明论的开端。

参见Takeuti G., Proof Theory, 2nd ed.,New York: Dover Publication, 2013, 第11节。

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。