第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