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}$

can then be read

I know A is true.^[2]

In the same vein, a conditional assertion

${\displaystyle P\vdash Q}$

can be read as:

From P, I know that Q

• In metalogic, the study of formal languages; the turnstile represents syntactic consequence (or "derivability"). This is to say, that it shows that one string can be derived from another in a single step, according to the transformation rules (i.e. the syntax) of some given formal system.^[3] As such, the expression

${\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 X⊢Y and ⊢Y are Y. The reversed symbol "⊣" is called "left tack" and represents the analogous left identity where X⊣Y 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 (⊢, ⊢)
  • = turnstile
  • = proves, implies, yields
  • = reducible
• U+22A3 ⊣ LEFT TACK (⊣, ⊣)
  • = reverse turnstile
  • = non-theorem, does not yield
• U+22AC ⊬ DOES NOT PROVE (⊬)
  • ≡ 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

See also

• Double turnstile ⊨
• List of logic symbols
• List of mathematical symbols

Notes