关于这个解释需要注意的是,满足T的可数传递模型M的存在往往严格强于Con(T)这个假设。
实际上,我们取的是集合论公理集T的任意一个有穷部分T0 (ZF可以证明任何ZF有穷子集都有可数传递模型)。
由此,上述解释本质上提供了一个证明转换的能行方法:如果T+φ不一致,即存在一个有穷的T0 +φ可以证明荒谬,那么我们就可以从Con(T0 )这个假设出发证明出存在T0 +φ的模型这个荒谬,因而T也是不一致的。
通过力迫语言的解释一定程度上可以避免这种曲折的处理方式。
我们先定义力迫语言的“语义”——力迫关系: p⊩α( ) τ ˉ ,其中τ ˉ是一串“力迫名词”,“力迫名词”可以被理解为在原有集合论宇宙中指称可能的力迫扩张中对象的名称,它们构成了原有集合论宇宙中的一个可定义的真类。
因此,力迫语言的“语义”作为一个 关系也是原有集合论宇宙中的一个可定义的真类。
在这种解释下,为了证明Con(T)→Con(T+φ),一般假设我们在T宇宙中定义了力迫语言,试图证明存在力迫条件p⊩φ。
由此,如果T+φ不一致,即T⊢¬φ,可以 证明任何力迫条件都有p⊩¬φ,从而我们得到了T中的矛盾:p⊩φ且p⊩¬φ(这与力迫关系的性质不符)。
我们还可以借助布尔值模型使得基于力迫语言的解释显得更直观。
布尔值模型VB可以被理解为对通常基于二值布尔代数的语义的推广,在其中每个语句的真值是B中的元素。
我们从一个ZFC宇宙V出发构造的布尔值模型VB中,ZFC和ZFC的推论的“真值”都是B中的最大元,而如果一个语句在VB中能取 除最小元以外的真值,它就是与ZFC是一致的了。
上述力迫法的解释无不涉及无穷模型,甚至真类(布尔值模型VB和力迫关系都是V中的真类)。
即使知道基于力迫法的相对一致性证明,要还原出其在PRA 中的版本也往往是一件非常困难的任务,很难想象对着ZF的形式定义就能够找到Con(ZF)→Con(ZF+ 2^ℵ_0=ℵ_2 )所需要的证明变换程序。
我们举一个极端的例子来解释为什么形如Con(T)的典型的形式主义“元数学”问题必须援引“外在的”直观。
我们通常只关心可公理化的理论T,也即T是递归可枚举的。
由此,Con(T)可以被写成一则Π0 1 的一阶算术语句① 。
例如,Con(ZFC)就是一则即使在ZFC中也无法证明的Π0 1 语句(假设ZFC一致)。
甚至,无论我们如何添加新的公理来扩张ZFC,只要所得到的仍然是一个一致的集合论公理系统,其中就仍然有不可证的真的Π0 1 语句。
这些是哥德尔第二不完全性定理告诉我们的。
一般认为Con(ZFC)作为对ZFC的扩张,并不是很强的命题。
例如,ZFC+存在不可达基数就可以证明它。
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。