直觉主义 Kripke 语义

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

否定 $\mathrm{\neg }A$ 因而比“此刻 $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$，语义会退回局部布尔解释，不能再证明 IPL 的预期完备性。

预序中可能有 $w\le v$ 且 $v\le w$ 的不同世界。单调性使它们强迫相同公式，可按互达关系取商得到偏序模型；因此使用预序或偏序通常不改变有效公式，但证明时仍需说明采用哪一约定。

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

完备性可用饱和理论或 prime theory 构造典范世界；析取条款需要世界具有足够的 prime 性，不能把经典最大一致集证明逐字照搬。

有限树状 Kripke 模型常用于给 IPL 非定理提供反例，并支撑可判定性与中间逻辑研究。分支表示不同的相容信息扩张，不代表概率选择；若需要概率或时间，必须另加结构。

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