复旦大学：《数理逻辑》课程教学资源（讲义）第6章哥德尔完全性定理.pdf_大学文库

第 6 章哥德尔完全性定理第 1 节可靠性定理定理 6.1 (可靠性定理). 如果 Γ ⊢ φ，则 Γ |= φ。我们把证明分成一些小的步骤。首先注意到：如果 Γ |= ψ 并且 Γ |= ψ → φ，则 Γ |= φ。（为什么？）换句话说，分离规则保持真确性。因此我们只需验证所有公理都是普遍有效的。根据习题 ??，一个公式 θ 是普遍有效的当且仅当 ∀xθ 是普遍有效的。我们得到：一个普遍有效公式的概括仍是普遍有效的。所以我们只要检查六组公理，验证每一组中的公式都是普遍有效的。习题 ?? 还告诉我们，{∀x(α → β), ∀xα} |= ∀xβ 和当 x 不在 α 中自由出现时，α → ∀xα。因而第三和第四组公理都是普遍有效的。我们把第一组公理的普遍有效性留做习题。第五组公理 x ≈ x 的普遍有效性是显然的。我们再来看第六组公理的普遍有效性：x ≈ y → (α → α ′ )，其中 α 为原子公式并且 α ′ 是将 α 中出现若干个 x 用 y 替换所得到的。我们只需验证 {x ≈ y, α} |= α ′。固定一个结构 A 和赋值 s 满足 (A, s) |= x ≈ y，即，s(x) = s(y)。通过对项 t 施行归纳（具体步骤省略），我们可以证明 s(t) = s(t ′ ) 其中 t ′ 是将 t 中出现若干个 x 用 y 替换所得到的。如果 α 是 t1 ≈ t2，则 α ′ 为 t ′ 1 ≈ t ′ 2，因而 (A, s) |= α 当且仅当 s(t1) = s(t2) 当且仅当 s(t ′ 1 ) = s(t ′ 2 ) 当且仅当 (A, s) |= α ′。类似的证明对形如 P t1 . . . tn 的原子公式 α 也适用。所以我们只剩下验证第二组替换公理的普遍有效性。我们先证明一个引理。引理 6.1 (替换引理). 如果项 t 可以在公式 φ 中替换变元 x，则 (A, s) |= φ x t 当且仅当 (A, sx s(t) ) |= φ。证明: 我们对公式 φ 施行归纳。初始情形：φ 是原子公式。首先利用对项 u 施行归纳，很容易证明：对任何项 u 和 t，都有 s(u x t ) = s x s(t) (u)。我们这里只证明当 φ 为 P u1u2 · · · un 的情形，而把 φ 为 u1 ≈ u2 的 1

第 2 节完全性定理第 6 章哥德尔完全性定理验证留给读者。 (A, s) |= (P u1u2 · · · un) x t 当且仅当 (s((u1) x t ), s((u2) x t ), · · · , s((un) x t )) ∈ P A 当且仅当 (s x s(t) (u1), s x s(t) (u2), · · · , s x s(t) (un)) ∈ P A 当且仅当 (A, sx s(t) ) |= P u1u2 · · · un。归纳情形：我们只处理量词的情形，而把 φ 为 ¬ψ 或者 ψ → θ 的情形留给读者。如果 φ 为 ∀yψ 并且 x 不在 φ 中自由出现。只须注意 s 和 s x s(t) 在出现在 φ 中的自由变元上取值相同，还有 φ x t 就是 φ，立刻可得知结论成立。剩下的情形为 φ 为 ∀yψ 并且 x 的确在 φ 中自由出现。由于 t 可以在 φ 中替换 x，我们有 y 不在 t 中出现并且 t 可以在 ψ 中替换 x。所以，对论域 | A | 中的任何 d 都有 s(t) = s y d (t)。由于 x ̸= y，φ x t = ∀yψx t 。所以 (A, s) |= φ x t 当且仅当对所有 d,(A, s y d ) |= ψ x t , 根据归纳假定当且仅当对所有 d,(A,(s y d ) x s(t) ) |= ψ 当且仅当对所有 d,(A,(s x s(t) ) y d ) |= ψ 当且仅当 (A, sx s(t) ) |= φ。这就完成了对替换引理的归纳证明。返回到对第二组公理可靠性的验证。假定 t 在 φ 中可以替换 x 并且 (A, s) |= ∀xφ。我们需要证明 (A, s) |= φ x t 。我们知道对 | A | 中的任意元素 d，都有 (A, sx d ) |= φ。特别地，取 d 为 s(t)，我们有 (A, sx s(t) ) |= φ。根据替换引理，(A, s) |= φ x t 。到此可靠性定理验证完毕。我们叙述可靠性定理的两个常用推论。推论 6.1. 如果 ⊢ (φ ↔ ψ)，则 φ 和 ψ 语义等价。推论 6.2. 如果 Γ 是可满足的，即存在结构 A 和赋值 s 满足 Γ 中的所有公式，则 Γ 是相容的。第 2 节完全性定理 “如果一个一阶语句在所有的模型中都成立，那一定是因为有一个统一的原因（证明），而不是源于偶然让它在不同的模型内或在不同的情形下因不同的原因而成立。”– 布拉斯1 1布拉斯，Andreas Blass （1947 - ），美国逻辑学家，数学家。 2

第6章哥德尔完全性定理第2节完全性定理接下来我们证明可靠性定理的逆定理一完全性定理。最初的证明是哥德尔在1929年证明1930年发表的。我们下面采用的证明是辛钦2在1949年给出的。我们只考虑一阶语言是可数的情形,即语言中所有的符号组成一个可数集。3 定理62(完全性定理) a)如果r9,则rhφ b)任何相容的公式集都是可满足的。根据引理?,(a)与(b)等价。(虽然引理?!讨论的是命题逻辑,但证明稍加改动便对一阶逻辑也适用。)所以我们只证明(b)。我们首先考虑语言中没有等词的情况。假定r 是一个相容的公式集。证明的思路与命题逻辑的完全性定理相似。我们首先把T扩充成个极大相容集Δ还包括一族新的“辛钦公理”,以帮助我们处理量词。所谓辛钦公理的形式如下其中c是“新的”常数符号。我们要做的其实是添加彐xv→v,即对每一个存在性的语句都添加一个直接证据c。我们写成以上的等价形式是因为后面用起来更直接。本质上说,辛钦公理其实就是量词消去,代价是添加新的常数。有了这样的△之后,我们很容易“读出”一个满足Δ中(除了带等词的)所有公式的结构和赋值。首先我们向语言L中添加可数多个新的常数符号C={c0,1,…}。把扩展后的语言记作LC。我们验证r在新的语言中仍然是相容的。这听起来是显然的,但添加了常数符号后,公理变多了,我们还是有必要验证一下。(这实际上是后面归纳验证辛钦公理的相容性的一部分。)假如在扩张语言之后T变得不相容了,则存在(Lc内的)公式B和某个(Lc内的)从r到B∧-B的证明序列。注意到证明序列中包含的新常数符号为有穷多。我们可以用常数概括定理把它们都替换成变元,从而得到一个从I到(B∧-β)(在 L中的)证明序列,其中β是从β中把新常数符号替换成变元而得到的。由于β"是L中的公式,这与r的相容性矛盾。接下来我们添加所谓辛钦公理,即对所有(Lc中的)公式p和所有的变元x,我们都向中添加公式其中c是某个新常数符号。具体做法如下4:固定一个(Lc中)公式和变元有序对(y,x 的枚举 2辛钦, Leon henkin(1921-2006),美国逻辑学家。 3完全性定理对不可数语言也成立,只不过证明要用到选择公理等集合论工具 4另一种常见的做法是:从语言Lo=L出发,添加可数多常数C使得Lo中的公式都有辛钦公理相配,但语言扩展成L1=Lo∪Co之后,我们还要添新的常数C1使得L1中的公式都有辛钦公理相配,如此下去,我们需要扩充u步才能达到目的

第 6 章哥德尔完全性定理第 2 节完全性定理接下来我们证明可靠性定理的逆定理 – 完全性定理。最初的证明是哥德尔在 1929 年证明 1930 年发表的。我们下面采用的证明是辛钦 2在 1949 年给出的。我们只考虑一阶语言是可数的情形，即语言中所有的符号组成一个可数集。3 定理 6.2 (完全性定理). (a) 如果 Γ |= φ，则 Γ ⊢ φ。 (b) 任何相容的公式集都是可满足的。根据引理 ??，(a) 与 (b) 等价。（虽然引理 ?? 讨论的是命题逻辑，但证明稍加改动便对一阶逻辑也适用。）所以我们只证明 (b)。我们首先考虑语言中没有等词的情况。假定 Γ 是一个相容的公式集。证明的思路与命题逻辑的完全性定理相似。我们首先把 Γ 扩充成一个极大相容集 ∆ 还包括一族新的“辛钦公理”，以帮助我们处理量词。所谓辛钦公理的形式如下： ¬∀xφ → ¬φ x c , 其中 c 是“新的”常数符号。我们要做的其实是添加 ∃xψ → ψ x c ，即对每一个存在性的语句都添加一个直接证据 c。我们写成以上的等价形式是因为后面用起来更直接。本质上说，辛钦公理其实就是量词消去，代价是添加新的常数。有了这样的 ∆ 之后，我们很容易“读出”一个满足 ∆ 中（除了带等词的）所有公式的结构和赋值。首先我们向语言 L 中添加可数多个新的常数符号 C = {c0, c1, · · · }。把扩展后的语言记作 LC。我们验证 Γ 在新的语言中仍然是相容的。这听起来是显然的，但添加了常数符号后，公理变多了，我们还是有必要验证一下。（这实际上是后面归纳验证辛钦公理的相容性的一部分。）假如在扩张语言之后 Γ 变得不相容了，则存在（LC 内的）公式 β 和某个（LC 内的）从 Γ 到 β ∧ ¬β 的证明序列。注意到证明序列中包含的新常数符号为有穷多。我们可以用常数概括定理把它们都替换成变元，从而得到一个从 Γ 到 (β ′ ∧ ¬β ′ ) （在 L 中的）证明序列，其中 β ′ 是从 β 中把新常数符号替换成变元而得到的。由于 β ′ 是 L 中的公式，这与 Γ 的相容性矛盾。接下来我们添加所谓辛钦公理，即对所有（LC 中的）公式 φ 和所有的变元 x，我们都向 Γ 中添加公式 ¬∀xφ → ¬φ x c , 其中 c 是某个新常数符号。具体做法如下4：固定一个（LC 中）公式和变元有序对 (φ, x) 的枚举： (φ1, x1),(φ2, x2), · · · 2辛钦，Leon Henkin (1921 - 2006)，美国逻辑学家。 3完全性定理对不可数语言也成立，只不过证明要用到选择公理等集合论工具。 4另一种常见的做法是：从语言 L0 = L 出发，添加可数多常数 C0 使得 L0 中的公式都有辛钦公理相配，但语言扩展成 L1 = L0 ∪ C0 之后，我们还要添新的常数 C1 使得 L1 中的公式都有辛钦公理相配，如此下去，我们需要扩充 ω 步才能达到目的。 3

第 2 节完全性定理第 6 章哥德尔完全性定理枚举存在性是由语言的可数性保证的。令 θ1 为 ¬∀x1φ1 → ¬(φ1) x1 ci1 , 其中 ci1 为第一个不在 φ1 中出现的新常数符号。假如我们已经处理完了前 k 个有序对，并且定义了辛钦公理 {θ1, θ2, · · · , θk}，则令 θk+1 为 ¬∀xk+1φk+1 → ¬(φk+1) xk+1 cik+1 , 其中 cik+1 为第一个在 φ1 · · · , φk, φk+1, θ1, · · · , θk 中都不出现的新常数符号。这样不断地做下去，我们最终得到一个公式集 Θ = {θ1, θ2, · · · }。我们验证 Γ ∪ Θ 仍然是相容的：如果不相容的话，则根据证明序列的有限性和前面验证的 Γ 的相容性，就存在某个 m ≥ 0，使得 Γ ∪ {θ1, · · · , θm+1} 为不相容的。选取最小的这样的 m。根据（RAA） Γ ∪ {θ1, · · · , θm} ⊢ ¬θm+1。假设 θm+1 为 ¬∀xφ → ¬φ x c。根据重言规则，我们有 Γ ∪ {θ1, · · · , θm} ⊢ ¬∀xφ, 并且 Γ ∪ {θ1, · · · , θm} ⊢ φ x c。注意到 c 在表达式左边不出现，根据常数概括定理，我们有 Γ ∪ {θ1, · · · , θm} ⊢ ∀xφ, 这与 m 的极小性矛盾。我们在相容公式集 Γ ∪ Θ 继续扩张，以得到一个极大相容的公式集 ∆，即对任何公式 φ 或者 φ ∈ ∆ 或者 (¬φ) ∈ ∆。具体做法与命题逻辑中林登鲍姆引理的证明完全类似，这里不再重复。注意任何的极大相容集 ∆ 都对语法后承（或说对推导）封闭：如果 ∆ ⊢ φ，则相容性告诉我们 ∆ ̸⊢ ¬φ 所以 (¬φ) ̸∈ ∆，在根据极大性，就有 φ ∈ ∆。小结：我们扩充了语言，添加了辛钦公理集 Θ，并把 Γ ∪ Θ 扩充成一个极大相容集 ∆。下一步我们将从 ∆ 中“读出”一个新语言 LC 上的结构 A，但把等词 ≈ 暂时替换成一个新的二元谓词 E。（等词的处理将使我们下一步的工作。）结构 A 的定义如下： 4

第 2 节完全性定理第 6 章哥德尔完全性定理假如 φ 为 α → β，则 (A, s) |= (α → β) ∗ 当且仅当 (A, s) ̸|= α ∗ 或者 (A, s) |= β ∗ , 当且仅当 α ̸∈ ∆ 或者 β ∈ ∆, 当且仅当 ¬α ∈ ∆ 或者 β ∈ ∆。无论 ¬α ∈ ∆ 还是 β ∈ ∆，我们都有 ∆ ⊢ (α → β)。根据 ∆ 对推导的封闭性，我们有 (α → β) ∈ ∆。另一方面，如果 (α → β) ∈ ∆，则或者 α ̸∈ ∆ 或者 [α ∈ ∆ 并且 ∆ ⊢ β]。因而或者 ¬α ∈ ∆ 或者 β ∈ ∆，再反向倒溯上文的论证，就得到 (A, s) |= (α → β) ∗。假如 φ 为 ∀xψ，我们证明：(A, s) |= ∀xψ∗ 当且仅当 ∀xψ ∈ ∆ （注意我们用了 ∀xψ∗ 为 (∀xψ) ∗ 这一事实。）从左向右，我们先选好 c 为辛钦公理 ¬∀xψ → ¬ψ x c 中的常数 c，然后有： (A, s) |= ∀xψ∗ ⇒ (A, sx c ) |= ψ ∗ ⇒ (A, s) |= (ψ ∗ ) x c 由替换引理 ⇒ (A, s) |= (ψ x c ) ∗ ⇒ ψ x c ∈ ∆ ⇒ ¬ψ x c ̸∈ ∆ ⇒ (¬∀xψ) ̸∈ ∆ 因为 θ ∈ ∆ 并且 ∆ 对推导封闭 ⇒ ∀xψ ∈ ∆。从右向左，首先利用约束变元替换先选一个公式 ϕ 使得 ϕ 和 ψ 的差别仅在于约束变元（因而联词和量词的个数不变）并且 t（t 的选法见下文）在 ϕ 中可以替换 x。我们有 (A, s) ̸|= ∀xψ∗ ⇒ (A, sx t ) ̸|= ψ ∗ 对某个 t，选好并固定 ⇒ (A, sx t ) ̸|= ϕ ∗ 因为 ψ ∗ 和 ϕ ∗ 语义等价 ⇒ (A, s) ̸|= (ϕ x t ) ∗ 根据替换引理 ⇒ ϕ x t ̸∈ ∆ 根据归纳假设 ⇒ ∀xϕ ̸∈ ∆ ⇒ ∀xψ ̸∈ ∆ 根据约束变元替换引理。这就完成了对归纳情形的证明。小结：我们得到了一个结构 A 和一个赋值 s，它们满足 ∆ 里面所有不含等词 ≈ 的公式。我们下面处理等词。首先看看等词到底带来什么问题。回忆一下我们对等词的解释的特殊要求。例如，假定我们的语言中本来有常数符号 d，我们在添加辛钦公理时，会把 ∃x(x ≈ d) → c ≈ d 添加进去，其中 c 是一个新的常数符号，特别地，c ̸= d。所以 6

第6章哥德尔完全性定理第3节自然推演系统的可靠性和完全性第3节自然推演系统的可靠性和完全性我们沿用第??章第??节的自然推演系统。其可靠性是不难证明的,我们留作练习。我们下面证明它的弱完全性,即它可以证明所有的普遍有效式。至于自然推演中一般形式的完全性定理也是成立的,有兴趣的读者可以参考[?或其它证明论的参考书。我们已经有了辛钦的证明,该证明在模型论中非常有用,因为利用常数符号来构造模型是模型论中最基本的方法。在后面谈到紧致性定理和它的应用时,用到的方法本质上都是辛钦构造。我们下面给出的搜寻证明树的构造模型方法虽然也利用了项,但它提供给我们一些新的信息。一是可以得到一些证明论学家关心的性质,如,切割消去和所谓子公式性质,即如果一个公式是可证的,则存在一个(自然推演系统的)证明,其中出现的都是它的子公式。二是它提供给我们一些能行性的信息。这一点有些超前,我们点到为止。有些读者可能会关心哥德尔的完全性定理是否等在“有穷数学”中得到证明。从下面的证明我们清楚地看到,我们需要在某棵树上拿到一个无穷支。因此完全性定理不能在“有穷数学”中得到证明。精确的版本是反推数学中如下的定理:完全性定理等价于弱的柯尼西引理我们证明:如果圹I,则r不是普遍有效的。证明思路是:我们试图从r出发,寻找它的一个证明树。在寻找过程中,我们不用切割规则,而把其它推理规则倒过来用,并把 r里的公式分解成其子公式。由于T不是可证的,我们的寻找注定失败,但从失败当中我们可以读出一个让r不成立的模型(反模型)。细节如下: 首先把r中的公式排成一个序列,原子公式(如果有的话)在前。令a为序列中第个非原子公式,△为其余部分,则序列r形如 r=若干原子公式,a,△。然后我们用下述规则把a拆成其子公式,从而产生新的公式序列r',在(∧)情形中我们会得到两个新序列r和r1 ()r=若干原子公式,( ao v al),△,则r=同样原子公式,ao,an,△ (∧)r=若干原子公式,(aoAa1),△,则对i=0,1,r=同样原子公式,a,△。 ()T=若干原子公式,wr(x),△,则r"=同样原子公式,B(vy),△,其中v为一个迄今为止没有用到过的变元; ()r=若干原子公式,丑xB(x),△,则r=同样原子公式,B(vk),△,其中tk为 o,1,t2,…中第一个迄今为止没有用来当成彐rB(x)证据的变元 3弱的柯尼西引理, Weak Konig Lemma(WKLo),柯尼西, Denes konig(1884-1944),匈牙利数学家

第 6 章哥德尔完全性定理第 3 节自然推演系统的可靠性和完全性第 3 节自然推演系统的可靠性和完全性我们沿用第 ?? 章第 ?? 节的自然推演系统。其可靠性是不难证明的，我们留作练习。我们下面证明它的弱完全性，即它可以证明所有的普遍有效式。至于自然推演中一般形式的完全性定理也是成立的，有兴趣的读者可以参考 [?] 或其它证明论的参考书。我们已经有了辛钦的证明，该证明在模型论中非常有用，因为利用常数符号来构造模型是模型论中最基本的方法。在后面谈到紧致性定理和它的应用时，用到的方法本质上都是辛钦构造。我们下面给出的搜寻证明树的构造模型方法虽然也利用了项，但它提供给我们一些新的信息。一是可以得到一些证明论学家关心的性质，如，切割消去和所谓子公式性质，即如果一个公式是可证的，则存在一个（自然推演系统的）证明，其中出现的都是它的子公式。二是它提供给我们一些能行性的信息。这一点有些超前，我们点到为止。有些读者可能会关心哥德尔的完全性定理是否等在“有穷数学”中得到证明。从下面的证明我们清楚地看到，我们需要在某棵树上拿到一个无穷支。因此完全性定理不能在“有穷数学”中得到证明。精确的版本是反推数学中如下的定理：完全性定理等价于弱的柯尼西引理5。我们证明：如果 ̸⊢ Γ，则 Γ 不是普遍有效的。证明思路是：我们试图从 Γ 出发，寻找它的一个证明树。在寻找过程中，我们不用切割规则，而把其它推理规则倒过来用，并把 Γ 里的公式分解成其子公式。由于 Γ 不是可证的，我们的寻找注定失败，但从失败当中我们可以读出一个让 Γ 不成立的模型（反模型）。细节如下：首先把 Γ 中的公式排成一个序列，原子公式（如果有的话）在前。令 α 为序列中第一个非原子公式，∆ 为其余部分，则序列 Γ 形如： Γ = 若干原子公式, α, ∆。然后我们用下述规则把 α 拆成其子公式，从而产生新的公式序列 Γ ′，在 (∧) 情形中我们会得到两个新序列 Γ ′ 0 和 Γ ′ 1。 (∨) Γ = 若干原子公式，(α0 ∨ α1), ∆，则 Γ ′ = 同样原子公式，α0, α1, ∆； (∧) Γ = 若干原子公式，(α0 ∧ α1), ∆，则对 i = 0, 1，Γ ′ i = 同样原子公式，αi , ∆。 (∀) Γ = 若干原子公式，∀xβ(x), ∆，则 Γ ′ = 同样原子公式，β(vj ), ∆，其中 vj 为一个迄今为止没有用到过的变元； (∃) Γ = 若干原子公式，∃xβ(x), ∆，则 Γ ′ = 同样原子公式，β(vk), ∆，其中 vk 为 v0, v1, v2, · · · 中第一个迄今为止没有用来当成 ∃xβ(x) 证据的变元。 5弱的柯尼西引理，Weak König Lemma (WKL0)，柯尼西，Dénes König （1884 - 1944），匈牙利数学家。 9

第3节自然推演系统的可靠性和完全性第6章哥德尔完全性定理重复上述过程,我们就得到一个序列I,r’,r",…,并且可以排成树状,将r排在最下面,然后自下而上,依次添加r,r",…等等。例如,它有可能是注意到我们的生成规则恰好是把推理规则倒过来,因此在这棵树上,排在下面的r可以视为从排在它上面的r*按照自然推演规则导出的,(在(∧)情形中则是从r*和I中导出的)。如果发现树的某个节点上的公式集是一个公理,则停止这一支的构造。根据r不可证的假定,这棵树至少有一支,记为p,或者(a)终结于一个由原子公式组成的但不是公理的序列;或者(b)永不终结,即形成一个无穷支。从分支p中我们定义一个r的“反模型”a如下:论域||为自然数集N;对每个谓词符号P定义 (1,12,…,in)∈P当且仅当原子公式P(vn1,v2,…,tn)不在分支p中出现。引理65.令赋值函数s为s(v2)=i对任意在分支p中出现的公式a,都有(2,s)长ao 证明:对公式a施行归纳初始情形:a为原子公式P(v1,2,…,vn),则根据定义,(Ql,s)a 归纳情形:我们分成如下子情形来讨论: 子情形1:a为P(v1,2,…,vn)。由于P中不含公理,因此公式P(12,t2…,tn) 在p中不出现,所以(2,s)=P(vn1,tv2,…,tn),因而(,s)≠a 子情形2:α为ao∨a1。当我们处理a时,ao和a1都被添进p中。根据归纳假定我们有(,s)长a和(,s)长a1。所以(,s)≠长ao 子情形3:α为ao∧a1。当我们处理a时,a0和α1至少有一个被添进p中。根据归纳假定,我们至少有(,s)长a或(,s)长a1所以(,s)ka 子情形4:α为vrβ(x)。当我们处理α时,某个β(υ)被添进p中。根据归纳假定, 我们有(,s)≠B(vy)。所以(,s)长a 子情形5:α为彐rβ(x)。根据构造,我们会处理a无穷多次,在每次处理它时,j最小的那个还不在p中的β(v)被添进p中。所以,对每一个自然数i,B(v)都在p中出现。根据归纳假定,对每一个自然数,我们有(,s)≠B(v)。所以(,s)≠a 这就完成了引理的归纳证明。推论63(甘岑1936).如果r是自然推演系统的一个定理,则有一个r的证明树其中没有用到切割规则。证明:假定}r。根据可靠性定理,}I。所以如果我们用完全性定理证明中的方法来搜索,结果一定找不到r的反模型。因此一定得到r的一个证明树。根据构造,这棵证明树显然没有用到切割规则

第 3 节自然推演系统的可靠性和完全性第 6 章哥德尔完全性定理重复上述过程，我们就得到一个序列 Γ, Γ ′ , Γ ′′ , · · · ，并且可以排成树状，将 Γ 排在最下面，然后自下而上，依次添加 Γ ′ , Γ ′′ , · · · 等等。例如，它有可能是： Γ ′′ 0 Γ ′′ 1 Γ ′ Γ 。注意到我们的生成规则恰好是把推理规则倒过来，因此在这棵树上，排在下面的 Γ ∗ 可以视为从排在它上面的 Γ ∗∗ 按照自然推演规则导出的，（在 (∧) 情形中则是从 Γ ∗∗ 0 和 Γ ∗∗ 1 中导出的）。如果发现树的某个节点上的公式集是一个公理，则停止这一支的构造。根据 Γ 不可证的假定，这棵树至少有一支，记为 p，或者 (a) 终结于一个由原子公式组成的但不是公理的序列；或者 (b) 永不终结，即形成一个无穷支。从分支 p 中我们定义一个 Γ 的“反模型”A 如下：论域 | A | 为自然数集 N；对每个谓词符号 Pj 定义： (i1, i2, · · · , in) ∈ P A j 当且仅当原子公式 Pj (vi1 , vi2 , · · · , vin ) 不在分支 p 中出现。引理 6.5. 令赋值函数 s 为 s(vi) = i。对任意在分支 p 中出现的公式 α，都有 (A, s) ̸|= α。证明: 对公式 α 施行归纳。初始情形：α 为原子公式 Pj (vi1 , vi2 , · · · , vin )，则根据定义，(A, s) ̸|= α。归纳情形：我们分成如下子情形来讨论：子情形 1：α 为 Pj (vi1 , vi2 , · · · , vin )。由于 p 中不含公理，因此公式 Pj (vi1 , vi2 , · · · , vin ) 在 p 中不出现，所以 (A, s) |= Pj (vi1 , vi2 , · · · , vin )，因而 (A, s) ̸|= α。子情形 2：α 为 α0 ∨ α1。当我们处理 α 时，α0 和 α1 都被添进 p 中。根据归纳假定，我们有 (A, s) ̸|= α0 和 (A, s) ̸|= α1。所以 (A, s) ̸|= α。子情形 3：α 为 α0 ∧ α1。当我们处理 α 时，α0 和 α1 至少有一个被添进 p 中。根据归纳假定，我们至少有 (A, s) ̸|= α0 或 (A, s) ̸|= α1。所以 (A, s) ̸|= α。子情形 4：α 为 ∀xβ(x)。当我们处理 α 时，某个 β(vj ) 被添进 p 中。根据归纳假定，我们有 (A, s) ̸|= β(vj )。所以 (A, s) ̸|= α。子情形 5：α 为 ∃xβ(x)。根据构造，我们会处理 α 无穷多次，在每次处理它时，j-最小的那个还不在 p 中的 β(vj ) 被添进 p 中。所以，对每一个自然数 i，β(vi) 都在 p 中出现。根据归纳假定，对每一个自然数 i，我们有 (A, s) ̸|= β(vi)。所以 (A, s) ̸|= α。这就完成了引理的归纳证明。推论 6.3 (甘岑 1936). 如果 Γ 是自然推演系统的一个定理，则有一个 Γ 的证明树其中没有用到切割规则。证明: 假定 ⊢ Γ。根据可靠性定理，|= Γ。所以如果我们用完全性定理证明中的方法来搜索，结果一定找不到 Γ 的反模型。因此一定得到 Γ 的一个证明树。根据构造，这棵证明树显然没有用到切割规则。 10

复旦大学：《数理逻辑》课程教学资源（讲义）第6章 哥德尔完全性定理

复旦大学：《数理逻辑》课程教学资源（讲义）第6章哥德尔完全性定理