贝思模型

直觉主义逻辑的一种语义解释，最初由荷兰逻辑学家E．W．贝思于1956年提出。直观上，贝思模型跟克里普克模型一样也可用理想数学家获得知识的进程来描述，不过对于析取联结词和存在量词的解释是有所不同的。当它在时刻t能够肯定，无论将来的选择如何，它终究能证实A或者证实B，这样也就在时刻t证实了命题A∨B。类似地，当理想数学家在时刻t能够肯定，无论将来的选择如何，他总可得到一个个体a使得命题A()被证实，这样他也就在时刻t证实了xA(x)。对于其它联结词乛、∧、→和全称量词的解释都完全跟克里普克模型中的解释相同。任一个克里普克模型都可转换成一个与之等价的贝思模型。1984年D．范达伦(1932一 )提出了两种模型的一个共同推广。

直觉主义逻辑贝思模型的精确定义如下：一个贝思模型就是一个四元序组α=(M，≤，D，)，其中(M，≤)是一个偏序集；D是M上的一个映射，它将M中任意元素α映成相应于语言的一个一阶结构D(α)，并且对于任意的α，β∈M而言，如果α≤β则D(α)的个体域｜D(α)｜是D(β)的个体域D(β)｜的子集，而且D(α)对各个谓词的解释被含于D(β)对它的解释；是M中元素与不含有自由变项的公式之间的一个二元关系，它的归纳定义如下：

①如果一阶结构D(α)满足原子公式A，那末αA；

②如果αA并且αβ，那末αA∧B；

③如果在M的任一个含有α的极大线性序子集N中都有元素β使得βA或βB，那末αA∨B；

④如果对一切≥α的β有，βAβB，那末aA→B；

⑤如果对一切≥α的β有，βA，即，βA不成立，那末α乛A；

⑥如果对一切≥α的β和一切a∈｜D(β)｜有，βA(ā)，那末α xA(x)；

⑦如果在M的任一个含有α的极大线性序子集N中都有元素β并且有个体a∈｜D(β)｜使得βA()，那末α xA(x)。

M的一个含有α的极大线性序子集相当于理想数学家关于α的将来所可能作的一个选择。“αA”可读成“α强制A”。令cl(A)表示A的全称闭包，即，当A的全部自由变项为x、x、…、x时，cl(A)就是闭公式 x x… xA。如果对于任意α∈M都有αcl(A)，那末称A在模型μ=(M，≤，D，)中有效。如果A在任一个贝思模型中都有效，那末称A为有效的或普遍有效的，记为A。令Γ为公式集，称公式A为Γ的语义后承，记为ΓA，仅当任一个使Γ中任意公式在其中有效的贝思模型也一定使A在其中有效。直觉主义逻辑相对于贝思模型是可靠而又完全的，也就是说，公式A是Γ的语义后承当且仅当它是Γ可推导的。