Знак выводимости в 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 и шрифтом, в котором он есть).