Proves in LaTeX (\vdash)

Where it is used

Turnstile, meaning the right-hand formula is derivable (provable) from the left-hand assumptions.

Proof theory writes \Gamma \vdash \varphi for syntactic consequence, and type theory uses it in typing judgments \Gamma \vdash e : \tau. It differs from \models, which states semantic consequence (truth in all models); soundness and completeness say the two coincide in first-order logic. Negate it with \nvdash. \vdash is a relation, so spacing is automatic. For inference rules, \frac or a dedicated proof-tree package produces the horizontal line, with judgments containing \vdash above and below. The mirror symbol is \dashv.

Minimal compilable example

Paste this into an empty .tex file and compile it with pdfLaTeX, XeLaTeX or LuaLaTeX.

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

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

Related symbols

• Models\models
• If and Only If\iff
• Therefore\therefore
• Implies\implies
• Because\because
• Left Right Arrow (Double)\Leftrightarrow

Frequently asked questions

How do I write Proves in LaTeX?

Type \vdash in math mode, for example $\Gamma, x : \sigma \vdash e : \tau$. It works in plain LaTeX without loading any package.

Which package do I need for \vdash?

None. \vdash is part of standard LaTeX, so it compiles with nothing in the preamble but the document class.

Can I use \vdash in text mode, or only in math mode?

Only in math mode. Outside $...$ LaTeX stops with "Missing $ inserted", so write $\vdash$ in running text. If you only need the glyph in text, paste the Unicode character ⊢ instead (with XeLaTeX or LuaLaTeX and a font that has it).