形式主义与多宇宙观（二） (4-2)

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

因此，力迫语言的“语义”作为一个关系也是原有集合论宇宙中的一个可定义的真类。在这种解释下，为了证明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)。

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