Symbole de déduction (taquet) en LaTeX (\vdash)

Où il est utilisé

Taquet (thèse) : la formule de droite est dérivable (démontrable) à partir des hypothèses de gauche.

La théorie de la démonstration écrit \Gamma \vdash \varphi pour la conséquence syntaxique, et la théorie des types l'utilise dans les jugements de typage \Gamma \vdash e : \tau. Il se distingue de \models, qui exprime la conséquence sémantique (vérité dans tous les modèles) ; la correction et la complétude affirment que les deux coïncident en logique du premier ordre. Sa négation s'écrit \nvdash. \vdash est une relation, l'espacement est donc automatique. Pour les règles d'inférence, \frac ou un paquet dédié aux arbres de preuve produit le trait horizontal, avec des jugements contenant \vdash au-dessus et en dessous. Le symbole miroir est \dashv.

Exemple minimal compilable

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

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

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

Symboles associés

• Conséquence sémantique (double taquet)\models
• Si et seulement si\iff
• Signe « donc »\therefore
• Implication\implies
• Signe « car »\because
• Double flèche gauche-droite\Leftrightarrow

Questions fréquentes

Comment écrire Symbole de déduction (taquet) en LaTeX ?

Tapez \vdash en mode mathématique, par exemple $\Gamma, x : \sigma \vdash e : \tau$. La commande fonctionne en LaTeX standard sans charger de paquet.

Quel paquet faut-il pour \vdash ?

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

Peut-on utiliser \vdash 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 $\vdash$. Si vous voulez seulement le glyphe dans le texte, collez le caractère Unicode ⊢ (avec XeLaTeX ou LuaLaTeX et une police qui le contient).