先说结论:我们是可以在PA 中讨论 ZF / ZFC 上的相对一致性结果的,或者不如说,一条关于某几个递归理论的相对一致性结果,如果未加额外说明,那么我们总是倾向于将其理解为元理论 PA (或者更弱的 PRA )中的结论。当然,对于力迫法等一些较复杂的证明手段,这需要一定的、非平凡的解读(比如布尔值模型),但依然是可行的。
在这里,我们试图通过两个例子来严谨并循序渐进地解释这一点:一个更简单的、不涉及力迫法的相对一致性结果,和一个在任意力迫模型上的相对一致性结果。
那么首先,让我们考虑“ZF 与 ZFC 相对一致”的这个结论。这个结论的非形式证明非常简单:在一个 ZF 宇宙中,我们考虑哥德尔的可构造宇宙 L ;可以证明, L 是 ZF 的模型,且 L 上有一个(可定义的)良序关系,从而可以推出 L 也满足选择公理。我们会把这个“ ZFC 模型”的存在性理解为 ZF 与 ZFC 相对一致的直接证据。
那么如何将这个非形式的论证转化为对命题Con(ZF) 和 Con(ZFC) 的严格讨论呢?我们就需要移步到一个能讨论递归理论上的形式证明的元语言中,比如 PA 。 ZF 上的超限递归定理告诉我们, L 可被定义为整个集合论论域上的一个真类,也就是说有一个一阶公式 θ(x) 使得我们想要定义的 L 恰好由全体满足这个公式的元素所构成(在元理论 PA 中,我们能够具体地写出这个公式的编码 ⌜θ⌝ )。由 θ 的编码,我们能够构造一个原始递归函数(因此是 PA 中可定义的函数) τ ,使得 τ(⌜φ⌝) 为一阶集合论公式 φ 在 L 上的相对化的结果(的编码)——也就是说, φ 中的每一个无限定量词 ∀xψ 或 ∃xψ 都被对应替换为了 ∀x(θ(x) → ψ) 以及 ∃x(θ(x)∧ψ) 。
这个编码τ(⌜φ⌝) 所表示的公式,我们通常在集合论中会缩写为 L╞ φ 。换句话说,我们在上面所进行的非形式证明“ L╞ ZFC ”,实际上是在元语言 PA 中证明了“对于任意 ZFC 的公理 φ ,从 ZF 能证明 τ(⌜φ⌝) ”。进一步地,我们还可以在元语言中验证 L 是一阶逻辑意义下的模型,或者严格地说“如果有一阶逻辑中的一个证明 m ,其全体前提为 φ₁,. . .,φₙ ,而结论为 ψ ,那么从 ZF 能证明 τ(⌜φ₁⌝)∧· · ·∧τ(⌜φₙ⌝) → τ(⌜ψ⌝) ”(对证明 m 的长度进行归纳可以非常容易地证明此性质)。从这两个结论可以直接推出“若从 ZFC 能证明 φ ,则从 ZF 能证明 τ(⌜φ⌝) ”,现在,只要将矛盾表示为任意的一阶公式 ρ∧¬ρ ,并注意到其相对化 τ(⌜ρ∧¬ρ⌝) 依然是一个命题与其否定之合取的形式,即也表示矛盾;代入 φ:=ρ∧¬ρ ,我们即可以轻松得到(元语言 PA 中)“ Con(ZF) → Con(ZFC) ”的结论(其逆是平凡的)。
现在,我们回到通过力迫法得到的那些更复杂的相对一致结果上。一般地,我们考虑ZFC 及其一个扩张理论 T ⊇ ZFC ,那么在通常的力迫构造中,我们会选择一个力迫偏序 P 并构造(某个)集合论宇宙 V 上的力迫扩张 V[G] ,其中 G 为偏序 P 的一个 V-脱殊集,从而不能存在于 V 中。最后,我们验证 V[G] 是理论 T 的模型,从而说明 ZFC 与 T 相对一致。这与上面对 L 的考察的区别在于,并没有一个显然的对应关系可以让我们将 V[G] 嵌入原本的集合论宇宙 V 中,从而“看似”无法找到这么一个将 V[G] 上公式中的量词翻译回 V 中的翻译函数 τ 。
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。