Kripke 模型

框架回答“从这里需要考虑哪些情形”，赋值回答“每个基本事实在哪些情形成立”。两部分缺一不可。只有赋值而没有边，$\square$ 和 $◇$ 没有量化范围；只有边而没有赋值，关系结构存在，却无法开始递归判断任何含原子的公式。

有点模型把观察位置也纳入对象。同一张世界图在 $w_0$ 与 $w_1$ 处可能给出不同答案，不是因为模型改变，而是观察者拥有不同的后继集合。模态逻辑研究的正是这种“位置相关但按统一规则计算”的真值。

令 $W=\{s,t,u\}$，关系为 $sRt,sRu,tRu$，赋值取

在 $s$ 看来，两个直接后继都满足 $p$，但只有 $u$ 满足 $q$；在 $t$ 看来，唯一后继 $u$ 同时满足 $p,q$。这个模型足以区分“所有下一种情形满足 $p$”与“至少一种下一情形满足 $q$”，也显示 $t$ 能借一步看见 $u$，并不让 $s$ 自动把 $u$ 当成经 $t$ 到达的第二步世界——$sRu$ 是否成立仍由原关系明确给出。

若把 $V(q)$ 改为 $\{t,u\}$，框架完全不变，但关于 $q$ 的公式真值会改变。反过来，保持赋值不动而删除 $sRu$，关于 $p$ 的原子真假不变，$\square p$、$◇q$ 等模态公式却可能改变。模型的两个组成部分承担不同信息，不能用“世界状态”一个模糊词同时代替。

普通模态 Kripke 模型不要求赋值沿 $R$ 单调。即使 $wRv$ 且 $p$ 在 $w$ 真，$p$ 也可以在 $v$ 假。持久性是直觉主义 Kripke 语义公理库直觉主义 Kripke 语义Intuitionistic Kripke semantics · Kripke semantics for IPL在信息增长的预序世界上用持久赋值和未来量化解释直觉主义联结词的语义。额外加入的条件；把它无声放进一般模态模型会错误排除合法反模型。

模态满足关系公理库模态满足关系Modal satisfaction relation · Kripke semantics for modal logic递归规定模态公式在 Kripke 模型某一世界何时为真的关系。把 $V$ 的原子情况递归扩张到布尔联结词和模态算子。一个公式在模型中全局为真，仍不等于它在底层框架上有效：框架有效还要对所有可能赋值重新检查。

典范模态模型公理库模态逻辑的典范模型Canonical modal model · Canonical model for K以最大一致公式集为世界、由方框义务定义可达边的句法生成 Kripke 模型。把最大一致公式集当作世界，是从句法自动制造 Kripke 模型的特殊构造。过滤法公理库Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。则从已有模型出发，把对有限公式集无法区分的世界合并。一个展开句法，一个压缩语义，但二者都必须明确给出 $W,R,V$，并证明新模型的满足关系具有所需性质。

模态互模拟公理库模态互模拟Modal bisimulation · Kripke bisimulation用原子一致与沿可达边的 forth、back 条件比较两个 Kripke 模型的模态行为。比较两个模型的原子赋值和逐步分支。互模拟不要求世界集合等大，也不要求存在全局双射；它只维护模态语言实际能追踪的局部行为，因此比模型同构弱得多。