LaTeX 中的克里普克模型（\mathcal{M}, w \models p）

用途

克里普克模型中的满足关系：公式 p 在模型 \mathcal{M} 的世界 w 处为真。

克里普克模型 \mathcal{M} = (W, R, V) 由世界集、可达关系和赋值组成，真值逐个世界定义，例如 \mathcal{M}, w \models \Box p 当且仅当 p 在所有 R 后继处成立。\models 是带有恰当间距的关系符；\vDash 给出相似的双十字转门字形，其否定为 \not\models 或 \nvDash。不要使用 \vdash，它表示可证性而非真。当模型固定时，作者会简写为 w \models p 或 w \Vdash p。

最小可编译示例

将其粘贴到空白 .tex 文件中，用 pdfLaTeX、XeLaTeX 或 LuaLaTeX 编译。

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Kripke Model: $\mathcal{M}, w \models p$

\[ \mathcal{M}, w \models \Box p \iff \forall v\,(wRv \Rightarrow v \models p) \]
\end{document}

相关符号

• 可能世界w
• 可达关系w R v
• 道义义务算子O p
• 下一时刻算子\bigcirc p
• 道义允许算子P p
• 直到算子p \mathcal{U} q

常见问题

如何在 LaTeX 中输入克里普克模型？

在数学模式中输入 \mathcal{M}, w \models p，例如 $\mathcal{M}, w \models \Box p \iff \forall v\,(wRv \Rightarrow v \models p)$。无需加载任何宏包即可在标准 LaTeX 中使用。

\mathcal{M}, w \models p 需要哪个宏包？

不需要。\mathcal{M}, w \models p 是标准 LaTeX 的一部分，导言区只需文档类即可编译。

\mathcal{M}, w \models p 能在文本模式中使用，还是只能用于数学模式？

只能用于数学模式。在 $...$ 之外，LaTeX 会报错 "Missing $ inserted"，所以在正文中请写 $\mathcal{M}, w \models p$。