Models in LaTeX (\models)

Where it is used

Double turnstile: semantic entailment or satisfaction, meaning true in every model.

\mathcal{M} \models \varphi says structure M satisfies formula \varphi, and \Gamma \models \varphi says every model of \Gamma satisfies \varphi. It contrasts with \vdash, which is syntactic provability. Its negation is \not\models or the dedicated glyph \nvDash. The similar \vDash has slightly different proportions and is used in some logics alongside \Vdash for forcing in set theory. As a relation, it gets spacing on both sides. Model checking writes s \models \phi for a state satisfying a temporal formula.

Minimal compilable example

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

\documentclass{article}
\begin{document}
Models: $\models$

\[ \Gamma \models \varphi \iff \Gamma \vdash \varphi \]
\end{document}

Related symbols

• Therefore\therefore
• Proves\vdash
• Because\because
• If and Only If\iff
• Contradiction (falsum, bottom)\bot
• Implies\implies

Frequently asked questions

How do I write Models in LaTeX?

Type \models in math mode, for example $\Gamma \models \varphi \iff \Gamma \vdash \varphi$. It works in plain LaTeX without loading any package.

Which package do I need for \models?

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

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

Only in math mode. Outside $...$ LaTeX stops with "Missing $ inserted", so write $\models$ 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).