In mathematical logic and computer science the symbol 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:

can then be read
I know A is true.[2]
In the same vein, a conditional assertion
can be read as:
From P, I know that 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
means that Q is a theorem in the system.
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 . One says that is a semantic consequence of , or , when all possible valuations in which is true, is also true. For propositional logic, it may be shown that semantic consequence and derivability are equivalent to one-another. That is, propositional logic is sound ( implies ) and complete ( implies )[5]

Typography

In TeX, the turnstile symbol 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 ().)

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

See also

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. ^ Dirk van Dalen, Logic and Structure (1980), Springer, ISBN 3-540-20879-8. See Chapter 1, section 1.5.
  6. ^ "Peter Selinger, Lecture Notes on the Lambda Calculus" (PDF).
  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 COMPUTER CO., LTD. 2015. p. 12.
  14. ^ "Remainder Calculations - Casio fx-92B User Manual [Page 13] | ManualsLib". www.manualslib.com. Retrieved 2020-12-24.
  15. ^ "Unicode standard" (PDF).
  16. ^ "CTAN: /tex-archive/macros/latex/contrib/turnstile". ctan.org.

References