Simbolo di deduzione (tornello) in LaTeX (\vdash)

Dove si usa

Tornello: la formula a destra è derivabile (dimostrabile) dalle ipotesi a sinistra.

La teoria della dimostrazione scrive \Gamma \vdash \varphi per la conseguenza sintattica, e la teoria dei tipi lo usa nei giudizi di tipo \Gamma \vdash e : \tau. Si distingue da \models, che esprime la conseguenza semantica (verità in tutti i modelli); correttezza e completezza affermano che le due coincidono nella logica del primo ordine. Si nega con \nvdash. \vdash è una relazione, quindi la spaziatura è automatica. Per le regole di inferenza, \frac o un pacchetto dedicato agli alberi di dimostrazione produce la linea orizzontale, con giudizi contenenti \vdash sopra e sotto. Il simbolo speculare è \dashv.

Esempio minimo compilabile

Incollalo in un file .tex vuoto e compilalo con pdfLaTeX, XeLaTeX o LuaLaTeX.

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

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

Simboli correlati

• Conseguenza semantica (doppio tornello)\models
• Equivalenza (se e solo se)\iff
• Simbolo “quindi”\therefore
• Implicazione\implies
• Simbolo “poiché”\because
• Freccia doppia bidirezionale\Leftrightarrow

Domande frequenti

Come si scrive Simbolo di deduzione (tornello) in LaTeX?

Scrivi \vdash in modalità matematica, per esempio $\Gamma, x : \sigma \vdash e : \tau$. Funziona in LaTeX standard senza caricare alcun pacchetto.

Quale pacchetto serve per \vdash?

Nessuno. \vdash fa parte di LaTeX standard, quindi compila con la sola classe del documento nel preambolo.

Posso usare \vdash in modalità testo o solo in modalità matematica?

Solo in modalità matematica. Fuori da $...$ LaTeX si ferma con "Missing $ inserted", quindi nel testo scrivi $\vdash$. Se ti serve solo il glifo nel testo, incolla invece il carattere Unicode ⊢ (con XeLaTeX o LuaLaTeX e un font che lo contenga).