直觉主义 Kripke 语义

世界表示当前已经获得的信息，$w\le v$ 表示 $v$ 延伸 $w$。已证明的原子不能在信息增加后撤回，所以赋值必须持久。蕴涵则是一份面向所有未来扩张的承诺：无论以后何时获得 $A$ 的证明，都能在那里得到 $B$。

否定 $\mathrm{\neg }A$ 因而比“此刻 $A$ 不真”强。它要求任何未来都不可能建立 $A$。因此，一个世界可以既不强迫 $A$，也不强迫 $\mathrm{\neg }A$：当前尚未建立 $A$，但未来仍可能建立它。

析取与蕴涵展示两种不同的时间要求。$w⊩A\vee B$ 必须在当前状态已经选定一边；仅仅知道每条未来分支最终会决定其中一边还不够，因为不同分支可能作出不同选择。$w⊩A\to B$ 则有意推迟检查：它准备好应对任何未来出现的 $A$ 证据。一个联结词要求现在交付选择，另一个要求未来持续兑现转换，分别对应析取与蕴涵的递归条款。

取两世界链 $w_0<w_1$，只在 $w_1$ 强迫原子 $p$。持久性成立，因为一旦到达 $w_1$ 就没有更高世界撤回 $p$。在 $w_0$：

但 $w_0⊮\mathrm{\neg }p$，因为未来 $w_1$ 强迫 $p$。所以 $w_0⊮p\vee \mathrm{\neg }p$。另一方面，没有任何 $v\ge w_0$ 强迫 $\neg p$：$w_0$ 因 $w_1$ 而失败，$w_1$ 因已经强迫 $p$ 而失败。因此

同一模型也反驳双重否定消去。

若允许 $p$ 在 $w_0$ 真、在 $w_1$ 假，原子单调性立刻失败，继而公式强迫不再随信息增长保持。若把 $A\to B$ 改成只检查当前世界的经典真值条件，则未来新获得的 $A$ 无需兑现 $B$，语义会退回普通模态满足关系理路模态满足关系Modal satisfaction relation · Kripke semantics for modal logic递归规定模态公式在 Kripke 模型某一世界何时为真的关系。采用的局部布尔解释，例如排中律会在每个世界成立，已经无法刻画 IPL。

预序中可能有 $w\le v$ 且 $v\le w$ 的不同世界。单调性使它们强迫相同公式，可按互达关系取商集理路商集Quotient set · Set of equivalence classes等价关系的所有等价类组成的集合。得到偏序模型；因此，在这里的持久赋值条款下，使用全部预序模型或全部偏序模型得到相同的有效公式。

IPL 对全部持久预序模型可靠且完备：

完备性可用素理论（prime theory）构造典范世界。素性要求：若一个世界包含 $A\vee B$，就包含 $A$ 或 $B$；这恰好实现了语义中的析取条款。

有限树状 Kripke 模型常用于给 IPL 非定理提供反例，并支撑可判定性与中间逻辑研究。

Gödel 翻译理路Gödel 翻译Gödel translation · Gödel–McKinsey–Tarski translation给原子与蕴涵加上必然算子，把直觉主义命题逻辑忠实嵌入模态逻辑 S4。把这套持久语义编码进 S4：自反传递关系保留信息顺序，原子前的方框保证其真值向上稳定，蕴涵外的方框复现对全部未来的量化。