直觉主义完全性（逻辑论文） (11-2)

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

φ的证明是一个构造方法，它把每个φ的证明转换为对于矛盾或荒谬句(如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。

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。