Ableitbarkeitszeichen (Turnstile) in LaTeX (\vdash)

Verwendung

Das Drehkreuz besagt, dass die Formel rechts aus den Annahmen links herleitbar (beweisbar) ist.

In der Beweistheorie schreibt man \Gamma \vdash \varphi für syntaktische Folgerung, und die Typentheorie verwendet es in Typisierungsurteilen \Gamma \vdash e : \tau. Es unterscheidet sich von \models, das die semantische Folgerung (Wahrheit in allen Modellen) ausdrückt; Korrektheit und Vollständigkeit besagen, dass beide in der Prädikatenlogik erster Stufe zusammenfallen. Die Negation ist \nvdash. \vdash ist eine Relation, die Abstände werden also automatisch gesetzt. Für Schlussregeln erzeugt \frac oder ein spezielles Paket für Beweisbäume den waagerechten Strich, mit Urteilen, die \vdash enthalten, darüber und darunter. Das Spiegelsymbol ist \dashv.

Minimales kompilierbares Beispiel

Fügen Sie dies in eine leere .tex-Datei ein und kompilieren Sie mit pdfLaTeX, XeLaTeX oder LuaLaTeX.

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

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

Verwandte Symbole

• Semantische Folgerung (doppeltes Turnstile)\models
• Äquivalenz (genau dann, wenn)\iff
• Folgerungszeichen „also“\therefore
• Implikation\implies
• Begründungszeichen „weil“\because
• Doppelpfeil nach links und rechts\Leftrightarrow

Häufige Fragen

Wie schreibe ich Ableitbarkeitszeichen (Turnstile) in LaTeX?

Schreiben Sie \vdash im Mathematikmodus, zum Beispiel $\Gamma, x : \sigma \vdash e : \tau$. Es funktioniert in Standard-LaTeX, ohne ein Paket zu laden.

Welches Paket brauche ich für \vdash?

Keines. \vdash gehört zum Standardumfang von LaTeX und kompiliert ohne weitere Angaben in der Präambel außer der Dokumentklasse.

Kann ich \vdash im Textmodus verwenden oder nur im Mathematikmodus?

Nur im Mathematikmodus. Außerhalb von $...$ bricht LaTeX mit "Missing $ inserted" ab, schreiben Sie im Fließtext also $\vdash$. Wenn Sie nur das Zeichen im Text brauchen, fügen Sie stattdessen das Unicode-Zeichen ⊢ ein (mit XeLaTeX oder LuaLaTeX und einer Schrift, die es enthält).