# Turnstile (symbol)

In mathematical logic and computer science the symbol ⊢ (${\displaystyle \vdash }$) has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails".

## Interpretations

The turnstile represents a binary relation. It has several different interpretations in different contexts:

• In epistemology, Per Martin-Löf (1996) analyzes the ${\displaystyle \vdash }$ symbol thus: "...[T]he combination of Frege's Urteilsstrich, judgement stroke [ | ], and Inhaltsstrich, content stroke [—], came to be called the assertion sign."[1] Frege's notation for a judgement of some content A
${\displaystyle \vdash A}$
I know A is true.[2]
In the same vein, a conditional assertion
${\displaystyle P\vdash Q}$
From P, I know that Q
${\displaystyle P\vdash Q}$
means that Q is derivable from P in the system.
Consistent with its use for derivability, a "⊢" followed by an expression without anything preceding it denotes a theorem, which is to say that the expression can be derived from the rules using an empty set of axioms. As such, the expression
${\displaystyle \vdash Q}$
means that Q is a theorem in the system.
• In proof theory, the turnstile is used to denote "provability" or "derivability". For example, if T is a formal theory and S is a particular sentence in the language of the theory then
${\displaystyle T\vdash S}$
means that S is provable from T.[4] This usage is demonstrated in the article on propositional calculus. The syntactic consequence of provability should be contrasted to semantic consequence, denoted by the double turnstile symbol ${\displaystyle \models }$. One says that ${\displaystyle S}$ is a semantic consequence of ${\displaystyle T}$, or ${\displaystyle T\models S}$, when all possible valuations in which ${\displaystyle T}$ is true, ${\displaystyle S}$ is also true. For propositional logic, it may be shown that semantic consequence ${\displaystyle \models }$ and derivability ${\displaystyle \vdash }$ are equivalent to one-another. That is, propositional logic is sound (${\displaystyle \vdash }$ implies ${\displaystyle \models }$) and complete (${\displaystyle \models }$ implies ${\displaystyle \vdash }$)[5]
• In sequent calculus, the turnstile is used to denote a sequent. A sequent ${\displaystyle A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}}$ asserts that, if all the antecedents ${\displaystyle A_{1},\,\dots ,A_{m}}$ are true, then at least one of the consequents ${\displaystyle B_{1},\,\dots ,B_{n}}$ must be true.
• In the typed lambda calculus, the turnstile is used to separate typing assumptions from the typing judgment.[6][7]
• In category theory, a reversed turnstile (${\displaystyle \dashv }$), as in ${\displaystyle F\dashv G}$, is used to indicate that the functor F is left adjoint to the functor G.[8] More rarely, a turnstile (${\displaystyle \vdash }$), as in ${\displaystyle G\vdash F}$, is used to indicate that the functor G is right adjoint to the functor F.[9]
• In APL the symbol is called "right tack" and represents the ambivalent right identity function where both XY and ⊢Y are Y. The reversed symbol "⊣" is called "left tack" and represents the analogous left identity where XY is X and ⊣Y is Y.[10][11]
• In combinatorics, ${\displaystyle \lambda \vdash n}$ means that λ is a
partition of the integer n.[12]
• In
HP Roman-8
character set used by other HP calculators.
• On the
modulo
operator; entering ${\displaystyle 5\vdash 2}$ will produce an answer of ${\displaystyle Q=2;R=1}$, where Q is the
quotient and R is the remainder. On other Casio calculators (such as on the Belgian variants—the fx-92B Spéciale Collège and fx-92B Collège 2D calculators[14]—where the decimal separator is represented as a dot instead of a comma), the modulo operator is represented by ÷R instead.
• In model theory, ${\displaystyle \varphi \vdash \psi }$ means ${\displaystyle \varphi }$ entails ${\displaystyle \psi }$, every model of ${\displaystyle \varphi }$ is a model of ${\displaystyle \psi }$.

## Typography

In TeX, the turnstile symbol ${\displaystyle \vdash }$ is obtained from the command \vdash.

In Unicode, the turnstile symbol () is called right tack and is at code point U+22A2.[15] (Code point U+22A6 is named assertion sign ().)

• U+22A2 RIGHT TACK (&RightTee;, &vdash;)
• = turnstile
• = proves, implies, yields
• = reducible
• U+22A3 LEFT TACK (&dashv;, &LeftTee;)
• = reverse turnstile
• = non-theorem, does not yield
• U+22AC DOES NOT PROVE (&nvdash;)
• ≡ 22A2⊢ 0338\$̸

On a typewriter, a turnstile can be composed from a vertical bar (|) and a dash (–).

In LaTeX there is a turnstile package which issues this sign in many ways, and is capable of putting labels below or above it, in the correct places.[16]

## Similar graphemes

• (U+A714) Modifier Letter Mid Left-Stem Tone Bar
• (U+251C) Box Drawings Light Vertical And Right
• (U+314F) Hangul Letter A
• Ͱ
(U+0370) Greek Capital Letter Heta
• ͱ
(U+0371) Greek Small Letter Heta
• (U+2C75) Latin Capital Letter Half H
• (U+2C76) Latin Small Letter Half H
• (U+23AC) Right Curly Bracket Middle Piece

## Notes

1. ^ Martin-Löf 1996, pp. 6, 15
2. ^ Martin-Löf 1996, p. 15
3. ^ "Chapter 6, Formal Language Theory" (PDF).
4. ^ Troelstra & Schwichtenberg 2000
5. . See Chapter 1, section 1.5.
6. ^
7. ^ Schmidt 1994
8. ^ "adjoint functor in nLab". ncatlab.org.
9. ^ @FunctorFact (5 July 2016). "Functor Fact on Twitter" (Tweet) – via Twitter.
10. ^ "A Dictionary of APL". www.jsoftware.com.
11. ^ Iverson 1987
12. ^ Stanley, Richard P. (1999). Enumerative Combinatorics. Vol. 2 (1st ed.). Cambridge: Cambridge University Press. p. 287.
13. ^ fx-92 Spéciale Collège Mode d'emploi (PDF). Casio. 2015. p. 12.
14. ^ "Remainder Calculations - Casio fx-92B User Manual". p. 13]. {{cite web}}: Missing or empty |url= (help)
15. ^ "Unicode standard" (PDF).
16. ^