直觉主义完全性（逻辑论文）

直觉主义完全性

经典逻辑的语形后承和语义后承等价。从我们在第五、六章中获得的经验来看，直觉主义逻辑严格弱于经典逻辑，因此，它的语形后承不对应于经典语义后承。那么，对直觉主义推演，我们能不能找到一个合适的语义恰好刻画它呢？本节回答这个问题。我们要描述一种特殊的语义，证明直觉主义逻辑对于这个语义也有可靠性与完全性。

首先说明两点。第一，直觉主义逻辑有没有甚至需不需要语义学，本身就是个问题。严格的直觉主义者不承认他们的逻辑观念有语义刻画（他们甚至不承认直觉主义推演的形式化），所谓「直觉主义语义」，因此只是对于直觉主义观念的一种代数描述，而并不严格表达直觉主义的哲学观点。这与经典逻辑的情形不同：经典语义虽然也是一种代数结构，但它同时提供了对于逻辑常项的经典哲学解释。第二，在经典逻辑的立场上，可以为直觉主义逻辑设计不同的「语义解释」，但这些语义学使用的语言与逻辑，仍然是经典的，所以它们可以看作在直觉主义之外对其推演概念的一种理解。在这些不同的设计中，Kripke 语义较为简明，其直观图景也更能帮助我们理解直觉主义的思想。我们下面介绍Kripke语义。

以下的讨论里，我们使用一个固定的一阶语言。为了突出直观思路而避免细节的繁杂，我们假设不含等词，但含有足够多的个体常项；而且，我们只关心-语句，所有的描述与证明，都是针对语句的。

8.1 直观描述

大体而言，哲学上的直觉主义主张，数学是个体的构造性的心智活动，而逻辑则标示和研究数学构造过程中的特定规则，因此数学先于逻辑。数学对象产生于某种先天的直觉。比如，自然数列源于某种关于时间的原始直觉，这种直觉从一个自然呈现的单位开始，意识到这个单位自身迭加的可能性，从而产生数1、2等等。这是一个潜无穷的构造过程，永无终点。数学命题的意义即是它的证明或构造：我们构造了7，构造了5，把它们「合起来」，发现这正是12的构造结果，这就是「7+5=12」的意义。命题中逻辑常项的意义也必须用构造这个基本概念来解释：当我们说存在具有某性质的数时，这只是意味

着我们已经构造出了具有这个性质的

一个具体数；反之，当我们说不存在这样的数时，这并不意味着我们已经穷尽了「所有」数而终未发现它我们没有能力「统观」整个过程），而只能意味着我们证明了这个存在命题导致矛盾。所以，我们不能在正反两个证明或构造都未得到时就无条件地断定或者有或者没有这样的数（排中律不成立）。

因此，没有一个已经完成的所有数学对象的集合，也没有一蹴而就的总体理论，一切都在构造中增长。我们想象一个理想的直觉主义数学家（「创造主体」），他在时间进程中自由地扩大他的论域，积累他的知识。在每个时刻i，他都拥有业已构造出的一组个体 D(i)，它们也可以说是一组业已确定了有指称的项（对一些直觉主义者来说，数学对象其实就是指称它们的项，即符号串）；此外，他还拥有一组关于D (i) 中的元素的基本知识A(i)，它们都是原子语句，被他直接「直觉」到，或从仅涉及原子语句的规则推出。这个数学家在时间进程中的可能的活动方式，组成一个偏序（甚至一个树），就是说，对于将来的某时刻j，他的D(j)和A (j)不是被D(i)和A(i)所唯一决定的，他可以用不同的方式扩大他的论域和基本知识，甚至在某一点干脆停下来。但是，个体一旦构造，便不会消亡；命题一经证明，便永远成立。所以，D(i) ⊆D (j)，A (i)

⊆A(j)。

那么，这个数学家如何确立复合语句呢？他依据的是直觉主义的可证性原则：确立一个命题就是提供它的一个证明，而联结词和量词的意义，也由此决定：

φ∧ψ的证明由φ的证明加上ψ的证明构成；

φ∨ψ的证明由φ的证明或者ψ的证明构成；

φ→ψ的证明是一个构造方法，它把每个φ的证明转换为ψ的一个证明；

φ的证明是一个构造方法，它把每个φ的证明转换为对于矛盾或荒谬句(如0=1)的证明(即证明φ没有证明)。

∀xφ的证明是一个构造方法，它对每个有指称的项t，导出φ(t/x)的证明。

∃xφ的证明是φ(t/x)的证明，其中的项t是某个已知的有指称的项。

在每个时刻i，A(i)包含基本的可证的语句，或「真」的语句，这为递归定义「φ在i时刻为真」提供了一个基始。但是，凡是牵涉到构造方法的证明，都不仅涉及当下的时刻，而且涉及将来，因为方法是可以普遍应用的。所以，φ→ψ在 i 时刻为真，如果有一个构造方法，它不仅在i时刻而且在将来也把每个φ的证明转换为ψ的一个证明。同样，φ在 i 时刻为真，如果不仅在 i 时刻而且在将来φ的证明都导致矛盾；∀xφ在 i 时刻为真，如果对将来 (包括 i 时刻) 每个有指称的项，都有

φ (t/x) 的证明。

8.2 Kripke 模型

Kripke 依据上面的直观图景，建立了下面的语义概念。

8.2.1 定义一个 Kripke 模型𝕶是一个如下规定的四元组〈l，≤，D，A〉：

1) l是一个非空指标集，其中的

指标i，j等也称为状态。

2) ≤ 是l上的偏序。

3)对每个i∈l，D(i)是一个非空的闭项集，满足对任意j∈l，i≤j

D (i) ⊆D(j)。

4)对每个i∈l，A (i)是一个原子语句的集合，其中出现的项都在D(i)中，且对任意j∈l，i≤jA(i)⊆A(j)。

指标集 l 包含所有可能的状态。这里状态的直观含义不仅是时刻，还包括这个时刻的论域大小、知识状况等。D (i)是 i 状态下已知有指称的项组成的集合，这些项的指称构成i状态的论域。A (i)是 i 状态下的基本知识，也就是此时为真的原子语句。对每个 i，i状态的论域和A(i)构成一个经典结构，其中的基本关系由A (i)决定：Pt ₁，···，t ₙ，∈A (i)，当且仅当

t ₁，···，t ₙ的指称具有 P 所表达的关系。在将来的状态里，结构的论域扩大，关系增加。所以，Kripke 模型可以说描述了动态的经典结构。

函数A可以扩张为如下赋值函数：

8.2.2 定义 对于𝕶＝〈1，≤，D，A〉，语句 φ 在𝕶中的 i 状态下为真，记为𝕶(i，φ)＝T；φ在𝕶中的 i 状态下为假，如果𝕶 (i，φ)≠T，记为𝕶(i，φ)＝F。𝕶(i，φ) 是如下递归定义的唯一的函数的值：

1)φ是原子语句。𝕶(i，φ)＝T⇔φ∈A (i)。

2)φ为ψ。𝕶(i，φ)＝T⇔对任意j∈l，若i≤j，则𝕶(j，ψ)＝F。

3)φ为ψ ₁ ∧ψ ₂ 。𝕶(i，φ)＝T⇔𝕶(i，ψ ₁) ＝𝕶（i，ψ ₂)＝T。

4)φ为ψ ₁ ∨ψ ₂ 。𝕶(i，φ)＝T⇔𝕶(i，ψ ₁)＝T或𝕶(i，ψ ₂)＝T。

5)φ为ψ ₁ →ψ ₂ 。𝕶(i，φ)＝T⇔对任意j∈l，若i≤j，则(𝕶 (j，ψ ₁)＝T ⇒𝕶(j，ψ ₂)＝T)。

6)φ为∀xψ。𝕶(i，φ)＝T⇔对任意j∈l，任意t∈D (j)，若i≤j，则𝕶 (j，ψ (t / x) )＝T。

7)φ为∃xψ 。𝕶(i，φ)＝T⇔存在t∈D (i)，使得𝕶 (i，ψ (t/x) )＝T。

否定式、蕴涵式与全称式的真假，都与未来状态有关。2) 表明，ψ在某状态下为真 (可证)，意味着ψ不仅在此状态下为假 (无证明)，而且永假 (永无证明)，即荒谬。5) 表明，要确定蕴涵式的真假，我们不必知道前后件的真假，只要前件的证明永远能转换为后件的证明，蕴涵式就是真的 (可证的)。6) 表明，全称式不仅涉及当前状态里的个体，而且包括未来状态的所有个体。其余语句的真假，只与当前的状态有关。

根据2)和3)矛盾句在任何的任何𝕶状态下为假。

从定义可推出如下的「单调性」引理：

8.2.3 引理 设φ是语句。对任意𝕶＝〈I，≤，D，A) 和i，j∈l，i≤j，

如果𝕶 (i，φ)＝T，则𝕶 (j，φ)＝T。

证明：施归纳于φ。假设𝕶 (i，φ)＝T。

1) φ 是原子公式。由定义

8.2.1-4，A(i) ⊆ A (j)。再由8.2.2-1 即得结果。

2)φ为ψ。由定义8.2.2-2 即得结果。

3)φ为ψ ₁ ∧ψ ₂ 。

𝕶(i，φ)＝T

⇒𝕶 (i，ψ₁)＝𝕶 (i，ψ₂)＝T(定义8.2.2-3)

⇒𝕶 (j，ψ₁)＝𝕶 (j，ψ₂)＝T(归纳假设)

⇒𝕶 (j，φ)＝T(定义8.2.2-3）。

4) φ为ψ ₁ ∨ψ ₂ 。与3) 类似。

5) φ为ψ ₁→ψ ₂。令j≤k。如果𝕶(k，φ ₁)＝T，则由于i≤k，有𝕶(k，ψ ₂)＝T。由定义 8.2.2-5，𝕶(j，φ)＝T。

6) φ为∀xψ。令j≤k。由于i≤k，所以对任意t∈D (k)，有𝕶 (k，ψ (t/x) )＝T。由定义8.2.2-6，𝕶(j，φ)＝T。

7) φ为∃xψ。由定义 8.2.1-3

与8.2.2-7 即得结果。

引理说明，我们的知识是单调递增的，命题一旦为真，则永远为真。

8.3 可靠性

模仿经典语义的情形，我们可以定义Kripke语义的后承概念。首先扩展一下术语：如果Φ是语句集，那么我们用𝕶 (i，Φ)＝T表示：对于任意φ∈Φ，𝕶 (i，φ)＝T。

8.3.1 定义设Φ是语句集，φ为语句。如果对于任意的Kripke 模型𝕶和𝕶中任意状态 i，只要𝕶(i，Φ)＝T.就有𝕶 (i，φ)＝T，则称φ是Φ的𝕶-语义后承，记为Φ╟φ。

ø╟φ记为 ╟φ 。这意味着，对于任意的𝕶和𝕶中任意状态 i，都有𝕶(i，φ)＝T。

下面证明，相对于这个语义后承概念，直觉主义逻辑是可靠的。

8.3.2 直觉主义逻辑的可靠性定理 设Φ是语句集，φ为语句。

如果Φ￾ ᵢ φ那么Φ╟φ。

证明：Φ￾ ᵢ φ，当且仅当有直觉主义推演，其前提在Φ中，结论是φ。因此，我们只要证明，对任何这样的推演 D，都有Φ╟φ。下面我们固定𝕶＝〈I，≤，D，A〉，施归纳于 D。

1) D是单点树 φ。此时φ∈Φ，显然有Φ╟φ。

2) D是最后一步应用合取、析取或蕴涵的引入或消去规则，归谬法规则或直觉主义规则 (IN)得到的推演。我们只证明 (→I) 和 (VE) 的情形。其他情形留作习题。

(→I) [ψ ₁]

D₁

ψ ₂

────

ψ ₁ → ψ ₂

D ₁ 的结论为ψ ₂，前提比 D 的前提多了一个

ψ ₁ 。此时归纳假设为Φ∪{ψ ₁}╟ψ ₂ 。我们要证：对𝕶中任意状态 i，只要 𝕶(i，Φ)＝T，就有𝕶(i，ψ ₁ →ψ ₂)＝T。

设𝕶(i，Φ)＝T。根据单调性引理 (8.2.3)，对j∈l，i≤j，我们有𝕶(j，Φ)＝T。如果𝕶(j，ψ ₁)＝T，则𝕶 (j，Φ∪{ψ ₁} )＝T。根据归纳假设，此时有𝕶 (j，ψ ₂) ＝T。由定义8.2.2-5，𝕶(i， ψ ₁ → ψ ₂)＝T。

(∨E) [ψ ₁] [ψ ₁]

D₁ D₂ D₃

ψ₁∨ψ₂ φ φ

─────────

φ

设D ₁、D ₂、D ₃ 的前提集分别

为Φ ₁、Φ ₂、Φ ₃，则Φ＝Φ ₁，∪

{Φ ₂ — {ψ ₁} ) ∪ (Φ ₃ — {ψ ₂} )。针对

D ₁、D ₂、D ₃ 的归纳假设分别为：

(*)Φ ₁ ╟ψ ₁ ∨ψ ₂；

(*) Φ ₂ ╟φ；

(***)Φ ₃ ╟φ。

对𝕶中任意状态 i，设𝕶(i，Φ)＝T，我们要证𝕶 (i，φ)＝T。

由于Φ ₁，⊆Φ，所以𝕶(i，Φ ₁)＝T。根据(*)，𝕶(i，ψ ₁ ∨ ψ ₂)＝T。由定义 8.2.2-4，

𝕶(i，ψ ₁)＝T或𝕶(i，ψ ₂)＝T.

如果𝕶(i，ψ ₁)＝T，那么根据𝕶(i，Φ)＝T，有𝕶 (i，Φ ₂)＝T。再由(**)𝕶(i，φ)＝T。

如果𝕶(i，ψ ₂)＝T，那么根据(***)同理可证，𝕶(i，φ)＝T。

总之，𝕶(i，φ)＝T。

3) D 的最后一步应用量词规则。由于我们只考虑语句组成的推演，所以 (∀l) 和 (∃E) 需要稍作改动，用个体常项代替其中的关键自由变项。但这些常项为了能够保持「任意性」，也必须满足原先对于变项的那些限制条件，具体见以下的叙述：

(∀l) D₁

ψ (a/x)

───

∀xψ

条件是：常项 a 不在前提集Φ中出现。因此，D ₁，实际上是一个推演模式，其前提未规定a有任何特殊性质，换言之，在a的位置上可以代以任何项t而仍然能够从原前提依据D ₁，推

出 ψ (t / x)。因而，我们可以有全称的结论。

此时的归纳假设为：Φ ╟ψ (a /x)。由a的「任意性丨，这意味着，对𝕶中任意状态i，如果𝕶 (i，Φ)＝T，则对任何t∈D (i)，都有𝕶 (i，ψ(t / x) )＝T。

现在假定 𝕶(i，Φ)＝T，我们要证𝕶 (i，∀xψ)＝T。根据单调性引理，对j∈l，i≤j，我们有𝕶 (j，Φ)＝T。由归纳假设，对任何t∈D (j)，𝕶(j，ψ (t / x) )＝T。因此，据定义

8.2.2-6，𝕶(i，∀xψ)＝T。

再考虑D的最后一步应用 (∃E) 的情形。

(∃E) [ ψ(a / x) ]

D₁ D₂

∃xψ φ

────────

φ

其中a满足如下条件：第一，a不在∃xψ中出现；第二，a不在φ中出现；第三，a不在D ₂，的除ψ (a / x)以外的前提中出现。这些条件保证了a的「任意性」，也保证了D ₂，的结论φ独立于a。这些条件满足后，对任何项t，我们都能依据D ₂ 从 ψ (t / x) (和D ₂ 的其他前提) 得到φ。

设D ₁，和D ₂，的前提集分别为 Φ ₁ 和Φ ₂ ∪{ψ (a / x) }，则D的前提集Φ＝Φ，∪Φ₂ 。

对于D ₁ 的归纳假设为：Φ ₁╟∃xψ。对于D ₂ 的归纳假设为：Φ ₂ ∪ {ψ(a / x) } ╟φ，即对𝕶中任意状态i，任何t∈D (i)，如果𝕶 (i，Φ ₂ ∪{ψ (t / x) } )＝T，则𝕶(i，φ)＝T。

现在假定𝕶 (i，Φ)＝T，我们要证𝕶 (i，φ)＝T。根据Φ ₁ ⊆Φ 和对于D ₁ 的归纳假设，存在t∈D (i)，使得𝕶 (i，ψ ( t/ x) )＝T。再由Φ ₂，⊆Φ，我们有𝕶 (i，Φ ₂ ∪ {ψ (t / x) } )＝T。最后根据对于D ₂ 的归纳假设，𝕶(i，φ)＝T。

量词规则的其他两种情形，留作习题。

我们把𝕶中 i 状态下为真的语句集

{φ│𝕶 (i，φ)＝T}记为Th (i)。从可靠性定理，我们得到以下的系理：

8.3.3 系理 对任何𝕶和𝕶中任何 i，如果Th (i)

￾ ᵢ φ，则φ∈ Th (i) 。

证明：设Th (i) ￾ ᵢ φ。根据可靠性定理，Th (i) ╟φ。因此，对𝕶中任何 j，若𝕶 (j，Th (i) )＝T，则𝕶(j，φ)＝T。特别地，𝕶(i，Th (i) )＝T，所以𝕶 (i，φ)＝T，即 φ∈Th (i) 。

所以，Th (i) 包含了它能推出的所有结论，或者说，它对直觉主义推演是封闭的。

8.3.4系理 如果是原子语

句，则Th(i) ￾ ᵢ φ⇔φ∈A (i)。

证 明：

Th(i)├ ᵢ φ⇔φ∈Th(i) (系理8.3.3)

⇔𝕶 (i，φ)＝T (Th(i)定义)

⇔ φ ∈ A(i) (φ是原子句，定义8.2.2-1)。

这就是说，我们从Th (i) 推不出不在 i 状态中为真的原子语句。一个状态的基本知识，不因推理而增加。

我们在前面诸章中一直声言，排中律、双重否定等经典逻辑定理不是直觉主义逻辑定理，但始终未证明这一点。现在我们可以方便地给出证明。

8.3.5系理 并非对任意语句φ，￾ ᵢ φ∨φ。

证明：对某原子句 φ，构造下面的简单的 Kripke模型𝕶：

指标集 l＝{i，j}；

≤＝{〈i，j〉}；

A (i)＝∅，A (j)＝{φ}

(在状态 i 中没有原子知识，在状态 j 中原子知识仅为 φ)。

那么，因为A (i)＝∅，所以由

定义8.2.2-1，𝕶(i，φ) ≠T。

又因为A (j)＝{φ}，所以同样由定义8.2.2-1，𝕶(j，φ)＝T。

但i≤j，根据定义8.2.2-2，𝕶(i，φ) ≠T。

于是，𝕶(i，φ) ≠T 且𝕶(i，φ) ≠T。再由定义8.2.2-4，𝕶(i，φ∨φ) ≠T。

因此，并非╟φ∨φ。据可靠性定理，并非

￾ ᵢ φ∨φ。

既然在直觉主义逻辑中，排中律、反证法、二难推理、双重否定消去、皮尔斯律等等相互等价，那么，依据这个系理，它们都不是直觉主义逻辑定理。

8.4完全性

直觉主义逻辑完全性的证明，大体上也采取经典情形下的步骤。我们需要类似前面的极大化引理和可靠性引理，使用 Henkin方法，得到最后的结果。但这里的情况毕竟不同，我们首先定义一个新的概念。

8.4.1 定义语句集Φ称为一个素理论，如果

1) 中是 i-一致的，即存在 φ，并非中Φ￾ ᵢ φ。

2)对任意语句φ，Φ￾ ᵢ φ⇒φ∈Φ ( Φ对直觉主义推演是封闭的)。

3) φ∨ψ∈Φ⇒φ∈Φ或ψ∈Φ。

4) ∃xφ∈Φ⇒φ(t / x) ∈Φ，对Φ的语言的某个闭项t。

素理论的作用，类似于经典情形下的（包含证据的）极大一致集。我们知道，每个经典结构中为真的全体语句构成一个极大一致集。与此类似，𝕶中每个 i 状态下为真的语句集Th (i) 也是一个素理论：首先，由系理 8.3.3，Th (i)对直觉主义推演是封闭的。再由定义 8.2.2，Th (i)满足素理论定义的3) 和4) 。最后，Th (i)推不出矛盾句，否则由它的封闭性，i 状态中就有矛盾为真。

下面的极大化引理相当于前面的「添加证据」与「极大一致扩张」的结合。注意，我们一直在一个固定的语言里谈论语句和语句集，但下面的扩张，涉及到更大的语言。

8.4.2 直觉主义极大化引理设Φ是-语句集，φ是-语句。如果并非 Φ￾ ᵢ φ，那么，存在素理论Ψ，使得Φ⊆Ψ，且并非Ψ￾ ᵢ φ。

证明：首先，往语言里添加可数无穷多个体常项，把扩张为。

其次，我们针对的存在句和析取句，逐步往Φ中添加证据式和析取支。为此，如下归纳定义-语句集的序列Ψ ₀，Ψ ₁，··· ：

1) Ψ ₀ ＝Φ。

2) 假设Ψ ₙ，已经定义，且并非Ψ ₙ ￾ ᵢ φ。

i)如果 n 为偶数，则找到第一个满足Ψ ₙ ￾ ᵢ ∃xψ而且其证据式尚未得到添加的-存在句 ∃xψ。定义Ψ ₙ₊₁＝Ψ ₙ ∪ {ψ (c / x ) }，其中 c 为不在

Ψ ₙ 、ψ 中出现的第一个新常项 (Ψ ₙ，中只含有穷多新常项，因此可以找到这样的 c)。

ii)如果 n 为奇数，则找到第一个满足Ψ ₙ ￾ ᵢ ψ ₁ ∨ψ ₂，而且其析取支尚未得到添加的-析取句

ψ ₁ ∨ψ ₂ 。定义：

Ψₙ∪{ψ₁}4如果并非Ψₙ ∪{ψ₁}├ ᵢφ；

Ψₙ₊₁＝

Ψₙ ∪{ψ₂}否则。

注意，如果Ψ ₙ ∪{ψ ₁} ￾ ᵢ φ，则不会有Ψ ₙ ∪ {ψ ₂} ￾ ᵢ φ。否则据 (∨E)，有Ψ ₙ ￾ ᵢ φ 。这与关于 Ψ ₙ，的假设矛盾。

现在令Ψ＝∪ {Ψ ₙ│ n≥0}。显然，Φ⊆Ψ。

下面验证，并非Ψ￾ ᵢ φ，而且 Ψ 是 (相对于语言的) 素理论。

1) 并非Ψ￾ ᵢ φ，

我们归纳证明：对任意n≥0，并非Ψ ₙ ￾ ᵢ φ。

a) n＝0 时，结果由引理假设保证。

b) 假设并非Ψ ₙ ￾ ᵢ φ。

n是奇数时，Ψ ₙ₊₁＝Ψ ₙ ∪ {ψ ₁} 或 Ψ ₙ₊₁＝Ψ ₙ ∪ {ψ ₁}。由定义知，二种情形下都有：并非

Ψ ₙ₊₁ ￾ ᵢ φ。

n是偶数时，Ψ ₙ₊₁＝Ψ ₙ ∪ {ψ (c / x) }。如果

Ψ ₙ ∪{ψ (c / x) } ￾ ᵢ φ，则由于 Ψ ₙ ￾ ᵢ ∃xψ，据我们新的存在消去规则 (见定理8.3.2)，有

Ψ ₙ ￾ ᵢ φ。这与归纳假设矛盾。

总之，并非 Ψ ₙ₊₁ ￾ ᵢ φ。归纳证明完毕。

2) Ψ 是 (相对于语言的) 素理论。

a) 因为并非 Ψ￾ ᵢ φ，所以 Ψ 是i-一致的。

b)设 ∃xψ∈Ψ。因此，Ψ￾ ᵢ ∃xψ。令 n 是使得Ψ ₙ ￾ ᵢ ∃xψ 的最小的数。那么，在第n步之前，∃xψ 的证据式未得到添加。但是，对某个m≥n，∃xψ 在第 m 步得到处理。因此，对某个c，ψ(c / x)∈Ψ ₘ₊₁，故ψ (c / x) ∈Ψ。

c) 设ψ ₁ ∨ψ ₂ ∈Ψ。令 n 是使得 Ψ ₙ ￾ ᵢ ∨ψ ₂

的最小的数。那么，对某个m≥n，ψ ₁，∨ψ ₂在第 m 步得到处理。因此，ψ ₁ ∈Ψ ₘ₊₁，或

φ ₂ ∈Ψ ₘ₊₁，故ψ ₁，∈Ψ 或ψ ₂ ∈Ψ。

d) Ψ 对直觉主义推演是封闭的。

如果 Ψ￾ ᵢ ψ，则 Ψ￾ ᵢ ψ∨ψ。有最小的 n，使得Ψ ₙ ￾ ᵢ ψ∨ψ。根据 c)，ψ∈Ψ。

在目前的阶段，我们得到了语句集的素理论扩张，这相当于获得了经典情形下的包含证据的极大一致集。下一阶段的任务是建立由这样的集合决定的「项结构」，从而证明「可满足性引理」。但是，对于一个Kripke模型𝕶来说，其中每个状态i下的D(i)和A(i)都对应一个经典项结构。因此，我们需要的不是一个，而是一组素理论，来建立Kripke「项模型」。

8.4.3 定义 𝕶ₚ是如下定义的

Kripke模型（I ₚ ，⊆，D，A）：

1) lₚ＝{Φ│Φ是素理论}；

2) ⊆ 是子集关系；

3) 对每个Φ∈l ₚ，D(Φ)是Φ中闭项的集合；

4) 对每个Φ∈l ₚ，A(Φ)＝{φ│φ 是原子语句，且Φ￾ ᵢ φ}。

由引理 8.4.2，存在素理论，因此 l ₚ 是非空的，D (Φ)也是非空的。⊆ 显然是一个偏序。如果Φ⊆Ψ，那么A(Φ) ⊆A(Ψ)，且D (Φ)⊆ D (Ψ)。因此，𝕶ₚ的确是一个 Kripke 模型。

因此，给定一个素理论Φ，我们就有𝕶ₚ中的一个状态Φ，或者说，一个「经典结构」，其论域为项集D (Φ)，论域中的基本关系由A (Φ)决定。按照Henkin方法，我们需要证明，理论Φ 恰好被状态Φ所「满足」，即理论Φ中的语句恰好是状态Φ中的真语句。

下面证明 Henkin定理的这个直觉主义版本。

8.4.4 直觉主义可满足性引理对于𝕶ₚ中的每个

Φ∈l ₚ，Φ＝Th (Φ)。

证明：我们要证，对任意语句φ，φ∈Φ当且仅当𝕶ₚ(Φ，φ)＝T。施归纳于 φ 的秩。

1)φ是原子句。

φ∈Φ

⇔Φ├ ᵢ φ(Φ 对直觉主义推演封闭)

⇔φ∈A(Φ)(A(Φ)定义)

⇔ 𝕶 ₚ (Φ，φ)＝T(定义8.2.2)。

2)φ是合取式。易证。

3)φ是ψ ₁ ∨ψ ₂ 。

ψ₁∨ψ₂∈Φ

⇔ψ₁∈Φ或ψ₂∈Φ (素理论性质)

⇔𝕶 ₚ(Φ，ψ₁)＝T或𝕶 ₚ (Φ，ψ₂)＝T (归纳假设)

⇔𝕶 ₚ(Φ，ψ₁∨ψ₂)＝T(定义8.2.2)。

4)φ是ψ ₁ →ψ ₂ 。

设 ψ ₁ →ψ ₂ ∈Φ。令Ψ∈l ₚ，使得 Φ ⊆ Ψ。如果𝕶ₚ (Ψ，ψ ₁)＝T，则由归纳假设，ψ ₁ ∈Φ。据Φ 的封闭性，ψ ₂ ∈Φ。再由归纳假设，𝕶ₚ(Ψ，ψ ₂)＝T。所以，𝕶ₚ(Ψ，ψ ₁ →ψ ₂)＝T。

反之，设ψ ₁ → ψ ₂ ∉Φ。那么，由Φ的封闭性，并非Φ ￾ ᵢ ψ ₁→ψ ₂ 。所以，并非Φ∪{ψ ₁} ￾ ᵢ ψ ₂ 。根据极大化引理(8.4.2)，存在素理论 Ψ，使得Φ∪{ψ ₁}⊆Ψ，且并非 Ψ￾ ᵢ ψ ₂ 。因此，Φ⊆Ψ，且ψ ₂ ∉Ψ。由归纳假设，𝕶ₚ(Ψ，ψ ₂)＝F。据定义8.2.2，𝕶ₚ(Ψ，ψ ₁ →ψ ₂)＝F。

5)φ是ψ。设θ为一矛盾句。

￢ψ∈Φ

⇔ ψ → θ∈Φ (├ ᵢ￢ψ ↔ (ψ→θ)，并且 Φ 对直觉主义推演封闭 )

⇔𝕶 ₚ(Φ，ψ → θ)＝T(根据4) )

⇔ 对任意Ψ∈lₚ，若Φ⊆Ψ，则 (𝕶 ₚ(Ψ，ψ)＝T ⇒𝕶 ₚ (Ψ，θ)＝T)

⇔ 对任意Ψ∈lₚ，若Φ⊆Ψ，则𝕶 ₚ (Ψ，ψ)＝F

(因为 𝕶 ₚ (Ψ，θ)＝F)

⇔ 𝕶 ₚ(Ψ，￢ψ)＝T(定义8.2.2)。

6) φ是∃xψ。设∃xψ∈Φ。既然Φ是素理论，那么存在项t，使得ψ (t / x) ∈Φ。t出现在Φ中，因此t∈D(Φ)。据归纳假设，𝕶ₚ(Φ，ψ (t / x) )＝T。由定义 8.2.2，𝕶ₚ(Φ，∃xψ)＝T。

反之，设𝕶ₚ (Φ，∃xψ)＝T。那么存在t∈D (Φ)，使得𝕶ₚ (Φ，ψ(t / x) )＝T。据归纳假设， ψ (t / x)∈φ。但 ￾ ᵢ ψ (t / x) →∃xψ。由Φ的封闭性，∃xψ∈Φ。

7)φ是∀xψ。留作习题。

现在，准备工作都已完成，让我们推导最后的结果。

8.4.5 直觉主义逻辑完全性定理 (Kripke) 设Φ 是语句集，φ为语句。

Φ╟φ⇒Φ￾ ᵢ φ。

证明：假定并非 Φ￾ ᵢ φ，那么，根据极大化引理，存在素理论Ψ，使得Φ⊆Ψ，但并非Ψ￾ ᵢ φ ──因此φ∉Ψ。Ψ既然是素理论，它就是𝕶ₚ的一个状态。由可满足性引理

(8.4.4)，Ψ＝Th (Ψ)。于是，Φ ⊆ Th (Ψ)，但φ∉Th(Ψ)。

以上证明了：如果并非 Φ￾ ᵢ φ，那么，存在Kripke模型𝕶(即𝕶ₚ) 和其中的状态 i (即Ψ)，使得𝕶 (i，Φ)＝T，而𝕶 (i，φ)＝F──就是说：并非Φ╟φ。

注释

①一致性是对于一个理论或主张的基本要求。含有矛盾的理论或主张，是荒谬的，或在逻辑上不可能成立。有一种观点认为，一致性提供了对于一个数学理论的根本性辩护（比如保证了这个理论谈论的对象的存在，等等)。在历史上，著名的希尔伯特方案，就是试图使用最初等的（有穷主义的）方法证明经典数学的一致性，而哥德尔的不完全性定理则表明，形式算术理论若是一致的，则这个一致性不能在这个理论里面得到证明（从而否定了希尔伯特原初想法的可行性）。

本书一直假定，我们所讨论的一阶语言都是可数的。由于可数语言的公式集也是可数的（参见第三章「公式」一节），所以，有函数枚举所有的-公式。对于不可数语言，Lindenbaum 引理的证明需要集合论中的选择公理或与之等价的假设，具体证明参阅通行教科书（如 Ebbinghaus，Flumand Thomas 1984，或叶峰1994）。

③3.2称为强完全性定理，而3.3则是弱完全性定理。命题逻辑的弱完全性可以不用强完全性而通过构造性方法证明，就是说，这些方法提供了能行的过程，从一个重言式找到它的一个命题推演。而这里完全性的Henkin 证明则是非构造性的方法。

④公式的秩即公式所包含的联结词和量词的个数之和。具体定义见第三章第5节。

⑤具体的证明，本书不做介绍。读者可参考其他的教科书，如Ebbinghaus，Flum and Thomas (1984) 第 V 章第 3节，叶峰（1994）第三章第6节等。

⑥即|的基数│l│＝A的基数│A│，就是说，

l 与 A 之间有双射。等势的定义见第二章第4节。

Lindstom定理的证明，参见Ebbinghaus, Flum and Thomas (1984)

第XI，XI章。

⑧与此相反，关于数学的「柏拉图主义」认为，数学对象（数、函数、集合等）独立于我们的定义与构造而存在，数学理论描述客观的数学世界，因此数学命题非真即假，而其是真是假也不依赖于我们的构造或证明。经典数学和经典逻辑虽然不必然采取这种哲学上的「柏拉图主义」立场，但经常与后者联系在一起。

⑨注意，这里的「真」不是经典意义上的，而是直觉主义意义上的，相当于「可证」或「可构造」。下面提到的直觉主义「真」概念，都要在这个意义上理解。

⑩这样改变的 (∀l) 与原来的 (∃l) 的等价性，可以这样理解：原规则中关键变项 y 的所有出现都可以代以这里的常项 a，而不改变规则的构成；反之亦然。下面的 (∃E) 同样如此。但这里的新规则要求语言中有足够多的常项以供使用。我们在本节开始已经假设了这一点。

参考文献

Church,Alonzo (1936):A Noteon the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1(1936),reprinted in Davis(1965).Davis，Martin （1965）: The

Undecidable: Basic Papers on Undecidable Propositions,

Unsolvable Problems, and

ComputableFunctions,RavenPress Hewlett, New York, 1965.

Ebbinghaus, H. -D, Flum, J.and Thomas. W.(1984):MathematicalLogic， Springer-Verlag, New York,1984.

Felscher, Walter （2000）:

Lectures on Mathematical Logic,vol.

ll, Gordon and Breach SciencePublishers.Amsterdam,2000.

Frege, Gottlob （1879）:

Begriffsschrift, eine der

arithmetischen nachgebildete

Formelsprache des reinen Denkens, Louis Nebert, Halle. English translation in van Heijenoort (1967).Gentzen, Gerhard (1934

一1935)：Untersuchungen über das logische Schliessen l-ll，

Mathematische Zeitschrift.,Vol.39.English translation in M. E.Szabo

(ed.), The Cöllected Papers of GerhardGentzen. North HollandPubl.Co.,Amsterdam,1969.

Gödel, Kurt (1930): Die

Vollstandigkeit der Axiome des logischen Funktionenkalküls,

Monatshefte für Mathematik und Physik, vol. 37, 1930, included in Gödel (1986) with English

translation by Bauer-Mengelberg. Godel,Kurt (1931)：über formal unentscheidbare Satze der Principia

Mathematica und verwandter Systeme 1 Monatshefte für

Mathematik und Physik, vol. 38,1931, included in Godel (1986) with English translation by J. van Heijenoort.

Godel, Kurt (1986):CollectedWorks,vol.1.ed. S.Feferman et al.. Oxford University Press,Oxford,1986

Heijenoort, J.van(1967):FromFrege to Godel. A Source Book in Mathematical Logic, 1879 — 1931,Harvard University Press,

Cambridge, MA, 1967, reprinted1970.

Hodges Wilfrid (1997)： A

Shorter Model Theory,Cambridge University Press, Cambridge, UK,1997.

Johansson, l (1937)： Der

Minimalkalkil, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica, 4,1937.Kleene, S. C. (1952)：

Introduction to Metamathematics, North Holland Publ. Co.,

Amsterdam,1952.

Smith Peter (2007): An

Introductionto Godel's Theorems Cambridge UniversityPress,2007.Szabo, Arpad （1964）: The

Transformation of Mathematics into Deductive Science and the

Beginnings sof its Foundation on Definitions and Axioms,SCRIPTA MATHEMATICA, Vol. X X Vll, No.1,

2 (1964).

Tarski, Alfred (1933): Der

Wahrheitsbegriff in den

formalisierten Sprachen, Studia Philosophica, vol.1 (1936),

translated by L. Blaustein from the Polish original (1933), English translation in Tarski, Logic,

Semantics, Metamathematics. Papers from 1923 to 1938,

Clarendon Press,Oxford,UK.1956.Tennant,Neil (1978):NaturalLogic, Edinburgh University Press,1978, reprinted in paperback with corrections 1990.

Troelstra, A. S. and

Schwichtenberg, H (2000):BasicProof Theory, 2nd ed.,Cambridge University Press, Cambridge, UK2000.

Zalabardo, J. L. （2000）:

Introduction to the Theory of Logic, Westview Press, Oxford,2000.

刘壮虎 (1993)：《逻辑演算》，中国社会科学出版社，1993年。

刘壮虎 (2001)：《素朴集合论》，北京大学出版社，2001年。

王宪钧 (1982)：《数理逻辑引论》，北京大学出版社，1982年，1998年重版。

晏成书 (1994)：《集合论导引》，中国社会科学出版社，1994年。

叶峰(1994)：《一阶逻辑与一阶理论》，中国社会科学出版社，1994年。

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