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

的确，无论在物理学还是数学实践中，人们往往（甚至注定）是在某个理论的一致性证明或其他“安全保证”尚未确立的情况下工作于其中的。

但这不妨碍这类基础问题始终是数学、物理及其哲学的核心关切。

而只要直面这一数学基础问题，无论柏拉图主义者、直觉主义者还是形式主义者（正如前文所分析的）都无法做到所谓的本体论中立。

关于科里的形式主义立场，一个有趣的事实是，他非常重视关于形式系统的“元数学”，甚至以此为数学的本质：“数学是关于形式系统的科学”[10]。

他所关注的“元命题”主要是关于形式系统本身（诸如“命题x是在形式系统X中可证的”），以及形式系统之间关系（诸如，一个系统是另一个系统的子系统）这样的命题。

而“形式系统X是一致的”无非是某个具体的谬误（如0=1或α∧¬α）“不是在形式系统X中可证的”。

因此，无论科里对系统一致性证明持有怎样的看法，他对所谓“元数学”地位的特别关注使他无法避免本体论上的二分立场。

事实上，在关于数学的“形式主义”定义中，科里明确将“非构造性命题排除在真正的数学的领域之外”。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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