LaTeX 中的总是算子（时序方框）（\Box p）

用途

时序意义上的“总是”：\Box p 表示 p 在当前以及运行中的每个未来时刻都成立。

在线性时序逻辑中，\Box 常写作 G（全局），安全性性质的形式为 \Box\neg\mathit{bad}。它与“最终”互为对偶，\Box p \leftrightarrow \neg\Diamond\neg p，而 \Box\Diamond p 表示 p 无穷多次发生。同一个方框在真势模态逻辑中表示必然，因此要说明采用哪种解读。\Box 和 \square 输出几乎相同的方块；\Box 是惯用的模态算子，并且它与 p 之间不会自动加间距。CTL 在它前面加路径量词，如 AG p。

最小可编译示例

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

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Always (temporal box): $\Box p$

\[ \Box(\mathit{req} \to \Diamond \mathit{grant}) \]
\end{document}

相关符号

• 最终算子（时序菱形）\Diamond p
• 公共知识C_G p
• 直到算子p \mathcal{U} q
• 信念算子B_a p
• 下一时刻算子\bigcirc p
• 知识算子K_a p

常见问题

如何在 LaTeX 中输入总是算子（时序方框）？

在数学模式中输入 \Box p，例如 $\Box(\mathit{req} \to \Diamond \mathit{grant})$。请先用 \usepackage{amssymb} 加载 amssymb。

\Box p 需要哪个宏包？

\Box p 需要 amssymb：在文档开始前把 \usepackage{amssymb} 加入导言区。

\Box p 能在文本模式中使用，还是只能用于数学模式？

只能用于数学模式。在 $...$ 之外，LaTeX 会报错 "Missing $ inserted"，所以在正文中请写 $\Box p$。