Conséquence sémantique (double taquet) en LaTeX (\models)

Où il est utilisé

Double taquet : conséquence sémantique ou satisfaction, c'est-à-dire vérité dans tout modèle.

\mathcal{M} \models \varphi signifie que la structure M satisfait la formule \varphi, et \Gamma \models \varphi que tout modèle de \Gamma satisfait \varphi. Il s'oppose à \vdash, qui exprime la prouvabilité syntaxique. Sa négation est \not\models ou le glyphe dédié \nvDash. Le symbole voisin \vDash a des proportions légèrement différentes et s'emploie dans certaines logiques à côté de \Vdash pour le forcing en théorie des ensembles. Comme c'est une relation, il reçoit une espace de chaque côté. En vérification de modèles, on écrit s \models \phi pour un état qui satisfait une formule temporelle.

Exemple minimal compilable

Collez-le dans un fichier .tex vide et compilez avec pdfLaTeX, XeLaTeX ou LuaLaTeX.

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

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

Symboles associés

• Signe « donc »\therefore
• Symbole de déduction (taquet)\vdash
• Signe « car »\because
• Si et seulement si\iff
• Contradiction (falsum, minimum)\bot
• Implication\implies

Questions fréquentes

Comment écrire Conséquence sémantique (double taquet) en LaTeX ?

Tapez \models en mode mathématique, par exemple $\Gamma \models \varphi \iff \Gamma \vdash \varphi$. La commande fonctionne en LaTeX standard sans charger de paquet.

Quel paquet faut-il pour \models ?

Aucun. \models fait partie de LaTeX standard : le préambule n’a besoin que de la classe de document.

Peut-on utiliser \models en mode texte, ou seulement en mode mathématique ?

Seulement en mode mathématique. Hors de $...$, LaTeX s’arrête avec "Missing $ inserted" : dans le texte, écrivez $\models$. Si vous voulez seulement le glyphe dans le texte, collez le caractère Unicode ⊨ (avec XeLaTeX ou LuaLaTeX et une police qui le contient).