皮亚诺算术

先说结论：我们是可以在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 中的翻译函数 τ 。

这个缺陷，实际上有数种不同但等价的解决方案，实际上也就是我们在集合论中所说的“对力迫法进行形式化”的不同选择，这里我们选择与前文中关于[公式] 的构造最为近似的构造布尔值模型的方法为例进行解释。对于接下来提及的形式构造以及相关结论的证明，均参考Jech的《集合论》教材第三版：

首先，关于力迫的基本理论告诉我们，任何力迫偏序P 都可以扩张为一个完备布尔代数 B ，这同样由宇宙 V 中的一个集合及其上的偏序构成，但还支持否定、合取与析取这三种运算；且这个扩张不影响对应的力迫构造：对于 P 进行力迫和对于排除最小元的 B \ {0}上的偏序进行力迫会给出同一个力迫模型。于是对于任意一个力迫构造，我们就可以取对应的完备布尔代数 B 并且递归地在 V 中构造真类 Vᴮ ：

Vᴮ∅＝∅

Vᴮα＋1＝∪ˣ B

x ⊆ Vᴮα

Vᴮᵧ＝∪Vᴮᵦ

β∈γ

Vᴮ＝∪Vᴮα

α∈Ord

其中 ˣ B 表示全体由 x 至 B 的函数构成的集合。由 ZF 上的递归定理， Vᴮ 可以像 L 一样由写为全体满足某个一阶公式 η(x) 的集合。同样递归地，我们可以在 Vᴮ 上定义二元运算符 ||– ∈ –||：Vᴮ × Vᴮ → B ，其计算规则由下式给出：

||x ∈ y||＝∑ (y(t)· ∏ (–x(r)＋||r ∈ t||).

t∈dom(y) r∈dom(x)

∏ (–t(r)＋||r ∈ x||))

r∈dom(t)

（该规则可以近似理解为保证了 x∈y ↔ ∃t∈y(∀r ∈ x r ∈ t ∧ ∀r ∈ t r ∈ x) ，参见下方关于逻辑连接符和量词的翻译规则。）进一步地，我们就可以在元语言 PA 中定义一个原始递归的翻译函数 σ ，使得对于任意公式 φ 都有 σ(⌜φ⌝)＝⌜||φ||＝1⌝ ，其中 ||φ|| 为一指代 B 中元素的词项，若 φ 是原子公式 x∈y 则直接定义为上面给出的二元运算符作用在变量 x，y 上的结果；对于其他 φ 则依照复杂度在元语言中递归地定义如下：

||¬φ||＝ – ||ψ||

||ψ∧χ||＝||ψ|| · ||χ||

||ψ∨χ||＝||ψ||＋||χ||

||∃x ψ(x)||＝∑ ||ψ(t)||

t∈Vᴮ

||∀x ψ(x)||＝∏ ||ψ(t)||

t∈Vᴮ

（这里，为简便起见，我们可以将公式 x＝y 视作 ∀t ∈ x t ∈ y∧∀t ∈ y t ∈ x 的缩写，而将 ψ → χ 视作 ¬ψ∨χ 的缩写。）

到这一步，应该就易于注意到布尔值模型的构造和上述关于L 作为集合论模型的分析的相似之处了。作用于布尔值模型的脱殊模型基本定理正是告诉我们，于上文类似地，对于任意 ZFC 的公理 φ ， ZFC 可以证明 ||φ||＝1 ，即 σ(⌜φ⌝) ；并且如果有一阶逻辑中的一个证明 m ，其全体前提为 φ₁，. . .，φₙ ，而结论为 ψ ，那么从 ZFC 同样能证明 σ(⌜φ₁⌝)∧· · ·∧σ(⌜φₙ⌝) → σ(⌜ψ⌝)。如果我们能验证所取的特定完备布尔代数 B 还使得对于扩张理论 T ⊇ ZFC 中的额外公理 φ ，比如经典例子科恩力迫所满足的 ¬CH ， ZFC 能够证明 σ(⌜φ⌝) ，那么我们就可以在元语言 PA 中推出“若从 T 能证明 φ ，则从 ZFC 能证明 σ(⌜φ⌝) ”。最后，再如上地考虑表达矛盾的公式 ρ∧¬ρ ，注意到 ||ρ∧¬ρ||＝1 等价于 ||ρ|| · – ||ρ||＝0＝1 ，与布尔代数必须满足的基本性质 p · –p＝0 矛盾，即 σ(⌜ρ∧¬ρ⌝) 依然亦是表示矛盾的公式；于是便可同样得到（元语言 PA 中）“ Con(ZFC) → Con(T) ”的结论。

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