典范模型（完备性到底是怎么证明的）

上级：soundness-and-completeness

Completeness（⊨ φ ⟹ ⊢ φ）的证明系于一条引理：每一个一致的理论都有一个模型。 这个技巧漂亮的地方在于，你不必去寻找一个模型——你可以直接从语法本身构造出那个典范模型：理论自身的语句变成了一个结构。这个结构就是典范模型（也叫词项模型（term model）/ Henkin 模型）。

需要证明什么

证明完备性的逆否命题：Γ ⊬ φ ⟹ Γ ⊭ φ。由于 Γ ⊬ φ，集合 Γ ∪ {¬φ} 是一致的（推不出矛盾）。所以只需证明：

一致 ⟹ 可满足 —— 任何一致的语句集合都有一个模型。

于是那个模型同时满足 Γ 和 ¬φ，也就见证了 Γ ⊭ φ。

从语句本身构造模型

从一个一致的集合 Δ（这里就是 Γ ∪ {¬φ}）出发，分三步把它变成一个结构：

补全它（Lindenbaum）。 把 Δ 扩展成一个极大一致集 Δ*：遍历每一个语句 ψ，把 ψ 或 ¬ψ 加进去——哪个能保持一致就加哪个。现在 Δ* 对每一个语句都有定论（对每个 ψ，ψ 和 ¬ψ 恰有一个在其中）。
补上见证者（Henkin）。 对 Δ* 中每一个 ∃x. ψ，确保存在某个常元 c 使得 ψ[c/x] 也在 Δ* 中（引入新鲜的见证常元）。这样每一个"存在"都有了一个具名的例子。
读出结构 M。 把定义域取为项本身（闭项，当 t = s ∈ Δ* 时约定 t ~ s）；每个函数符号和关系符号的解释，就照 Δ* 所断言的来定。模型的元素，字面意义上就是语法本身。

真值引理——语法变成真值

真值引理

在这个 M 中，对每一个语句都有：M ⊨ ψ ⟺ ψ ∈ Δ*。（对 ψ 做归纳：联结词的情形靠 Δ* 的极大一致性成立，量词的情形靠 Henkin 见证者成立。）

于是 M 恰好使 Δ* ⊇ Γ ∪ {¬φ} 中的语句为真。这就是一个满足 Γ 而 φ 为假的模型 → Γ ⊭ φ。∎

看它实际运作——一个三段论

我们来证明假言三段论——从 P→Q 和 Q→R，推出 P→R：

    P → Q        (premise)
    Q → R        (premise)
  ───────────
  ∴ P → R        (conclusion)

这就是蕴含的传递性（P⇒Q⇒R 一路连下去，所以 P⇒R）——它是每一个多步论证的骨架。选它做示范再合适不过，正因为你早就知道它是对的：看着这套构造把它重新推出来，你学到的是要去信任这个方法本身（之后就可以把它对准那些你不知道答案的命题）。

现在换语义的路子。由完备性，只需证明 Γ ⊨ P→R，而典范模型定理恰好给出了这一点：Γ ⊢ P→R 只有在 Γ ∪ {¬(P→R)} 一致时才会不成立（一致的话它就会有一个典范模型——一个反例模型）。所以试着去构造这个模型，然后看它怎么崩塌。

这个集合是（用 ¬(P→R) ≡ P ∧ ¬R）：

   P → Q ,   Q → R ,   P ,   ¬R

补全它（Lindenbaum）——把被迫成立的东西都加进去：

P 在集合里，P→Q 也在 ⟹ Q 必须被加进去（加入 ¬Q 会破坏一致性）；
Q 在集合里，Q→R 也在 ⟹ R 必须被加进去；
但 ¬R 已经在集合里了——矛盾。

所以这里不存在极大一致扩张 → 没有典范模型 → 这个集合是不可满足的 → Γ ⊨ P→R，因此（由完备性）Γ ⊢ P→R。∎

回头看发生了什么：这套构造试图构造一个前提成立而结论失败的世界，却没能成功——语法硬生生把 R 逼成既真又假。（如果这个集合原本是一致的，补全就会成功，交给你一个货真价实的模型，正如上面那套一般性构造所展示的那样。在完整的一阶逻辑中，这个成功同样要用到 Henkin 见证者——为每一个 ∃x.ψ 找一个常元 c 使 ψ[c/x] 成立——并把项取作定义域。）

为什么叫它典范

你并不是在数学的荒野里发现了一个模型——你是制造出了这个理论用来描述自身的那唯一一个典范模型：它的对象就是项，它的真值就是"极大一致理论怎么说"。语法就是语义。这正是 completeness 的真正内容：一堆仅仅一致的符号，已经被强迫去描述一个世界——这就是为什么可证性和真最终会重合。

（这里"典范"的含义不同于 CNF/DNF 这类范式：那边的典范对象是一个公式，这里的典范对象是一个模型。这套构造还顺带白送了compactness——如果 Γ 的每一个有限子集都可满足，那么 Γ 就是一致的，因而它有一个典范模型。）