LaTeX 中的推出符号（可证）（\vdash）

用途

十字转门符号，表示右侧公式可以从左侧的假设推导（证明）出来。

证明论用 \Gamma \vdash \varphi 表示语法后承，类型论则在类型判断 \Gamma \vdash e : \tau 中使用它。它不同于 \models，后者表示语义后承（在所有模型中为真）；可靠性定理和完备性定理表明二者在一阶逻辑中一致。其否定形式是 \nvdash。\vdash 是关系符，间距会自动处理。对于推理规则，可用 \frac 或专门的证明树宏包画出横线，上下两侧放含有 \vdash 的判断。它的镜像符号是 \dashv。

最小可编译示例

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

\documentclass{article}
\begin{document}
Proves: $\vdash$

\[ \Gamma, x : \sigma \vdash e : \tau \]
\end{document}

相关符号

• 语义蕴涵符号（满足）\models
• 当且仅当符号\iff
• 所以符号\therefore
• 蕴含符号\implies
• 因为符号\because
• 双线左右箭头\Leftrightarrow

常见问题

如何在 LaTeX 中输入推出符号（可证）？

在数学模式中输入 \vdash，例如 $\Gamma, x : \sigma \vdash e : \tau$。无需加载任何宏包即可在标准 LaTeX 中使用。

\vdash 需要哪个宏包？

不需要。\vdash 是标准 LaTeX 的一部分，导言区只需文档类即可编译。

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

只能用于数学模式。在 $...$ 之外，LaTeX 会报错 "Missing $ inserted"，所以在正文中请写 $\vdash$。 如果只需要在正文中显示该字形，可以直接粘贴 Unicode 字符 ⊢（需使用 XeLaTeX 或 LuaLaTeX 以及包含该字形的字体）。