可能世界模型

直觉主义逻辑的一种语义解释，是由美国逻辑学家克里普克于1965年提出的。这种语义解释是直觉主义逻辑的各种语义解释中较为简单而又容易应用的一种。直观地讲，直觉主义逻辑的可能世界模型(或称克里普克模型)可以用理想数学家获得知识的进程来描述。想象有一位理想的数学家，他的知识和对象领域随时间的流逝而不断增长。在各个时刻t，这位数学家有一组由他证实了的命题(这个命题组记为S)和一个对象域(记为A)。由于理想数学家的记忆良好，就有理由假定S和A都随时间t单调递增。这位数学家在任何时候对于他将来的活动都可以有种种选择(甚至完全停止活动)，因此应当认为在他活动的时间点之间有偏序关系但不一定是线性序的。现在要问的是，他将如何来解释联结词和量词?很显然，他对复合命题的解释必须依赖于他对各个支命题的解释。当他在时刻t证实了命题A或者(并且)证实了命题B时，他也就证实了命题A∨B(A∧B)。对蕴涵的解释比较麻烦，因为即使在时刻t不证实A或者B，他可以证实A→B。他所必须证实的一切就是：在他将来证实A的任何时刻也一定证实B。类似地，对于全称量同的解释也必须考虑将来的时刻，如果对于将来任一个时刻(包括时刻t)已知的任一个对象a而言他都证实了A(a)，那末他也就证实了xA(x)。但是，对于存在量词的解释就不必考虑将来的时刻，如果在时刻t他已构造一个对象a使得A()被证实，那末他也就在时刻t证实了xA(x)。理想的数学家当然在任何时候都不会证实恒假命题。命题A的否定4可以利用蕴涵联结词→和恒假命题来定义，也可以直接以为初始联结词。理想数学家在时刻t证实A，仅当他知道自己现在和将来决不会证实A。

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

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

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

③如果αA或者αB，那么aA∨B；

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

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

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

⑦如果有a∈｜D(α)｜使得αA()，那么αxA(x)；

这里，｜D(α)｜表示D(α)的个体域，α表示个体α的名字。“αA”可读成“α强制A”。令cl(A)表示A的全称闭包，即，当A的全部自由变项为x、x、…、x时，cl(A)就是闭公式xx…xA。如果对于任意的α∈M都有αcl(A)，那么称A在模型μ=(M，≤，D，)中有效。如果A在任一个克里普克模型中都有效，那么称A为有效的或普遍有效的，记为A。令Γ为公式集，称公式A为Γ的语义后承，记为ΓA，仅当任一个使Γ中任意公式在其中有效的克里普克模型也一定使A在其中有效。直觉主义逻辑相对于克里普克模型是可靠而完全的，也就是说，公式A是Γ的语义后承当且仅当它是从Γ可推导的。

克里普克模型在设计反模型和直接的理论应用方面，比直觉主义逻辑的其它一些语义解释要方便一点。此外，克里普克模型在直觉主义算术和分析的元数学研究中也很有用处。