模态满足关系

$\square$ 与 $◇$ 是沿关系边作全称和存在量化。判断 $w$ 的 $\square \phi$ 时，不看 $\phi$ 在 $w$ 自己是否成立，除非框架恰有自环；它逐一检查 $w$ 能看见的世界。$◇\phi$ 只需找到一条边和一个见证世界。两者的对偶来自经典否定把“并非所有后继都失败”化成“某个后继成功”。

递归定义让嵌套模态具有明确的路径深度。$\square ◇p$ 先对每个一步后继 $v$ 提要求，再允许每个 $v$ 各自选择一个下一步见证；$◇\square p$ 则先选一个后继，再要求这个后继的所有下一步都满足 $p$；两个公式的量词顺序不同。

令 $W=\{w,a,b,c\}$，边为 $wRa,wRb,aRc,bRc$，且 $V(p)=\{a,c\}$。在 $w$：

• $◇p$ 为真，因为 $a$ 是满足 $p$ 的直接后继；
• $\square p$ 为假，因为直接后继 $b$ 不满足 $p$；
• $\square ◇p$ 为真，因为 $a,b$ 都能到达满足 $p$ 的 $c$；
• $◇\square p$ 为真：选择 $a$ 即可，因 $a$ 的唯一后继 $c$ 满足 $p$。

若再给 $a$ 增加一个不满足 $p$ 的后继 $d$，最后一项仍可由 $b$ 作见证；只有让 $a,b$ 各自都有失败后继，$◇\square p$ 才会失败。

死端世界 $z$ 满足每个 $\square \phi$，却不满足任何 $◇\phi$。这是全称与存在量化在空后继集上的结果。若应用要求每个世界至少有一个后继，就选取满足串行条件的框架。

还要区分局部与全局：$\mathcal{M},w⊩\phi$ 只谈一个点，$\mathcal{M}⊩\phi$ 谈固定赋值下所有点，$\mathcal{F}⊩\phi$ 再量化框架上的所有赋值。公式的逻辑有效性则进一步要求它在所讨论框架类的全部模型与世界中成立。

模态逻辑 K理路K 模态逻辑Modal logic K · System K由全部命题重言式、K 公理、modus ponens、代入与必然化生成的最小正规模态逻辑。对所有 Kripke 模型可靠且完备；分配公理

之所以在每个世界成立，是因为两个方框共享同一批后继，可在每个后继使用一次 modus ponens。这个证明直接展开满足条款，不需要假定 $R$ 具备任何额外性质。

典范模型定理理路模态逻辑典范模型定理Canonical model theorem for modal logic · Truth lemma for modal KK 的典范模型中公式在世界为真，当且仅当公式属于对应的最大一致集。证明句法成员关系与这里的满足关系逐公式一致；过滤法理路Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。证明商模型对指定子公式集保持这里的真值；模态互模拟理路模态互模拟Modal bisimulation · Kripke bisimulation用原子一致与沿可达边的 forth、back 条件比较两个 Kripke 模型的模态行为。则通过结构归纳证明相关世界满足相同公式。三项元理论都以这组递归条款为共同接口。

与直觉主义 Kripke 语义理路直觉主义 Kripke 语义Intuitionistic Kripke semantics · Kripke semantics for IPL在信息增长的预序世界上用持久赋值和未来量化解释直觉主义联结词的语义。相比，此处的蕴涵与否定只在当前世界按经典真值解释。直觉主义蕴涵会量化所有更强信息状态，原子赋值还必须持久；这些条款使公式的真值随信息增长保持。