模态满足关系

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

递归定义让嵌套模态具有明确的路径深度。$\square ◇p$ 先对每个一步后继 $v$ 提要求，再允许每个 $v$ 各自选择一个下一步见证；它与 $◇\square 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,b$ 的全部后继；在当前图中选择 $a$ 即可，因 $a$ 的唯一后继 $c$ 满足 $p$。

若再给 $a$ 增加一个不满足 $p$ 的后继 $d$，最后一项仍可能由 $b$ 作见证；只有让 $a,b$ 各自都有失败后继，$◇\square p$ 才会失败。这个轨迹展示量词嵌套的真实机制，而不是更换原子真值后的同型算例。

死端世界 $z$ 满足每个 $\square \phi$，却不满足任何 $◇\phi$。前者是全称量化在空后继集上的空真，不表示 $z$ “知道所有事实”。若应用不允许死端，应在框架层要求串行，而不能临时改写真值条款。

还要区分局部与全局：$\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在信息增长的预序世界上用持久赋值和未来量化解释直觉主义联结词的语义。相比，此处的蕴涵与否定只在当前世界按经典真值解释。直觉主义蕴涵会量化所有更强信息状态，原子赋值还必须持久；两套语义共享关系图外观，却不能混用递归条款。