数学多元论（三） (7-4)

因为，“这些命题的真取决于与构造主义命题中所蕴涵的形式不同的理想假设。”[10]56

在结束本节之前，我们试图进一步厘清形式主义的“元数学”概念。

科里声称他的“元数学”并不局限于希尔伯特的有穷数学。

而正如前文中提到的，科里所举的“元命题”的例子主要是关于公理系统可证性以及公理系统之间证明论强度的命题。

一般认为，一个公理系统的公理集必须是能行可判定的。

也就是说，至少要有一个有穷的机械的程序，任给一则表达式，该程序能够在有穷时间内判断该表达式是否是一条公理。

进一步，我们要求该公理系统下的证明是能行可检测的。

也即，原则上存在一个有穷的机械程序，任给一个表达式序列，该程序能够在有穷时间内判断这个序列是否构成一个有效的证明。

上述这些要求恐怕是对公理系统最低的要求。

事实上，数学家社区对公理系统及其证明的可检测性有着更高的要求。

例如，经验上可以被其他数学家所理解等。

由于证明有效性是能行可检测的，原则上， 人们就可以设计一个计算机程序来枚举某个公理系统所有可能的数学定理。

因此，关于公理系统内部可证性的问题，也就成了关于上述程序能否枚举到某个命题的问题。

我们可以通过哥德尔编码和克莱尼谓词（Kleene’sPredicate）将它变成一个算术问题，更准确地说，它是一个Σ0 1 的一阶算术问题。

相对一致性命题，如Con(T1 )→Con(T2 )是关于公理系统间证明论强度的典型问题。

一个相对一致性证明往往来自具体给出一个统一的程序，将任何T2 中到谬误的证明转换为T1 中到某个谬误的证明。

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

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

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

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

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

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

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

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

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

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