形式主义与多宇宙观（二）

二、形式主义对数学实践的影响

笔者在《结构主义是一种有效的数学哲学吗？》中质疑结构主义是有效的数学哲学[12]。

在同样的意义上，形式主义无疑是有效的数学哲学。

希尔伯特的形式主义纲领直面数学工作者的困惑。

无论是希尔伯特本人关于几何的公理化工作，还是一阶谓词逻辑和集合论的公理化，抑或前文提到的根岑和哥德尔关于皮亚诺算术的一致性和相对一致性证明，都是在希尔伯特形式主义纲领启发下的数学工作。

在这个意义上，形式主义的确对数学实践有着积极的影响。

裘江杰在《集合论多宇宙观与形式主义》中认为，元数学“作为对数学的反思性研究”是“形式主义的重要组成部分”，并且形式主义，尤其是被纳入形式主义框架的集合论多宇宙观有助于为集合论搜寻新公理。

本节中，笔者则试图说明：形式主义者尤其关注的元数学研究恰恰非常依赖超出形式主义的思想和直观；而形式主义对探究集合论新公理的作用是有限的。

的确，当代集合论研究中大量使用力迫法得到的结果都可以写成 Con(T)→Con(T+φ)这样的形式。

这种相对一致性结果可以被看作是典型的元数学命题，并且本质上可以在弱如PRA这样的算术公理系统中得到证明。

但实际上，几乎没有集合论工作者是在算术公理系统中工作来发现这些证明的。

一般关于力迫法的直观是构造一个已有集合论宇宙中不存在的泛型（泛型，generic）对象，例如ℵ2个实数，来得到满足某个命题的“更大的”集合论宇宙，并称之为力迫扩张（forcing extension）。

按照朴素的单一宇宙观，把集合论宇宙理解成所有集合组成的宇宙，就无法解释何以能够再造出一个在集合论宇宙中不存在的泛型对象。

对此，一般可以借助可数传递模型或力迫语言来解释。

用可数传递模型来解释Con(T)→Con(T+φ)的力迫法证明，首先假设存在T的可数传递的玩具模型M，由于可数模型上的泛型对象总存在，我们可以证明存在M的力迫扩张M[G]满足T+φ。

在这个解释下，我们处理的只是玩具模型，无论玩具模型M、泛型对象G还是M的力迫扩张M[G]都真实地存在于我们的宇宙中。关于这个解释需要注意的是，满足T的可数传递模型M的存在往往严格强于Con(T)这个假设。

实际上，我们取的是集合论公理集T的任意一个有穷部分T0（ZF可以证明任何ZF有穷子集都有可数传递模型）。

由此，上述解释本质上提供了一个证明转换的能行方法：如果T+φ不一致，即存在一个有穷的T0+φ可以证明荒谬，那么我们就可以从Con(T0)这个假设出发证明出存在T0+φ的模型这个荒谬，因而T也是不一致的。

通过力迫语言的解释一定程度上可以避免这种曲折的处理方式。

我们先定义力迫语言的“语义”——力迫关系：PⅡ-a

(ˉτ)

，其中

ˉτ

是一串“力迫名词”，“力迫名词”可以被理解为在原有集合论宇宙中指称可能的力迫扩张中对象的名称，它们构成了原有集合论宇宙中的一个可定义的真类。

因此，力迫语言的“语义”作为一个关系也是原有集合论宇宙中的一个可定义的真类。在这种解释下，为了证明Con(T)→Con(T+φ)，一般假设我们在T宇宙中定义了力迫语言，试图证明存在力迫条件p⊩φ。

由此，如果T+φ不一致，即T⊢¬φ，可以证明任何力迫条件都有 p⊩¬φ，从而我们得到了T中的矛盾：p⊩φ且 p⊩¬φ（这与力迫关系的性质不符）。

我们还可以借助布尔值模型使得基于力迫语言的解释显得更直观。

布尔值模型VB可以被理解为对通常基于二值布尔代数的语义的推广，在其中每个语句的真值是B中的元素。

我们从一个 ZFC宇宙V出发构造的布尔值模型VB中，ZFC和ZFC的推论的“真值”都是B中的最大元，而如果一个语句在Vᴮ中能取到除最小元以外的真值，它就是与ZFC是一致的了。

上述力迫法的解释无不涉及无穷模型，甚至真类（布尔值模型Ⅴᴮ和力迫关系都是V中的真类）。

即使知道基于力迫法的相对一致性证明，要还原出其在PRA中的版本也往往是一件非常困难的任务，很难想象对着ZF的形式定义就能够找到con(zf)→con(zf+2ℵ0=ℵ₂)所需要的证明变换程序。

我们举一个极端的例子来解释为什么形如Con(T)的典型的形式主义“元数学”问题必须援引“外在的”直观。

我们通常只关心可公理化的理论T，也即T是递归可枚举的。

由此，Con(T)可以被写成一则∏º₁的一阶算术语句①。

例如，Con(ZFC)就是一则即使在ZFC中也无法证明的∏º₁语句（假设ZFC一致）。

甚至，无论我们如何添加新的公理来扩张ZFC，只要所得到的仍然是一个一致的集合论公理系统，其中就仍然有不可证的真的∏º₁语句。

这些是哥德尔第二不完全性定理告诉我们的。

一般认为Con(ZFC)作为对ZFC的扩张，并不是很强的命题。

例如，ZFC+存在不可达基数就可以证明它。

但下面的事实告诉我们，在处理形如 Con(T)的语句时，我们必须对 T的具体编码方式保持谨慎。

通过一些处理，我们甚至可以把“ZFC是一致的”这则∏º₁语句变得任意强。

事实固定对集合论语言的编码，令{σi}i∈N是对集合论语言语句的能行枚举。

对任意∏º₁语句∀xφ(x) （其中φ(x)是一个△º₁公式），存在一个自然数e使得：

（1）∀xφ(x)蕴含{σi: i∈We}=ZFC；

（2）ZFC+Con({σi: i∈We})⊢∀xφ(x)。

这里我们援引递归论中的术语，用 We表示编码为 e的图灵机的定义域，或“第 e个递归可枚举集”。

我们说，ZFC 是一个递归可枚举的（实际上是递归的）公理集，也即存在一个自然数 d 使得 ZFC={σi: i∈ Wd}。

所以事实陈述中的{σi: i∈We}=ZFC实际上是 We=Wd这样一则一阶算术命题。

此外，Wd又可以被表示为一个递归函数δ的值域：Wd={δ(i): i∈N}。

事实的证明

假设ZFC={δ(i): i∈N}。

我们可以构造一个部分递归函数Φe：

δ(n)，如果∀x＜nφ(x)，

Φₑ(n)＝{

δ(n)∧0=1，否则。

我们先验证（1）：如果∀xφ(x)成立，那么We=ranΦe=ZFC。

此时，Con(We)等价于Con(ZFC)。

验证（2）：我们在ZFC中工作，如果¬∀xφ(x)，那么We中就包含0=1。

因而，¬Con(We)。

证毕。

因此，对任何真的∏º₁语句（例如，“ZFC+存在任意大的武丁基数是一致的”），我们都可以找到 ZFC的某个编码，使得Con(ZFC)蕴含这则语句。

在弗雷格这样的实在论者看来，这并没有什么吊诡的地方，因为它们都是真的。

科里认为，当我们证明一个数学命题的时候，重要的是我们证明了这个命题在某个公理系统中可证这一元数学事实。

一度作为ZFC形式主义②者的谢赫拉（Saharon Shelah）在已知ZFC关于正则基数为指数的幂所知甚少的情况下，提议尽可能在ZFC中证明关于奇异基数为指数的幂的取值上限，并证明了著名的不等式：

2ℵω＜ℵω₄

。

证明使用了谢赫拉发明的相比基数幂运算更精细的共尾可能性理论（pcf theory），涉及在各种超积模型中可能的共尾数。

这依赖于相当深刻的集合直观。

尽管所有在ZFC公理系统中的证明自然都会有相应的元定理作为副产品，但即使在ZFC形式主义者看来，他所证明的是一则关于集合的事实，而不是一则有穷的算术“元数学”命题。

事实上，没有人真正给出过见证

ZFC⊢2ℵω＜ℵω₄

的形式化证明的编码。

裘江杰在《集合论多宇宙观与形式主义》中认为形式主义能够帮助探究集合论新公理。

后者是哥德尔纲领的核心议题，也被认为是柏拉图主义面对不完全性现象的标准回应。裘江杰写道：“为获得具有某种独立性的常规数学结果所必须的命题可能可以作为新公理的候选。这一进路是形式主义的。”[3]对这句话可以有两种解读。

一种是，得到独立性结果这种“元数学”结果所必须的命题可以作为新公理的候选；

第二种是，要证明已知独立命题（如独立于ZF的CH）所必须的命题可以作为新公理的候选。

已知的独立性元数学结果（由一对相对一致性命题组成）往往是在弱如PRA这样的有穷主义公理系统中可证的，并不需要什么扩张了现有集合论公理系统的新公理候选。

因此，第一种解读可以排除。

关于第二种解读，来自形式主义对新公理的要求是证明目标已知独立命题所必须的命题。

笔者认为，这是不合理的。

按照哥德尔纲领对新公理的标准的讨论，集合论新公理除了必须满足符合我们关于集合概念的直观这一内在性要求，还应该具有成果丰富性这一外在性要求，即可以加深我们关于集合论宇宙的理解。

除去丰富性要求，最“安全的”新公理无疑是将目标独立问题或其否定本身作为新公理，这恰好符合形式主义者的上述要求。

目前关于集合论新公理的主要候选理论（W. Hugh Woodin的终极L、力迫公理和内模型假设）都有远超连续统假设问题的丰富后承。

又或许形式主义者思考的对新公理的探究是类似反推数学的工作，后者试图厘清被广泛接受的数学成果所需要的最小二阶算术公理系统是什么。

由此，构造主义者可以在选择他们所认可的公理系统之前就了解他们能够保留什么以及必须放弃什么。

反推数学的一些工作的确被宣称为希尔伯特纲领的部分实现[13]。

但笔者认为这类工作意义在于为部分怀疑论者在选择可接受的极小系统时提供参考，所涉及的都是在柏拉图主义者看来显然成立的公理系统。

它与为集合论乃至全部数学寻找新公理的哥德尔纲领的志趣相去甚远。

综上，形式主义思想对探究新公理的作用十分有限。

① 我们用Con(T)表示“理论T是一致的”这样一则数学命题。一般通过固定一种编码方式，并假设T在这种编码方式下可以被表示为一个算术可定义的公式集，从而将“T是一致的”写成一则算术语句。

② 在典范翻译下也是一则集合论语句，即把自然数集定义为第一个无穷序数ω，再以标准的方式定义其上的运算。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。